@inproceedings(AFV13,
 author       = {M. Alpuente and {M. A.} Feli\'u and A. Villanueva},
 year         = {2013},
 title        = {{Automatic Inference of Specifications using Matching Logic}},
 booktitle    = {Proc.e {ACM} {SIGPLAN} 2013 Workshop on Partial Evaluation and Program Manipulation, {PEPM} 2013},
 publisher    = {ACM},
 pages        = {127--136},
 doi          = {10.1145/2426890.2426914},
)
@article(APV2009-LazyInit,
 author       = {S. Anand and {C. S.} Pasareanu and W. Visser},
 year         = {2009},
 title        = {{Symbolic execution with abstraction}},
 journal      = {International Journal on Software Tools for Technology Transfer (STTT)},
 volume       = {11},
 number       = {1},
 pages        = {53--67},
 doi          = {10.1007/s10009-008-0090-1},
)
@inproceedings(Arusoaie-SymbolicK2014,
 author       = {A. Arusoaie and D. Lucanu and V. Rusu and {T.{-}F.} Serbanuta and A. Stefanescu and Ro\c{s}u, G.},
 year         = {2014},
 title        = {{Language Definitions as Rewrite Theories}},
 booktitle    = {10th International Workshop on Rewriting Logic and Its Applications (WRLA), Revised Selected Papers},
 pages        = {97--112},
 doi          = {10.1007/978-3-319-12904-4\_5},
)
@inproceedings(BacciCFV12,
 author       = {G. Bacci and M. Comini and M. A. Feli\'u and A. Villanueva},
 year         = {2012},
 title        = {{Automatic Synthesis of Specifications for First Order Curry Programs}},
 booktitle    = {Proc. of the 14th Intl. Symp. on ACM Principles and Practice of Declarative Programming (PPDP'12)},
 publisher    = {ACM Press},
 pages        = {25--34},
 doi          = {10.1145/2370776.2370781},
)
@inproceedings(ChristodorescuJK07,
 author       = {M. Christodorescu and S. Jha and C. Kruegel},
 year         = {2007},
 title        = {{Mining Specifications of Malicious Behavior}},
 booktitle    = {Proc. of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007)},
 publisher    = {ACM},
 pages        = {5--14},
 doi          = {10.1145/1287624.1287628},
)
@inproceedings(CSH2010,
 author       = {K. Claessen and N. Smallbone and J. Hughes},
 year         = {2010},
 title        = {{QuickSpec: Guessing Formal Specifications Using Testing}},
 booktitle    = {Proc, 4th Int'l Conf. on Tests and Proofs (TAP 2010)},
 series       = {Lecture Notes in Computer Science},
 volume       = {6143},
 publisher    = {Springer},
 pages        = {6--21},
 doi          = {10.1007/978-3-642-13977-2\_3},
)
@book(maude-book,
 author       = {M. Clavel and F. Dur\'{a}n and S. Eker and P. Lincoln and Mart\'{\i}-Oliet, N. and J. Meseguer and C. Talcott},
 year         = {2007},
 title        = {{All About Maude: A High-Performance Logical Framework}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4350},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-540-71999-1\_7},
)
@inproceedings(dysy,
 author       = {C. Csallner and N. Tillmann and Y. Smaragdakis},
 year         = {2008},
 title        = {{DySy: Dynamic Symbolic Execution for Invariant Inference}},
 booktitle    = {Proc. 30th International Conference on Software Engineering (ICSE 2008)},
 publisher    = {ACM},
 pages        = {281--290},
 doi          = {10.1145/1368088.1368127},
)
@article(DSilvaKW08,
 author       = {V. D'Silva and {D. I.} Kroening and G. Weissenbacher},
 year         = {2008},
 title        = {A Survey of Automated Techniques for Formal Software Verification},
 journal      = {IEEE Trans. on CAD of Integrated Circuits and Systems},
 volume       = {27},
 number       = {7},
 pages        = {1165--1178},
 doi          = {10.1109/TCAD.2008.923410},
)
@inproceedings(ellison-rosu-2012-popl,
 author       = {C. Ellison and Ro\c{s}u, G.},
 year         = {2012},
 title        = {An Executable Formal Semantics of {C} with Applications},
 booktitle    = {Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12)},
 publisher    = {ACM},
 pages        = {533--544},
 doi          = {10.1145/2103656.2103719},
)
@article(Daikon,
 author       = {M. D. Ernst and J. H. Perkins and P. J. Guo and S. McCamant and C. Pacheco and M. S. Tschantz and C. Xiao},
 year         = {2007},
 title        = {{The Daikon System for Dynamic Detection of Likely Invariants}},
 journal      = {Sci. Comput. Program.},
 volume       = {69},
 number       = {1-3},
 pages        = {35--45},
 doi          = {10.1016/j.scico.2007.01.015},
)
@inproceedings(Ghezzi09,
 author       = {C. Ghezzi and A. Mocci and M. Monga},
 year         = {2009},
 title        = {{Synthesizing Intensional Behavior Models by Graph Transformation}},
 booktitle    = {Proc. 3st Int'l Conf. on Software Engineering (ICSE 2009)},
 publisher    = {IEEE},
 pages        = {430--440},
 doi          = {10.1109/ICSE.2009.5070542},
)
@inproceedings(GPasareanu,
 author       = {D. Giannakopoulou and C. S. Pasareanu},
 year         = {2009},
 title        = {{Interface Generation and Compositional Verification in JavaPathfinder}},
 booktitle    = {Proc. 12th In'l Conf. on Fundamental Approaches to Software Engineering (FASE 2009)},
 series       = {Lecture Notes in Computer Science},
 volume       = {5503},
 publisher    = {Springer},
 pages        = {94--108},
 doi          = {10.1007/978-3-642-00593-0\_7},
)
@inproceedings(DIDUCE,
 author       = {S. Hangal and M. S. Lam},
 year         = {2002},
 title        = {{Tracking down Software Bugs using Automatic Anomaly Detection}},
 booktitle    = {Proc. 22rd International Conference on Software Engineering (ICSE 2002)},
 publisher    = {ACM},
 pages        = {291--301},
 doi          = {10.1145/581339.581377},
)
@inproceedings(Diwan,
 author       = {J. Henkel and A. Diwan},
 year         = {2003},
 title        = {{Discovering Algebraic Specifications from Java Classes}},
 booktitle    = {Proc. ECOOP},
 pages        = {431--456},
 doi          = {10.1007/978-3-540-45070-2\_19},
)
@inproceedings(GenSymbExec2003,
 author       = {S. Khurshid and {C. S.} Pasareanu and W. Visser},
 year         = {2003},
 title        = {Generalized Symbolic Execution for Model Checking and Testing},
 booktitle    = {TACAS},
 pages        = {553--568},
 doi          = {10.1007/3-540-36577-X\_40},
)
@article(King1976,
 author       = {J. C. King},
 year         = {1976},
 title        = {Symbolic execution and program testing},
 journal      = {Commun. ACM},
 volume       = {19},
 number       = {7},
 pages        = {385--394},
 doi          = {10.1145/360248.360252},
)
@book(Liskov86,
 author       = {B. Liskov and J. Guttag},
 year         = {1986},
 title        = {Abstraction and specification in program development},
 publisher    = {MIT Press},
)
@inproceedings(Z3-2008,
 author       = {{L. M.} de Moura and B. Nikolaj},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 booktitle    = {14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@article(PasareanuV09,
 author       = {C. S. Pasareanu and W. Visser},
 year         = {2009},
 title        = {{A Survey of new Trends in Symbolic Execution for Software Testing and Analysis}},
 journal      = {STTT},
 volume       = {11},
 number       = {4},
 pages        = {339--353},
 doi          = {10.1007/s10009-009-0118-1},
)
@inproceedings(Rosu2015,
 author       = {Ro\c{s}u, G.},
 year         = {2015},
 title        = {{From Rewriting Logic, to Programming Language Semantics, to Program Verification}},
 booktitle    = {{Logic, Rewriting, and Concurrency - Festschrift Symposium in Honor of Jos\'e Meseguer}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9200},
 publisher    = {Springer Verlag},
 pages        = {598--216},
 doi          = {10.1007/978-3-319-23165-5\_28},
)
@inproceedings(rosu-schulte-serbanuta-2009-rv,
 author       = {Ro\c{s}u, G. and W. Schulte and {T.{-}F.} Serbanuta},
 year         = {2009},
 title        = {Runtime Verification of {C} Memory Safety},
 booktitle    = {Runtime Verification (RV'09)},
 series       = {Lecture Notes in Computer Science},
 volume       = {5779},
 pages        = {132--152},
 doi          = {10.1007/978-3-642-04694-0\_10},
)
@article(RosuS2010,
 author       = {Ro\c{s}u, G. and {T.{-}F.} Serbanuta},
 year         = {2010},
 title        = {{An Overview of the \unhbox\voidb@x \hbox{$\mathbb{K}$}\xspace\ Semantic Framework}},
 journal      = {J. Log. Algebr. Program.},
 volume       = {79},
 number       = {6},
 pages        = {397--434},
 doi          = {10.1016/j.jlap.2010.03.012},
)
@inproceedings(RosuS11,
 author       = {Ro\c{s}u, G. and A. Stefanescu},
 year         = {2011},
 title        = {{Matching Logic: A New Program Verification Approach}},
 booktitle    = {Proceedings of the 33rd International Conference on Software Engineering, {ICSE} 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011},
 publisher    = {{ACM}},
 pages        = {868--871},
 doi          = {10.1145/1985793.1985928},
)
@article(TaghdiriJ07,
 author       = {M. Taghdiri and D.Jackson},
 year         = {2007},
 title        = {{Inferring Specifications to Detect Errors in Code}},
 journal      = {Autom. Softw. Eng.},
 volume       = {14},
 number       = {1},
 pages        = {87--121},
 doi          = {10.1007/s10515-006-0005-x},
)
@inproceedings(TillmannCS06,
 author       = {N. Tillmann and F. Chen and W. Schulte},
 year         = {2006},
 title        = {{Discovering Likely Method Specifications}},
 booktitle    = {Proc. 8th Int'l Conf. on Formal Engineering Methods (ICFEM 2006)},
 series       = {Lecture Notes in Computer Science},
 volume       = {4260},
 publisher    = {Springer},
 pages        = {717--736},
 doi          = {10.1007/11901433\_39},
)
@inproceedings(WhaleyML02,
 author       = {J. Whaley and {M. C.} Martin and {M. S.} Lam},
 year         = {2002},
 title        = {Automatic extraction of object-oriented component interfaces},
 booktitle    = {Proc. ISSTA 2002},
 pages        = {218--228},
 doi          = {10.1145/566172.566212},
)