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