Program Equivalence by Circular Reasoning, In Integrated Formal Methods Lecture Notes in Computer Science, vol.7940, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01065830
A Generic Framework for Symbolic Execution, 6th International Conference on Software Language Engineering, pp.281-301, 2013. ,
DOI : 10.1007/978-3-319-02654-1_16
URL : https://hal.archives-ouvertes.fr/hal-00853588
Proving optimizations correct using parameterized program equivalence, Programming Languages Design and Implementation, pp.327-337, 2009. ,
DOI : 10.1145/1543135.1542513
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.348.3828
Inference rules for proving the equivalence of recursive procedures, Acta Informatica, vol.21, issue.7, pp.403-439, 2008. ,
DOI : 10.1007/s00236-008-0075-2
Regression verification, Proceedings of the 46th Annual Design Automation Conference on ZZZ, DAC '09 ,
DOI : 10.1145/1629911.1630034
Regression Verification for Multi-threaded Programs, Lecture Notes in Computer Science, vol.6, issue.5, pp.119-135, 2012. ,
DOI : 10.1007/BF00268134
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Translation validation for an optimizing compiler, pp.83-94, 2000. ,
Operational semantics and program equivalence Advanced Lectures, Applied Semantics, International Summer School, pp.378-412, 2000. ,
DOI : 10.1007/3-540-45699-6_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.166
Formal Verification of Backward Compatibility of Microcode, Computer-Aided Verification, pp.185-198, 2005. ,
DOI : 10.1007/11513988_20
Proving the Equivalence of CLP Programs, International Conference of Logic Programming, pp.287-301, 2002. ,
DOI : 10.1007/3-540-45619-8_20
Symdiff: A language-agnostic semantic diff tool for imperative programs, Computer Aided Verification, pp.712-717, 2012. ,
Electronic Design Automation For Integrated Circuits Handbook, 2006. ,
Circular Coinduction: A Proof Theoretical Foundation, CALCO 2009, pp.127-144, 2009. ,
DOI : 10.1007/978-3-540-73859-6_25
Symbolic Model Checking of Infinite-State Systems Using Narrowing, Term Rewriting and Applications, 18th International Conference, pp.153-168, 2007. ,
DOI : 10.1007/978-3-540-73449-9_13
An overview of the K semantic framework, The Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010. ,
DOI : 10.1016/j.jlap.2010.03.012
Co-Logic Programming: Extending Logic Programming with Coinduction, ICALP, pp.472-483, 2007. ,
DOI : 10.1007/978-3-540-73420-8_42
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.9618
Corecursive Featherweight Java, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP '12, pp.3-10 ,
DOI : 10.1145/2318202.2318205
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.413.5137
Checking reachability using matching logic, Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12, 2012. ,
A Generic Approach to Symbolic Execution ,
A Decision Procedure for Bisimilarity of Generalized Regular Expressions, Proc. 13th Brazilian Symposium on Formal Methods, pp.226-241, 2011. ,
DOI : 10.1145/321312.321326
All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007. ,
Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems RESEARCH CENTRE LILLE ? NORD EUROPE Parc scientifique de la Haute-Borne 40 avenue Halley -Bât A -Park Plaza 59650 Villeneuve d'Ascq, pp.337-340, 2008. ,