The KeY tool. Software and Systems Modeling, pp.32-54, 2005. ,

Model Checking Linear Programs with Arrays, Electronic Notes in Theoretical Computer Science, vol.144, issue.3, pp.79-94, 2006. ,

DOI : 10.1016/j.entcs.2006.01.006

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

Symbolic execution based on language transformation Computer Languages, Systems & Structures, 2015. To appear, preprint available at https ,

The Spec# Programming System: An Overview, Proc. 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS'04, pp.49-69, 2005. ,

DOI : 10.1007/978-3-540-30569-9_3

Symbolic Execution with Separation Logic, Yi [48], pp.52-68 ,

DOI : 10.1007/11575467_5

Klee: unassisted and automatic generation of high-coverage tests for complex systems programs, Proc. 8th USENIX conference on Operating systems design and implementation, OSDI'08, pp.209-224, 2008. ,

EXE: automatically generating inputs of death, ACM Conference on Computer and Communications Security, pp.322-335, 2006. ,

Hardware verification using ANSI-C programs as a reference, Proceedings of the 2003 Asia and South Pacific Design Automation Conference, ASP-DAC '03, pp.308-311, 2003. ,

All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, 2007. ,

Using symbolic execution for verifying safety-critical systems, ACM SIGSOFT Software Engineering Notes, vol.26, issue.5, pp.142-151, 2001. ,

DOI : 10.1145/503271.503230

Introduction to Algorithms, 2001. ,

All-Path Reachability Logic, Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), pp.425-440, 2014. ,

DOI : 10.1007/978-3-319-08918-8_29

Verifying systems rules using rule-directed symbolic execution, ACM SIGPLAN Notices, vol.48, issue.4, pp.329-342, 2013. ,

DOI : 10.1145/2499368.2451152

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.310.2374

Parameterized unit testing with Pex, TAP, pp.171-181, 2008. ,

Z3: An efficient SMT solver In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS'08, pp.337-340, 2008. ,

Variant Narrowing and Equational Unification, Electronic Notes in Theoretical Computer Science, vol.238, issue.3, pp.103-119, 2009. ,

DOI : 10.1016/j.entcs.2009.05.015

Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013. ,

DOI : 10.1007/978-3-642-37036-6_8

DART: directed automated random testing, PLDI, pp.213-223, 2005. ,

Dynamic logic, Handbook of Philosophical Logic, pp.497-604, 1984. ,

A Quick Tour of the VeriFast Program Verifier, Proceedings of the 8th Asian conference on Programming languages and systems, APLAS'10, pp.304-311, 2010. ,

DOI : 10.1007/978-3-642-17164-2_21

TRACER: A Symbolic Execution Tool for Verification, Proc. 24th international conference on Computer Aided Verification, CAV'12, pp.758-766, 2012. ,

DOI : 10.1007/978-3-642-31424-7_61

Symbolic execution and program testing, Communications of the ACM, vol.19, issue.7, pp.385-394, 1976. ,

DOI : 10.1145/360248.360252

Fast pattern matching in strings, SIAM Journal of Computing, vol.6, issue.2, pp.323-350, 1977. ,

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Logic, Rewriting, and Concurrency -Festschrift Symposium in Honor of José Meseguer, 2015. ,

DOI : 10.1007/978-3-319-23165-5_21

URL : https://hal.archives-ouvertes.fr/hal-01158941

CinK -an exercise on how to think in K, 2013. ,

Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, pp.123-160, 2007. ,

Program verification by coinduction, 2015. ,

Verification of Java Programs Using Symbolic Execution and Invariant Generation, LNCS, vol.2989, pp.164-181, 2004. ,

DOI : 10.1007/978-3-540-24732-6_13

A survey of new trends in symbolic execution for software testing and analysis, International Journal on Software Tools for Technology Transfer, vol.17, issue.2, pp.339-353, 2009. ,

DOI : 10.1007/s10009-009-0118-1

Practical, low-effort equivalence verification of real code, Proceedings of the 23rd international conference on Computer aided verification, pp.669-685, 2011. ,

Separation logic: A logic for shared mutable data structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02, pp.55-74, 2002. ,

Rewriting modulo SMT and open system analysis. In Rewriting Logic and Its Applications -10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, pp.247-262, 2014. ,

From Hoare Logic to Matching Logic Reachability, Proceedings of the 18th International Symposium on Formal Methods (FM'12), pp.387-402, 2012. ,

DOI : 10.1007/978-3-642-32759-9_32

One-path reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013. ,

Circular Coinduction: A Proof Theoretical Foundation, CALCO 2009, pp.127-144, 2009. ,

DOI : 10.1007/978-3-540-73859-6_25

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

Checking reachability using matching logic Also available as technical report http, OOPSLA, pp.555-574, 2012. ,

Language definitions as rewrite theories, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, p.48, 2015. ,

DOI : 10.1016/j.jlamp.2015.09.001

URL : https://hal.archives-ouvertes.fr/hal-00950775

An Introduction to Bisimulation and Coinduction A preliminary version of Chapter, 2012. ,

Inferring invariants by symbolic execution, CEUR Workshop Proceedings. CEUR-WS.org, 2007. ,

CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, ESEC/FSE-13, pp.263-272, 2005. ,

A rewriting logic approach to operational semantics, Information and Computation, vol.207, issue.2, pp.305-340, 2009. ,

DOI : 10.1016/j.ic.2008.03.026

? = ? 1 (??) = (? 1 ?)? and since ? ? µ(? 1 , ?), ? 1 ? ? =A ?. Hence, (? 1 ?)? ? =A ??, and since ? =A is the equality "=" in T , we have (? 1 ?)? = ??. Using the hypothesis var (?) ? var (? 1 , ? 2 ) = ? we obtain var (?) ? var (? 1 ) = ?, and since ? is the identity everywhere except perhaps on var (? 1 ) and ? ?? we obtain that ? and ? coincide on var (?); hence ,

from hypothesis (? , ?) |= ? 2 ? ? ? 1 ? ? ? 2 ? ? ? we obtain in particular ? |= ?. Using again the hypothesis var (?) ? var (? 1 , ? 2 ) = ? we obtain that that ? and ? coincide on var (?), hence, ? |= ? as well ,

we prove (?): (? , ?) |= ? 2 ? 2 ? ? 2 . We prove ? |= ? 2 by analogy with ? |= ? 1 ,

From (?) and (?) we get ? ? {?1 ? ? ? ?2} ? . Using that and (?) and Lemma 4.1, which says that symbolic execution steps forward-simulate concrete ones, we obtain that there exists ? such that ? ? s ?1 ? ? ? ?2} ? and (? , ?) |= ? . By definition of ? s , ? ? {?1 ? ? ? ?2} (?), which proves (? , ?) |= ? {?1 ? ? ? ?2} (?), i.e., ? ? ? {?1 ? ? ? ?2} (?) and the conclusion of the (?) inclusion follows. This completes the proof of the lemma for X, Y = ?. For the general case: ? {?1 ? ? ? ?2} (?) (?var (? 1 , ? 2 ))(? 1 ? (?X)? ? ?) =? ? ? 2 is, due to the variable disjointness hypothesis in the lemma, ML-equivalent to the formula (?X, var (? 1 , ? 2 ))(? 1 ? ? ? ?) =? ? ? 2 , i.e., to (?X)? {?1 ? ? ? ?2} (? ? ?). To conclude the proof we apply the identity ? = (?X)?, which holds for every ML formulas ? and set X ? Var of variables (which is a simple consequence of Def. 3.9 of the ML satisfaction relation), to the two members of the equality in the lemma's conclusion ,

?) iff ? ? ? (now interpreted as an ML formula in the signature of L) for some transition ? ? S s ? , which proves the theorem, Inria RESEARCH CENTRE LILLE ? NORD EUROPE Parc scientifique de la Haute-Borne 40 avenue Halley -Bât A -Park Plaza 59650 Villeneuve d'Ascq Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN, pp.249-6399 ,