Dorel Lucanu

Vlad Rusu
email: vlad.rusu@inria.fr

Andrei Arusoaie

A Generic Framework for Symbolic Execution: Theory and Applications

Keywords: symbolic execution, programming language, formal operational semantics, reachability logic, circular coinduction, program verification

We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the syntax and execution infrastructure of the language, a model interpreting the signature, and rewrite rules for the language's operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. A prototype implementation of our approach has been developed in K. We illustrate it on the symbolic analysis and deductive verification of nontrivial programs.

Introduction

Symbolic execution is a well-known program analysis technique introduced in 1976 by James C. King [START_REF] King | Symbolic execution and program testing[END_REF]. Since then, it has proved its usefulness for testing, verifying, and debugging programs. Symbolic execution consists in executing programs with symbolic inputs, instead of concrete ones, and it involves the processing of expressions containing symbolic values [START_REF] Păsăreanu | A survey of new trends in symbolic execution for software testing and analysis[END_REF]. The main advantage of symbolic execution is that it allows to reason about multiple Preprint submitted to Journal of Symbolic Computation concrete executions of a program, and its main disadvantage is the statespace explosion determined by decision statements and loops. Recently, the technique has found renewed interest in the formal-methods community due to new algorithmic developments and progress in decision procedures.

In this paper we address two foundational issues regarding the symbolic execution, namely its relationships with the formal definition of the language, for soundness, and with the program logics, for applications to program analysis and verification.

Description of the contribution. The main contribution of the paper is a formal, language-independent theory and tool for symbolic execution, based on a language's operational semantics defined by term rewriting 1 . On the theoretical side, we define symbolic execution as the application of rewrite rules in the semantics by derivation, a logical description of symbolic successors of a given set of states also symbolically represented as a logical formula in Matching Logic (ML) [START_REF] Roşu | Matching logic -extended abstract[END_REF]. We prove that the symbolic execution thus defined has properties ensuring that it is related to concrete program execution in a natural way:

Coverage: to every concrete execution there corresponds a feasible symbolic one; Precision: to every feasible symbolic execution there corresponds a concrete one;

where two executions are said to be corresponding if they take the same path, and a symbolic execution is feasible if the path conditions along it are satisfiable. Or, stated in terms of simulations: the feasible symbolic executions and the concrete executions of any given program mutually simulate each other.

We also show how a simple extension of our symbolic-execution approach results in a deductive system for proving programs with respect to Reachability Logic (RL) [START_REF] Ştefănescu | All-path reachability logic[END_REF] properties; RL is a language-independent program logic also used for defining language semantics, which has been shown to subsume existing language-dependent logics such as Hoare and Separation logics [START_REF] Roşu | From Hoare logic to matching logic reachability[END_REF][START_REF] Roşu | Checking reachability using matching logic[END_REF]. The proposed deductive system is proved to be sound by using a coinductive proof technique. It is shown to be a strict generalization of an approach we presented in [START_REF] Lucanu | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF], in the sense that the procedure for RL proposed there is a strategy of the proof system proposed here. Our 3-rule proof system is also substantially simpler that the original 8-rule proof system given in [START_REF] Ştefănescu | All-path reachability logic[END_REF]; the price to pay is the theoretical relative completeness property, which the original proof system has, whereas ours is not known to have. The proof system we propose is inspired from the circular coinduction proof technique [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF], applied in this paper to programming language definitions (whereas in [START_REF] Roşu | Circular coinduction -a proof theoretical foundation[END_REF] it is applied to proving observational equalities between possibly infinite data structures, e.g., streams). This was possible by defining an appropriate notion of derivative in the new context and by exploiting the common framework of induction and coinduction based on ground rules [START_REF] Sangiorgi | An Introduction to Bisimulation and Coinduction[END_REF]. We thus obtain an uniform and rigorous approach for both finite and infinite symbolic executions.

On the practical side, we present an implementation of the theory in a prototype implementation based on in K [START_REF] Roşu | An overview of the K semantic framework[END_REF], a framework dedicated to defining formal operational semantics of languages. Our current prototype is built on version 3.4 of K (https://github.com/kframework/k/releases/tag/v3.4) and enhances the previous one based on the language transformation [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF]. K is based on rewriting, hence, we formally prove that the derivation operation can be correctly implemented by applying certain modified rewrite rules (obtained by automatically transforming the original ones) over ML formulas. This additional intermediary step between abstract theory and implementation is important for ensuring that the resulting prototype tool adequately implements the theory, since the two extreme sides of our approach lie at quite distant levels of abstraction. We describe our prototype and demonstrate it on examples, which illustrate the bounded model checking of programs and their deductive verification with respect to RL formulas.

Related work.

There is a substantial number of tools performing symbolic execution available in the literature. However, most of them have been developed for specific programming languages and are based on informal semantics.

An approach closely related to ours is implemented in the MatchC tool [START_REF] Roşu | Onepath reachability logic[END_REF][START_REF] Roşu | Checking reachability using matching logic[END_REF], which has beed used for verifying challenging C programs such as the Schorr-Waite garbage collector. MatchC also uses the formalism of Reachability Logic for program specifications; the MatchC tool implementation, is, however, dedicated to a subset of C. The main difference with our approach is that we emphasise on bridging the gap between theory and implementation (from an initial, abstract definition of symbolic execution to its extension for program verification, then to its encoding by rewriting and finally to its implementation in code), whereas in the MatchC tool it does not focus on intermediary steps between theory (a language-independent deductive system) and code implementing it for a subset of C. The same comparison holds between our approach and [START_REF] Ştefănescu | All-path reachability logic[END_REF], in which a deductive system for a different version of RL is implemented for verifying programs written in a specific language. Since our approach of symbolic execution is founded on coinduction, it can also be seen as a bridge between the pure coinductive program verification techniques [START_REF] Moore | Program verification by coinduction[END_REF] and verification techniques based on operational semantics [START_REF] Ştefănescu | All-path reachability logic[END_REF][START_REF] Roşu | Onepath reachability logic[END_REF].

Java PathFinder [START_REF] Păsăreanu | Symbolic PathFinder: symbolic execution of Java bytecode[END_REF] is a complex symbolic execution tool which uses a model checker to explore different symbolic execution paths. The approach is applied to Java programs and it can handle recursive data structures, arrays, preconditions, and multithreading. Java PathFinder can access several Satisfiability Modulo Theories (SMT) solvers and the user can also choose between multiple decision procedures. The tools is fully dedicated to the Java language.

Another approach consists of combining concrete and symbolic execution into concolic execution. First, some concrete values given as input determine an execution path. When the program encounters a decision point, the paths not taken by concrete execution are explored symbolically. This has been implemented by several tools: DART [START_REF] Godefroid | DART: directed automated random testing[END_REF], CUTE [START_REF] Sen | CUTE: a concolic unit testing engine for C[END_REF], EXE [START_REF] Cadar | EXE: automatically generating inputs of death[END_REF], PEX [START_REF] De | Parameterized unit testing with Pex[END_REF]. We note that our approach allows mixed concrete/symbolic execution; it can be the basis for language-independent implementations of concolic execution.

There are several tools that check program correctness using symbolic execution. Some of them are more oriented towards finding bugs [START_REF] Cadar | Klee: unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF], while others are more oriented towards verification [START_REF] Coen-Porisini | Using symbolic execution for verifying safety-critical systems[END_REF][START_REF] Jaffar | Tracer: a symbolic execution tool for verification[END_REF][START_REF] David | Practical, low-effort equivalence verification of real code[END_REF]. Several techniques are implemented to improve the performance of these tools, such as bounded verification [START_REF] Clarke | Hardware verification using ANSI-C programs as a reference[END_REF] and pruning the execution tree by eliminating redundant paths [START_REF] Cui | Verifying systems rules using rule-directed symbolic execution[END_REF]. Other approaches offer support for verification of code contracts over programs. Spec# [START_REF] Barnett | The Spec# programming system: an overview[END_REF] is a tool developed at Microsoft that extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. A similar approach, which provides functionality for checking the correctness of a JAVA implementation with respect to a given UML/OCL specification, is the KeY [START_REF] Ahrendt | The KeY tool[END_REF] tool. In particular, KeY allows to prove that after running a method, its postcondition and the class invariant holds, using Dynamic Logic [START_REF] Harel | Dynamic logic[END_REF] and symbolic execution. The VeriFast tool [START_REF] Jacobs | A quick tour of the verifast program verifier[END_REF] supports verification of single and multi-threaded C and Java programs annotated with preconditions and postconditions written in Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. The Smallfoot tool [START_REF] Berdine | Symbolic execution with separation logic[END_REF] uses symbolic execution together with separation logic to prove Hoare triples. There are also approaches that attempt to automatically detect invariants in programs [START_REF] Păsăreanu | Verification of Java programs using symbolic execution and invariant generation[END_REF][START_REF] Peter | Inferring invariants by symbolic execution[END_REF]. The major advantage of most of these tools is that they perform very well, being able to verify substantial pieces of code, some of which are parts of actual safety-critical systems. On the other hand, they deal only with specific programs (e.g. written using subsets of C) and specific properties (e.g., allocated memory is eventually freed).

Regarding performance, our generic and formal tool is, quite understandably, not in the same league as existing pragmatic tools, which are dedicated to specific languages and are focused on specific applications of symbolic execution. We focus here on language-independence: given a programming language defined in an algebraic/rewriting setting, we build its symbolic semantics and use it for various analyses and verifications of programs in those languages. Symbolic execution in term-rewriting systems is another related work. The technique called narrowing, initially used for solving equation systems in ab-stract datatypes, was extended for solving reachability problems in termrewriting systems and was applied to the analysis of security protocols [START_REF] Meseguer | Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols[END_REF]. Such analyses rely on powerful unification-modulo-theories algorithms [START_REF] Escobar | Variant narrowing and equational unification[END_REF], which work well for security protocols since there are unification algorithms modulo the theories involved there (exclusive-or, . . . ). This is not always the case for programming languages, which have arbitrarily complex datatypes.

A recent evolution of symbolic execution in term-rewriting systems is rewriting modulo SMT [START_REF] Rocha | Rewriting modulo SMT and open system analysis[END_REF], in which terms are constrained with unquantified firstorder formulas over builtin sorts, and the constraints accumulated during termrewriting are handled by SMT solving. For non-builtin sorts unification modulo theories reduces (under technical conditions) to matching modulo theories. There are some similarities with our approach,e.g., they also obtain mutual simulations between symbolic and concrete rewriting. However, the unquantified constrained terms that [START_REF] Rocha | Rewriting modulo SMT and open system analysis[END_REF] can rewrite over are a subset of ML, hence, our approach, which handles the full ML logic, is more general.

Finally, there is the comparison with our own previous work on this topic. The conference paper [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF] presents our initial approach, and has since evolved into several directions. The present paper extends [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF] with the following features: more expressive language definitions (including configurations satisfying associativity and/or commutativity and/or unity (ACU) axioms, an essential feature in real languages definition in the K framework); a more expressive (and thus more precise) symbolic model (ML formulas vs. terms constrained with Boolean formulas); a more general presentation of symbolic execution (using the logical construction of derivatives, for which the approach based on language transformation of [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF] is only an implementation); and the RL-formula verification application of symbolic execution. We also systematically employ (co)induction in order to reason about possibly infinite program executions.

The paper [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF] expands another idea present in [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF], namely, language transformations for symbolic execution, for a different symbolic model (equivalence classes of ML formulas having the same semantics, which is in some sense the best possible model in terms of precision with respect to concrete program configurations). Language transformations techniques to compute for such a symbolic model are proposed in [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF]. Moreover, the paper [START_REF] Rusu | Language definitions as rewrite theories[END_REF] deals with the implementation of concrete and symbolic execution in programming languages using rewrite theories; precise and approximated implementations are proposed. While ML formulas as a precise symbolic model, and combination of ACU axioms, are considered in [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF][START_REF] Rusu | Language definitions as rewrite theories[END_REF], neither of those papers deal with RL formula verification, nor do they employ (co)induction as a systematic, rigorous technique for reasoning about possibly infinite program executions. RL formula verification is dealt with in [START_REF] Lucanu | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF], but the procedure for RL verification proposed there is only a a particular case of the proof system proposed here.

Paper organisation. After this introduction, Section 2 presents the CinK language, a kernel of the C ++ programming language. We shall use CinK programs for illustrating various aspects of symbolic execution. In Section 3 we present some background theoretical material used in the rest of the paper: coinduction, a general technique for defining and reasoning about possibly infinite objects such as program executions; reachability logic, which is used for defining operational semantics of languages and for stating program properties; and a generic language-definition framework, in order to make our approach independent of the K language-definition framework. Section 4 contains our formalisation of symbolic execution, including the coverage and precision results stated earlier in this introduction. Section 5 presents how reachability logic formulas can be verified using a coinductive extension of symbolic execution. In Section 6 we show how symbolic execution and its core derivative operation can be implemented in language definitions based on standard rewriting, such as the K framework. Section 7 presents a prototype tool based on the language transformations from the previous section, as well as applications of the tool for the symbolic execution, model checking, and deductive verification of nontrivial programs. We conclude in Section 8.

Example: the K Definition of the CinK language

In this section we present CinK [START_REF] Lucanu | CinK -an exercise on how to think in K[END_REF], a kernel of the C ++ programming language. The K definition of CinK used here is available on the K Framework Github repository, http://github.com/kframework/cink-semantics/ releases/tag/v1.0. As any K definition, it consists of the language's syntax, given using a BNF-style grammar, and of its semantics, given by means of rewrite rules.

In this paper we only exhibit a small part of the K definition of CinK, whose syntax is shown in Figure 1. Some of the grammar productions are annotated with K-specific attributes. The most important is the attribute strict that specifies that the arguments of the operator defined by the corresponding production are evaluated in a strict nondeterministic order before evaluating the operator itself. The attribute strict may have parameters, which are in fact sub-attributes. For instance, the sub-attribute context, which can be applied to a specified argument or to all arguments, may specify that the corresponding sub-expressions have to be evaluated as rvalues, by wrapping them with the semantic operator rvalue. Otherwise, the subexpressions are implicitly evaluated as lvalues (see, e.g., the syntax for the increment and decrement operators). The difference between the two kinds of evaluations can be observed in the rules giving semantics to the operators (Figure 3). Other attributes (funcall , divide, plus, minus, . . . ) are names associated to each syntactic production, which can be used to refer to them. Program states are described in K framework as configurations. A configuration is a nested structure of cells, specified using an XML-like notation. The (partial) configuration of CinK (Figure 2) includes the following cells:

Exp ::= Id | Int | ++ Exp [strict, prefinc] | --Exp [strict, prefdec] | Exp / Exp [strict(all (context(rvalue))), divide] | Exp + Exp [strict(all (context(rvalue))), plus] | Exp > Exp [strict(all (context(rvalue)))] Stmt ::= Exps ; [strict] | {Stmts} | while (Exp)Stmt | return Exp ; [strict(all (context(rvalue)))] | if (Exp)Stmt else Stmt [strict(1 (context(rvalue)))] Fig. 1. Fragment of CinK syntax $PGM k • env • store • stack • return • out cfg
cfg -the top cell that includes the other cells; k -containing the code that remains to be executed, which is represented as a list of sequential computation tasks C 1 C 2 . . .. Computation tasks are typically statements and expression evaluations; env -holding a map from variables to addresses (locations); store -holding a map from addresses to values); stack -storing function call stack; return -for the return values of functions; and out -holding the output of the program and is here connected to the standard output stream.

When the configuration is initialised at runtime a CinK program is loaded in the k cell and all the other cells remain empty. This is specified by the special variable $PGM in the cell k and the dot in the other cells.

The semantics of the syntactical constructs is given by K rules. A K rule is a topmost rewrite rule specifying transitions between configurations. Since usually only a small part of the configuration is changed by a rule, a configuration abstraction mechanism is used, allowing one to only specify the parts transformed by the rule. For instance, the (abstract) rule for addition, shown in

I 1 + I 2 ⇒ ⇒ ⇒ I 1 + Int I 2 [plus] I 1 / I 2 ∧ I 2 = Int 0 ⇒ ⇒ ⇒ I 1 / Int I 2 [division] ++lval( L ) ⇒ ⇒ ⇒ lval( L ) ••• k ••• L → (V ⇒ ⇒ ⇒ V + Int 1) ••• store [inc] --lval( L ) ⇒ ⇒ ⇒ lval( L ) ••• k ••• L → (V ⇒ ⇒ ⇒ V -Int 1) ••• store [dec] lval( L )= V ⇒ ⇒ ⇒ V ••• k ••• L → _ ⇒ ⇒ ⇒ V ••• store ••• cfg [update] if( true ) St else _ ⇒ ⇒ ⇒ St [if-true] if( f alse ) _ else St ⇒ ⇒ ⇒ St [if-false] while( B ) St ⇒ ⇒ ⇒ if( B ){ St while( B ) St else {}} [while] V ; ⇒ ⇒ ⇒ • [instr-expr ] { Sts } ⇒ ⇒ ⇒ Sts [block ] X ⇒ ⇒ ⇒ lval (L) ••• k ••• X → L ••• env [lvalue] rvalue (lval (L : Loc) ⇒ ⇒ ⇒ $lookup (L)) [rvalue] $lookup( L ) ⇒ ⇒ ⇒ V ••• k ••• L → V ••• store ••• cfg [lookup]
I 1 + I 2 C k E env S store T stack V return O out cfg ⇒ ⇒ ⇒ I 1 + Int I 2 C k E env S store T stack V return O out cfg (1)
where + Int is the mathematical operation for addition, I 1 , I 2 , V are integers, E and S are maps, and T and O are lists. The rules for the other binary arithmetic operators are similar, excepting the rule for division that has a side condition which restricts its application. The increment and update rules have side effects in the store cell, modifying the value stored at a specific address.

We briefly describe the rules for the statements. The semantics of the conditional statement if is given by two corresponding rules, one for each possible evaluation of the condition expression. The rule giving semantics to the while loop performs an unrolling into an if statement. This unrolling process does not generate infinite rewritings because the rule can be applied only when the statement while is on top of the cell k. The rules giving semantics to the expression and block statements are self-explaining.

The last rules evaluate the program variables as lvalues and give semantics to the rvalue wrapper introduced by the sub-attribute context, respectively. The auxiliary construct $lookup is used is also used in other rules, not included in the paper.

The semantics of the attribute strict is given by so-called heating and cooling rules, which are automatically generated. We show the case of addition:

A 1 + A 2 ⇒ ⇒ ⇒ rvalue(A 1 ) + A 2 A 1 + A 2 ⇒ ⇒ ⇒ rvalue(A 2 ) A 1 + rvalue(I 1 ) + A 2 ⇒ ⇒ ⇒ I 1 + A 2 rvalue(I 2 ) A 1 + ⇒ ⇒ ⇒ A 1 + I 2
where is a special symbol, destined to receive the result of an evaluation.

Example 2.1 The CinK program gcd from Figure 4 computes the greatest common divisor of two non-negative numbers using Euclid's algorithm. We use it as an example to illustrate symbolic execution and program verification.

x = a; y = b; while (y > 0){ r = x % y; x = y; y = r; } In this section we present some theoretical material used in the rest of the paper: induction and coinduction (Section 3.1), a general technique for reasoning about finite and possibly infinite objects such as program executions; reachability logic (Section 3.2), which is used for defining operational semantics of languages and for stating program properties; and language definitions (Section 3.3), which captures the essence of language definition frameworks such as K. We note that Sections 3.1 and 3.2 adapt material from the literature ( [START_REF] Sangiorgi | An Introduction to Bisimulation and Coinduction[END_REF] and [START_REF] Ştefănescu | All-path reachability logic[END_REF], respectively) and Section 3.3 also reuses some of our own [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF][START_REF] Lucanu | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF].

(Co)induction

In this section we present some material on coinduction, which we intensively use in the rest of the paper. Most of the material is adapted from [START_REF] Sangiorgi | An Introduction to Bisimulation and Coinduction[END_REF]. Coinduction is dual to induction, a perhaps better-known reasoning technique, which we also use in a few instances hereafter; we thus present them together.

The common framework for induction and coinduction is generally given using lattice theory, but here we consider only the particular case of powerset lattices, where the partial order is given by inclusion. Let U be a set and P(U) its powerset (the set of all subsets of U). A function F : P(U) → P(U) is monotone if F (X) ⊆ F (Y ) whenever X ⊆ Y , for all X, Y ∈ P(U). Given a function F : P(U) → P(U), an element X ∈ P(U) is a fixed point of F if F (X) = X. If X is the least element (or greatest element) in the set of fixed points of F then X is called the least fixed point (or greatest fixed point, respectively) of F . The following result is an instance of a more general one known as Knaster-Tarski Theorem: Theorem 3.1 Let U be a set and P(U) its powerset. Any monotone function F : P(U) → P (U) has a least fixed point µ Y. F (Y ) (abbreviated as µ F ) and a greatest fixed point ν Y. F (Y ) (abbreviated as ν F ). Moreover,

µ F = {X | F (X) ⊆ X} and ν F = {X | X ⊆ F (X)}.
Definition 3.1 Let U be a set and F : P(U) → P (U) be a monotone function. Then µ F is the set inductively defined by F and ν F is the set coinductively defined by F .

A function

F : P(U) → P(U) is continuous if F ( n≥0 X n ) = n≥0 F (X n ) for any increasing chain X 0 ⊆ X 1 ⊆ • • • , and F is cocontinuous if F ( n≥0 X n ) = n≥0 F (X n ) for any decreasing chain X 0 ⊇ X 1 ⊇ • • • .
The following result, which is an instance of Kleene's Theorem, shows how the least fixed point and the greatest fixed point can be computed when F is (co)continuous. Theorem 3.2 If F : P(U) → P(U) is continuous then µ F = n≥0 F n (∅). If F : P(U) → P(U) is cocontinuous then ν F = n≥0 F n (U). Theorem 3.1 suffices for the purposes of this paper, Theorem 3.2 being used only for some particular examples. We often use the case when the function F : P(U) → P(U) is defined by a set of inference rules. Definition 3.2 Let U be a set. A ground inference rule on U is a pair (S, x), where S ⊆ U, x ∈ U. A set R of ground rules yields a function R : P(U) → P(U) given by R(X) = {x | (∃S ⊆ X)(S , x) ∈ R}.

If S = {x 1 , x 2 , . . .}, then a rule (S, x) is written as

x 1 x 2 . . . x
The function R associated to a set of ground rules R is monotone. It follows that each set of ground rules R inductively defines a set µ R and coinductively defines a set ν R.

A particular case when R is (co)continuous is given by the following result.

Proposition 3.1 Let R be a set of ground rules. If for any (S, x) ∈ R, S is finite, then R is continuous. If for any x, the set {S | (S, x) ∈ R} is finite, then R is cocontinuous.

Example 3.1 The system LIST, given below, coinductively defines the possibly infinite lists over integers:

[A] nil [B] z, z ∈ Z
Let U be any set including all (finite and infinite) strings over Z ∪ {nil , , }.

Note that [B] is a rule scheme; the ground rules are obtained by instantiating z and with concrete integers and elements in U, respectively. We have

LIST(X) = {z, | z ∈ Z, ∈ X} ∪ {nil }.
The set of possibly infinite (i.e., finite and infinite) lists is the greatest fixed point, Z ∞ = ν LIST. We obtain

Z ∞ = U ∩ LIST(U) ∩ LIST 2 (U) ∩ . . . = U ∩ ({z 1 , u | z 1 ∈ Z, u ∈ U} ∪ {nil }) ∩ ({z 1 , z 2 , u | z 1 , z 2 ∈ Z, u ∈ U} ∪ {z 1 , nil | z 1 ∈ Z} ∪ {nil }) ∩ . . . by
Z ω = ∅ ∪ LIST(∅) ∪ LIST 2 (∅) ∪ . . . = ∅ ∪ {nil } ∪ ({z 1 , nil | z 1 ∈ Z} ∪ {nil }) ∪ ({z 2 , z 1 , nil | z 1 , z 2 ∈ Z} ∪ {z 1 , nil | z 1 ∈ Z} ∪ {nil }) ∪ . . .
We now give the induction and coinduction principles, which can be used for reasoning about inductively, resp. coinductively defined sets: Proposition 3.2 (Induction proof principle) Let U be a set and F : P(U) → P (U) be a monotone function. Then

F (X) ⊆ X µ Y. F (Y ) ⊆ X
We shall be using this principle with F R for a set R of rules. The principle says that if, for a given X, for all rules (S, x) ∈ R, S ⊆ X implies x ∈ X, then (the set inductively defined by the rules) ⊆ X. A set X satisfying F (X) ⊆ X is called forward closed w.r.t. F . Example 3.2 In order to show that the finite list over integers satisfy a property p( ), it is enough to prove that the set

{ | p( )} is forward closed, i.e., {z, | z ∈ Z and p( )} ∪ {nil } ⊆ { | p( )}.
The coinduction proof principle is dual to the induction principle: Proposition 3.3 (Coinduction proof principle) Let U be a set and F : P(U) → P (U) be a monotone function. Then

X ⊆ F (X) X ⊆ ν Y. F (Y )
We also use the coinduction proof principle with F R for a set R of rules. The principle now says that if, for a given X, for all x ∈ X there is a rule (S, x) ∈ R with S ⊆ X, then X ⊆ (the set coinductively defined by the rules). A set X satisfying X ⊆ F (X) is called backward closed w.r.t. F .

Example 3.3 We consider the lists over integers again. Let

f : U → U be a function. If we want to show that f (u) is a list for each u ∈ U, it is sufficient to prove that the set {f (u) | u ∈ U} is backward closed, i.e., {f (u) | u ∈ U} ⊆ {z, f (u) | z ∈ Z, u ∈ U} ∪ {nil}.
For the specific case of coinductively defined sets we shall use the fact that membership in such a set amounts to the existence of a certain proof tree: Definition 3.3 (Proof Trees) Let R be a set of ground rules over U and x ∈ U. A (finite or infinite) tree T is a proof tree of x under R if it satisfies the following properties:

• the root of T is labelled with x;

• if y is the label of a node of T and S is the set of labels of the children of this node, then (S, y) ∈ R.

We often refer the nodes of a proof tree T by their labels. Note that a proof tree can be finite or infinite.

Proposition 3.4 Let R be a set of a set of ground rules over U such that R is cocontinuous. Then

x ∈ µ R iff there is a well-founded proof tree of x under R and x ∈ ν R iff there is a proof tree of x under R.

Example 3.4

We have 3, 8, nil ∈ ν LIST because there is the following wellfounded proof tree under LIST:

[A] nil [B] 8, nil [B] 3, 8, nil
Note that the rule labels are not part of the tree, they are added to emphasise what rule is applied for each node in the tree. We also have that the infinite list 1, 0, 1, 0, 1, 0, . . . is in ν LIST since there is the following infinite tree under LIST:

. . . [B] 1, 0, 1, 0, 1, 0, . . . [B] 0, 1, 0, 1, 0, 1, . . . [B] 1, 0, 1, 0, 1, 0, . . .
In general, for an element in ν R (or µ R) there may exist more than one proof tree. In [START_REF] Sangiorgi | An Introduction to Bisimulation and Coinduction[END_REF] games and strategies are used for finding specific proof trees. Here we use the proof trees to define functions on sets (co)inductively defined, i.e., functions of the form f : A → B, where A ∈ {µ R, ν R} and B ∈ {µ R, ν R}.

According to [START_REF] Moss | On the foundations of corecursion[END_REF], the functions with A = µ R for some R are called recursive, and the functions with B = ν R for some R are called corecursive. Such functions can be easily defined (specified) using rules (schemes). We assume that R is defined over U and R over U . A partial proof tree (under R ) is a tree t with nodes labeled with elements in U that can be extended to a proof tree. Let f be a function that sends each rule in R into a partial proof tree under R . This function can be easily extended to proof trees, so we may consider that f (a) = b if the f sends the proof tree of a ∈ A into the proof tree of b ∈ B. Note that each of these proof trees could be finite (for both inductive and coinductive cases) or infinite (only for the coinductive case).

Here is an example. Let NAT be the set of rules

0 x s(x)
Then ν NAT is the set of extended natural numbers N ∪ {∞}. The function size : ν LIST → ν NAT associating to a list its size can be defined by size(nil ) = 0, meaning that the it maps the rule nil into the partial tree (that is also a rule in this case) 0 , and size(z, ) = s(size( )), meaning that the it maps the rule z, into the partial tree size( ) s(size( ))

. It is interesting that the version for finite lists, size : µ LIST → µ NAT, is specified in the same way. Therefore it is important to mention which sets the function is defined on.

Matching Logic and Reachability Logic

This section is dedicated to presenting the logics that we use in the paper: matching logic and reachability logic. There are several versions of these recently introduced logics, of which we chose those presented in [START_REF] Ştefănescu | All-path reachability logic[END_REF].

We start with some notions on algebraic specifications and first-order logic.

A many-sorted algebraic signature Σ consists of a set S of sorts and of a set of S * × S-sorted set of function symbols. Let T Σ denote the Σ-algebra of ground terms and T Σ,s denote the set of ground terms of sort s. Given a sort-wise infinite set of variables Var , let T Σ (Var ) denote the free Σ-algebra of terms with variables, T Σ,s (Var ) denote the set of terms of sort s with variables, and var (t) denote the set of variables occurring in the term t. For terms t 1 , . . . , t n we let var (t 1 , . . . , t n ) denote the set var

(t 1 ) ∪ • • • var (t n ).
For any substitution σ : Var → T Σ (Var ) and term t ∈ T Σ (Var ) we denote by tσ the term obtained by applying the substitution σ to t. We use the diagrammatical order for the composition of substitutions, i.e., for substitutions σ and σ , the composition σσ consists in first applying σ then σ . Let T be a Σ-algebra. Any valuation ρ :

Var → T is extended to a (homonymous) Σ-algebra morphism ρ : T Σ (Var ) → T .
The interpretation of a ground term t in T is denoted by T t . For simplicity, we often write true, false, 0, 1, . . . instead of T true , T false , T 0 , T 1 , . . . etc.

φ ::= | p(t 1 , . . . , t n ) | ¬φ | φ ∧ φ | (∃X)φ
where p ranges over predicate symbols Π, t i range over Σ(Var )-terms, and X over finite subsets of Var . Given a (Σ, Π)-formula φ, a (Σ, Π)-model model T , and ρ : Var → T , the satisfaction relation ρ |= φ is defined as follows:

(1)

ρ |= ; (2) ρ |= p(t 1 , . . . , t n ) iff (t 1 ρ, . . . , t n ρ) ∈ T p ; (3) ρ |= ¬φ iff ρ |= φ; (4) ρ |= φ 1 ∧ φ 2 iff ρ |= φ 1 and ρ |= φ 2 ; and (5) ρ |= (∃X)φ iff there is ρ with xρ = xρ, for all x ∈ X, such that ρ |= φ. A formula φ is valid (in T ), denoted by |= φ, if it is satisfied by all valuations.
The other first-order formulas (including disjunction, implication, equivalence, universal quantifiers,. . . ) are defined as syntactical sugar in the usual way.

Matching Logic

We next recall the syntax and semantics of matching logic (ML) [START_REF] Roşu | Matching logic -extended abstract[END_REF] and reachability logic (RL) [START_REF] Ştefănescu | All-path reachability logic[END_REF]. ML is a static logic of configurations, whereas RL is a dynamic logic of configurations, expressing their evolution over time.

Here we consider only the topmost version of ML. RL can be used both for specifying the operational semantics of programs (e.g., the rules in Fig. 3 denote RL formulas) and as a program-specification formalism.

Definition 3.5 (ML signature) An ML signature is a triple Φ = (Σ, Π, Cfg), where (Σ, Π) is a many-sorted first-order signature and Cfg is a distinguished sort in Σ for configurations. The set of ML formulas over Φ is defined by

ϕ ::= π | | p(t 1 , . . . , t n ) | ¬ϕ | ϕ ∧ ϕ | (∃V )ϕ
where π ranges over T Σ,Cfg (Var ), p ranges over predicate symbols Π, each t i ranges over T Σ (Var ) of appropriate sorts, and V over finite subsets of Var .

Definition 3.6 (Basic, Elementary, Quantified Elementary Patterns) Let Φ = (Σ, Π, Cfg) be an ML signature. A basic pattern is a term π ∈ T Σ,Cfg (Var ). An elementary pattern is an ML formula of the form π ∧ φ, where π is a basic pattern and φ is a Φ-formula, called the condition of the elementary pattern. A quantified elementary pattern is an ML formula of the form (∃X)π ∧ φ with X ⊂ Var and π ∧ φ an elementary pattern. We identify basic patterns π with corresponding elementary patterns π ∧ true and with quantified elementary patterns (∃∅)π ∧ φ.

A basic pattern π thus defines a set of (concrete) configurations, and the condition φ gives additional constraints these configurations must satisfy. If present, existentially quantified variables are used to abstract away some details from the pattern. Examples of CinK patterns are the basic pattern

I 1 + I 2 C k E env S store T stack R return O out cfg
and the elementary pattern

I 1 / I 2 C k E env S store T stack Rt return O out cfg ∧ I 2 = Int 0
An example of a CinK quantified elementary pattern is given below; it will occur in the sequel and its meaning will be explained at the appropriate place: Hereafter we fix an ML signature Φ = (Σ, Π, Cfg) and a model T for it. The following encoding of ML into FOL will be used in the rest of the paper.

(∃l, g) • k (x → l)E env (l → g)S store cfg ∧ g = gcd (
Definition 3.9 (FOL encoding of ML [START_REF] Ştefănescu | All-path reachability logic[END_REF]) If ϕ is an ML formula then ϕ =? is the FOL formula (∃z)ϕ , where ϕ is obtained from ϕ by replacing each basic pattern occurrence π with z = π, and z is a variable that does not occur in ϕ.

Example 3.5 Here are a few examples of ML formulas and their FOL encodings:

ϕ ϕ =? (π 1 ∧ φ 1 ) ∨ (π 2 ∧ φ 2 ) (∃z)((z = π 1 ∧ φ 1 ) ∨ (z = π 2 ∧ φ 2 )) ¬π (∃z)¬(z = π) π 1 ∧ ¬π 2 (∃z)((z = π 1 ) ∧ ¬(z = π 2 )) π ∨ ¬π (∃z)(z = π ∨ ¬(z = π))
The relationship between ML formulas and their FOL encodings is now given.

Proposition 3.5 ( [START_REF] Ştefănescu | All-path reachability logic[END_REF]) Let ϕ be an ML formula and ρ : Var → T . Then ρ |= ϕ =? iff there is γ such that (γ, ρ) |= ϕ.

Reachability Logic

Definition 3.10 An RL formula is a pair of ML formulas ϕ 1 ⇒ ⇒ ⇒ ϕ 2 .

The following example illustrates RL as a program-specification formalism.

Example 3.6 Consider the program gcd from Figure 4. The following RL formula

gcd k a → l 1 b → l 2 ••• env l 1 → a l 2 → b ••• store ••• cfg ∧ a ≥ 0 ∧ b ≥ 0 ⇒ ⇒ ⇒ (∃l, g) • k (x → l) ••• env (l → g) ••• store ••• cfg ∧ g = gcd (a,b) (2)
specifies that finite complete executions of the program gcd from configurations where the program variables a, b are bound to non-negative values a, b reach configurations where x is bound to a location l where an integer value g such that g = gcd (a, b) is stored. Here, gcd () is a mathematical definition of the greatest-common-divisor operation (with gcd (0, 0) = 0 by convention).

Also by convention the indices from data-domain predicates such as ≥ Int are dropped to simplify the presentation, and variables occurring in both left and right-hand sides of a formula, but are irrelevant to the formula's meaning, are replaced by ellipses (e.g., the rest of the store and environment cells).

RL formulas are interpreted over transition systems generated by language definitions. Next, we introduce that concept and give the semantics of RL.

Language Definitions

Our symbolic-execution approach is independent of the formal framework used for defining languages as well as from the languages being defined. We thus use a general notion of language definition based on algebraic specification and rewriting.

A language definition is a triple L = (Φ, T , S), where

• Φ is an ML signature (Σ, Π, Cfg) giving syntax to the language's execution infrastructure (called configuration). Cfg is the sort for configurations. • A Φ-Model T . Recall that T s denote the elements of the model T that have the sort s, in particular, the elements of T Cfg are called configurations. • A set S of RL formulas, defining the operational semantics of the language.

In the rest of the paper we shall also be using a fragment of the CinK language (shown in Section 2), called while, whose definition is simpler and therefore is easier to use for small yet illustrative examples. The syntax of while consists only of expressions, assignments, sequences and blocks of statements, and while loops. For simplicity, the configuration for while consists of only two cells k and env which contain the program to be executed, and respectively, a map from program variables to their values: Pgm k Map env cfg . The semantics of expressions in while is given using the same rules as in CinK. However, we choose a slightly different semantics for some statements, namely for assignment and lookup (due to the new configuration structure), and for the while loop:

X ••• k ••• X → I ••• env ⇒ ⇒ ⇒ I ••• k ••• X → I ••• env [while_lookup] X = I ; ••• k ••• X → _ ••• env ⇒ ⇒ ⇒ ••• k ••• X → I ••• env [while_assign] while( E ) S ••• k σ env ∧ σ[E] = Bool false ⇒ ⇒ ⇒ ••• k σ env [while_true] while( E ) S ••• k σ env ∧ σ[E] = Bool true ⇒ S while( E ) S ••• k σ env [while_false]
The while loop statement has two corresponding rules in the semantics, one for each possible evaluation of the condition E: if the evaluation of the condition

E in state σ, denoted σ[E]
, is true, then execute once the body of the loop and the loop again; otherwise, continue executing the rest of the program. The definition of while exhibits the flexibility of the K Framework to define the semantics of a language in various styles.

We now show how while fits into our notion of language definition. The ML signature (Σ, Π, Cfg) corresponding to while contains all the sorts and operations defined in its syntax. Nonterminals in the syntax are sorts and syntax productions are operations. For instance, Σ includes a sort for expressions Exp and its corresponding operations, e.g., _+_: Exp × Exp → Exp, _/_: Exp × Exp → Exp, etc. The ML signature also contains a sort Cfg for configurations, which has a unique constructor Stmt × Map → Cfg denoted by _ k _ env cfg (the occurrences of the symbol _ show the places of the arguments). The model T interprets all the constants and operations from the signature. By T 1 and T true we denote the interpretation of the constant symbols 1 and true. The set S of RL formulas contains the rules shown above (for assignment, lookup, and while), the rules corresponding to expressions from Figure 3, and rules generated by K from strictness annotations.

Language definitions generate execution paths obtained by applying rules in S to configurations in T Cfg . We give the relevant definitions using coinduction.

Notation We write γ 1 ⇒ ρ S γ 2 iff there exists ϕ 1 ⇒ ϕ 2 ∈ S and a renaming σ of the variables in ϕ 1 ⇒ ϕ 2 such that (γ i , σρ) |= ϕ i , i = 1, 2, and γ ⇒ S γ iff there is ρ such that γ 1 ⇒ ρ S γ 2 .
Definition 3.11 (Execution Paths) Let (Φ, T , S) be a language definition. The set of execution paths (τ, ρ) is coinductively defined by the following set of rules:

(γ, ρ) (τ, ρ) (γ 0 ⇒ S τ, ρ) γ 0 ⇒ ρ S hd (τ )
where γ ∈ T Cfg and ρ : Var → T , and hd is coinductively defined by

hd (γ) = γ hd (γ 0 ⇒ S τ ) = γ 0 We say that (τ, ρ) starts from ϕ if (hd (τ ), ρ) |= ϕ.
Note that this set of rules is akin to the one for lists (shown in Example 3.1); an execution path can be seen as a list of concrete configurations, where every two consecutive elements γ and γ satisfy γ ⇒ ρ S γ . The largest set satisfied by these rules is the set of all finite and infinite execution paths.

Example 3.7 Let ρ : Var → T be a valuation such that Xρ = x and Iρ = 2, where X and I are variables from the assignment rule for while. Then

x = 2; k x → 3 env cfg ⇒ S • k x → 2 env cfg
is a (finite) execution path obtained using the rules from Definition 3.11. Execution paths can be infinite too, e.g.,

τ while(true) x=1; k x → 0 env cfg ⇒ S x=1;while(true) x=1; k x → 0 env cfg ⇒ S while(true) x=1; k x → 1 env cfg ⇒ S x=1;while(true) x=1; k x → 1 env cfg ⇒ S while(true) x=1; k x → 1 env cfg ⇒ S • • •
which is obtained by applying the rules for while and assignment repeatedly.

Remark 3.1 The above definition for execution paths is not quite standard since it includes a fixed valuation ρ. A more natural definition is

γ τ γ 0 ⇒ S τ γ 0 ⇒ S hd (τ )
Recall that the variables occurring in rules can be renamed when they are used in execution steps (see the notation preceding Definition 3.11) and hence for each execution path γ 0 ⇒ S γ 1 ⇒ S • • • , defined by the above rules, there is a valuation ρ and the execution path (γ 0 , ρ) ⇒ S (γ 1 , ρ) ⇒ S • • • defined by Definition 3.11. We preferred the version with a fixed valuation since it simplifies many proofs.

We shall also be needing the following two notions. A configuration is irreducible if there is no transition outgoing from it: Definition 3.12 (Irreducible Configurations) Let (Φ, T , S) be a language definition. We say that γ ∈ T Cfg is irreducible iff there is no γ such that γ ⇒ S γ .

An execution path is complete if either it is finite and ends up in an irreducible configuration, or it is infinite.

Definition 3.13 (Complete Execution Paths) Let (Φ, T , S) be a language definition. The set of complete execution paths is coinductively defined by the following set of rules:

(γ, ρ) γ irreducible (τ, ρ) (γ 0 ⇒ S τ, ρ) γ 0 ⇒ ρ S hd (τ ) Example 3.8 Recall γ • k x → 2 env
cfg from the previous example. Then, γ is irreducible because there is no rule in the semantics of while that can be applied to it. Another example of irreducible configuration is

γ 10/0 k x → 2 y → 1 env cfg .
Since the side condition of division rule does not hold in this case, the rule cannot be applied and thus, there are no successors for γ .

From γ irreducible we obtain that any path γ ⇒ S γ is complete. Note that infinite execution paths are complete as well; for instance, the infinite path τ from Example 3.7 is complete.

Next, we define the notion of derivative of ML and RL formulas needed to define semantics of RL and symbolic execution (in Section 4). We shall see in Section 4 that this rather technical definition encodes the set of all concrete successors of configurations that satisfy a given ML formula. In Section 6 we shall also see that it amounts (under reasonable conditions) to standard rewriting with a modified set of rules.

Definition 3.14 (Derivatives for ML and RL Formulas)

If ϕ is an ML formula then ∆ S (ϕ) {(∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ) =? ∧ ϕ r | ϕ l ⇒ ⇒ ⇒ ϕ r ∈ S}. If ϕ ⇒ ⇒ ⇒ ϕ is an RL formula then ∆ S (ϕ ⇒ ⇒ ⇒ ϕ ) {ϕ 1 ⇒ ⇒ ⇒ ϕ | ϕ 1 ∈ ∆ S (ϕ)}.
Example 3.9 Let ϕ X =I ; C k X → V M env cfg be an ML formula and ϕ l ⇒ ⇒ ⇒ ϕ r be the RL formula corresponding to assignment in while:

X=I; C k X → V M env cfg ⇒ ⇒ ⇒ C k X → I M env cfg
The derivative ϕ ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ) specifies the configurations obtained from those satisfying the initial formula ϕ after executing the assigment rule:

ϕ (∃var (ϕ l , ϕ r )) ϕ l ∧ ϕ =? ∧ ϕ r = (∃X, I, C, V, M ) X = I; C k X → V M env cfg ∧ X = I ; C k X → V M env cfg =? ∧ C k X → I M env cfg = (∃X, I, C, V, M )(∃z) z = X = I; C k X → V M env cfg ∧ z = X = I ; C k X → V M env cfg ∧ C k X → I M env cfg = (∃X, I, C, V, M ) X = I; C k X → V M env cfg = X = I ; C k X → V M env cfg ∧ C k X → I M env cfg which simplifies to ϕ = C k X → I M env cfg
using the fact that the equality

X = I; C k X → V M env cfg = X = I ; C k X → V M env cfg implies X = X , I = I , C = C , M = M , and V = V .
That is, after performing the assignment of X = I , X is bound to I in the environment.

In the paper we use the notions of S-derivability of an ML formula ϕ (also extended to RL formulas ϕ ⇒ ⇒ ⇒ ϕ ), and totality of a set S of RL formulas:

Definition 3.15 (S-derivability) An ML formula ϕ is S-derivable if ∆ S (ϕ) is satisfiable. An RL formula ϕ ⇒ ⇒ ⇒ ϕ is S-derivable if ϕ is S-derivable.
Example 3.10 Recall ϕ, ϕ and ϕ l ⇒ ⇒ ⇒ ϕ r from Example 3.9. The ML formula ϕ is S-derivable since ϕ

∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ)(∈ ∆ S (ϕ)) is satisfiable (we have γ ∈ ϕ , where γ • k x → 2 env cfg ).
On the other hand, the ML formula ϕ = I 1 /I 2 ;

C k E env cfg ∧I 2 = Int 0 is not S-derivable. In fact, for any rule ϕ l ⇒ ⇒ ⇒ ϕ r ∈ S, the derivative ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} ( ϕ) is not satisfiable. For example, let ϕ l ⇒ ⇒ ⇒ ϕ r be the division rule:

I 1 /I 2 C k E env cfg ∧ I 2 = Int 0 ⇒ ⇒ ⇒ I 1 / Int I 2 C k E env cfg
The derivative ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} ( ϕ) is:

(∃I 1 , I 2 , C, E) I 1 /I 2 C k E env cfg = I 1 /I 2 ; C k E env cfg ∧ I 2 = Int 0 ∧ I 2 = Int 0 ∧ I 1 / Int I 2 C k E env cfg ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} ( ϕ)
is not satisfiable because there is no I 2 which simultaneously satisfies

I 2 = I 2 (implied by I 1 /I 2 C k E env cfg = I 1 /I 2 ;
C k E env cfg ), I 2 = Int 0, and I 2 = Int 0. Definition 3.16 (Totality) A set S of RL formulas is total iff for each Sderivable ϕ and each (γ, ρ) such that (γ, ρ) |= ϕ, there is γ 1 such that γ ⇒ S γ 1 .

Note the difference between S-derivability and totality: S-derivability requires to have at least one transition starting from ϕ and the totality requires to have at least one transition starting from γ for any model (γ, ρ) of ϕ.

Remark 3.2

The semantics of CinK is not total because of the rules for division and modulo. The rule for division:

I 1 / I 2 ••• k ••• cfg ∧ ∧ ∧ I 2 = 0 ⇒ ⇒ ⇒ I 1 / Int I 2 ••• k ••• cfg
does not meet the condition of Definition 3.16 because of the condition I 2 = 0 which restricts the application of the rule. The semantics can be made total by adding a rule

I 1 / I 2 ••• k ••• cfg ∧ ∧ ∧ I 2 = 0 ⇒ ⇒ ⇒ error ••• k ••• cfg that
leads divisions by zero into "error" configurations. In this way, for any γ which is an instance of

I 1 / I 2 ••• k ••• cfg
there is at least one rule in the semantics which can be applied.

We assume hereafter that the CinK semantics (and implicitly that of while) has been transformed as above.

We can now define the semantics of RL, in a different, yet equivalent manner to the original definition given in [START_REF] Ştefănescu | All-path reachability logic[END_REF]. Again, we are using coinduction: Definition 3.17 (Semantics of RL) Let (τ, ρ) be an execution path and ϕ ⇒ ⇒ ⇒ ϕ an RL formula. We say that (τ, ρ) satisfies ϕ ⇒ ⇒ ⇒ ϕ and we write [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF], where (3, 4) is the system of ground rules:

(τ, ρ) |= ϕ ⇒ ⇒ ⇒ ϕ if (τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ ∈ ν (3,
(τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ (hd (τ ), ρ) |= ϕ ∧ ϕ (3) (τ, ρ), ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ ⇒ ⇒ ⇒ ϕ ) (γ 0 ⇒ S τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ (γ 0 , ρ) |= (ϕ l ∧ ϕ), ϕ l ⇒ ⇒ ⇒ ϕ r ∈ S (4)
S |= ϕ ⇒ ⇒ ⇒ ϕ iff (τ, ρ) |= ϕ ⇒ ⇒ ⇒ ϕ for each complete (τ, ρ) starting from ϕ. If F is a set of RL formulas then S |= F iff S |= ϕ ⇒ ⇒ ⇒ ϕ for each ϕ ⇒ ⇒ ⇒ ϕ ∈ F . We let ϕ ⇒ ⇒ ⇒ ϕ {τ | (∃ρ)(τ, ρ) |= ϕ ⇒ ⇒ ⇒ ϕ } and F = ϕ ⇒ ⇒ ⇒ ϕ ∈F ϕ ⇒ ⇒ ⇒ ϕ .
Example 3.11 According to Example 3.9 and Example 3.10 we obtain

( x = 2; k x → 3 env cfg ⇒ S • k x → 2 env cfg , ρ) |= X =I ; C k X → V M env cfg ⇒ ⇒ ⇒ C k X → I M env cfg
with ρ : Var → T a valuation such that X ρ = x, I ρ = 2, C ρ = •, and V ρ = 3.

Symbolic Execution

In this section we present a symbolic execution approach for languages defined using the language-definition framework presented in the previous section. We prove that the transition system generated by symbolic execution forwardsimulates the one generated by concrete execution, and that the transition system generated by concrete execution backward-simulates the one generated by symbolic execution (restricted to satisfiable patterns). These properties are the naturally expected ones from a symbolic execution framework. They allow to perform analyses on symbolic programs, and to transfer the results of those analyses to concrete instances of the symbolic programs in question.

We consider given a language definition L = (Φ, T , S), with Φ = (Σ, Π) and Cfg the sort for configurations. Since our goal is to relate concrete and symbolic executions we need to define first what symbolic execution paths are.

Definition 4.1 (Symbolic Execution Path)

The set of symbolic execution paths is coinductively defined by the following set of rules:

ϕ ϕ satisfiable (5)
τ s ϕ 0 ⇒ s S τ s ϕ 0 S-derivable, hd (τ s ) ∈ ∆ S (ϕ 0 ) (6)
where hd is coinductively defined by

hd (ϕ) = ϕ hd (ϕ 0 ⇒ s S τ s ) = ϕ 0
Remark 4.1 An alternative, equivalent definition for symbolic paths consists in requiring that hd(τ s ) is satisfiable in the rule (6) above. As a consequence, the symbolic paths thus defined are all feasible.

A symbolic execution path essentially consists in a possibly infinite list of ML formulas, where every two consecutive formulas ϕ and ϕ satisfy ϕ ∈ ∆ S (ϕ).

Notation We write ϕ 1 ⇒ s {ϕ l ⇒ ⇒ ⇒ ϕr} ϕ 2 if ϕ 2 = ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ 1 ).
A symbolic execution path covers a concrete one if the latter is an instance of the former. Formally, this notion is defined below: Definition 4.2 Consider the following rules:

ϕ, (γ, ρ) (γ, ρ) |= ϕ (7) τ s , (τ, ρ) ϕ 0 ⇒ s {ϕ l ⇒ ⇒ ⇒ ϕr} τ s , (γ 0 ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} τ, ρ) (γ 0 , ρ) |= ϕ 0 (8)
We write τ s (τ, ρ) if τ s , (τ, ρ) ∈ ν (7, 8), where (7, 8) is the system of the ground rules defined by [START_REF] Cadar | Klee: unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF] and [START_REF] Cadar | EXE: automatically generating inputs of death[END_REF].

Note that if τ s (τ, ρ) then the symbolic path and the concrete one either are finite and have the same length or both are infinite.

We now show that the symbolic execution thus defined is related with concrete execution via the coverage and precision properties stated in the introduction. The coverage property states that the symbolic paths symbolically simulate concrete ones.

Lemma 4.1 (Symbolic Step Forward-Simulates Concrete Step) If γ 1 ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} γ 2 and (γ 1 , ρ) |= ϕ 1 then there is ϕ 2 such that (γ 2 , ρ) |= ϕ 2 and ϕ 1 ⇒ s {ϕ l ⇒ ⇒ ⇒ ϕr} ϕ 2 .
The next theorem follows from the previous lemma. It can be used to draw conclusions about the absence of concrete program executions on a given path from the absence of feasible symbolic executions on the same path.

Theorem 4.1 (Coverage) For every concrete path τ (γ ⇒ S τ, ρ) and ML formula ϕ such that (γ, ρ) |= ϕ there exists a symbolic path τ s (ϕ ⇒ s S τ s ) such that τ s (τ, ρ).

The precision property states that symbolic execution paths are backwardssimulated by concrete ones. Forward simulation does not hold in this case, because the formulas resulting from a symbolic step may be unsatisfiable.

Lemma 4.2 (Concrete Step Backward-Simulates Symbolic Step)

If ϕ 1 ⇒ s {ϕ l ⇒ ⇒ ⇒ ϕr} ϕ 2 and (γ 2 , ρ) |= ϕ 2 then there is γ 1 such that γ 1 ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} γ 2 and (γ 1 , ρ) |= ϕ 1 .
The precision result, given below, is based on above the backwards-simulation lemma. Path executed "backwards" are finite because they end up in an initial state, thus, the precision result holds for finite paths only.

Theorem 4.2 (Precision) For all finite symbolic executions τ s , there exists (τ, ρ) such that τ s (τ, ρ).

The theorems in this section generalise the similar ones in [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF] and say that symbolic execution can be used as a sound program-analysis technique. That is, to check whether a given (finite) control-flow path is concretely executable in a program, one can attempt to symbolically execute the rules corresponding to the instructions in the control-flow path; thanks to the coverage and precision results, the attempt succeeds if and only if the path is concretely executable.

Application: Reachability-Logic Verification

Symbolic execution is, in general, not enough for performing program verification, because one can (obviously) only generate bounded-length symbolic executions, whereas program verification, especially in the presence of loops and recursive function calls, would require in general executions of an unbounded length. For example, verifying the RL formula (2) on the program in Fig. 4 require such an unbounded-length symbolic executions because of the unboundedly many iterations of the loop. This issue is dealt with in the present section by means of circular coinduction built on top of symbolic execution.

We first define the notion of symbolic semantics of RL formulas, then rephrase RL formula verification by symbolic execution as a proof system. Finally, circular coinduction amounts to adding a circularity rule to that proof system. We prove that the resulting 3-rule proof system is sound, i.e., that if it manages to prove a given (set of) RL formula(s) then the formulas hold semantically. Definition 5.1 (Symbolic Semantics of RL) Let τ s be a symbolic execution path and ϕ ⇒ ⇒ ⇒ ϕ and RL formula. We say that τ s satisfies ϕ ⇒ ⇒ ⇒ ϕ and we write τ s |= ϕ ⇒ ⇒ ⇒ ϕ for τ s , ϕ ⇒ ⇒ ⇒ ϕ ∈ ν (9, 10), where (9,10) is the system of the ground rules:

ϕ 0 , ϕ ⇒ ⇒ ⇒ ϕ T |= ϕ 0 → ϕ ∧ ϕ (9) τ s , ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ ⇒ ⇒ ⇒ ϕ ) ϕ 0 ⇒ s ϕ 1 ⇒ ⇒ ⇒ ϕ 2 τ s , ϕ ⇒ ⇒ ⇒ ϕ T |= ϕ 0 → ϕ, ϕ 1 ⇒ ⇒ ⇒ ϕ 2 ∈ S (10)
The following proof system can be used to prove RL formulas by symbolic execution. The first rule says that RL formulas hold if their left hand-side implies (in the sense of ML) their right-hand side. The second rule says that (derivable) formulas hold whenever their derivatives hold.

Definition 5.2 (SYSTEP)

[impl] ϕ ⇒ ⇒ ⇒ ϕ T |= ϕ → ϕ [der] ∆ S (ϕ ⇒ ⇒ ⇒ ϕ ) ϕ ⇒ ⇒ ⇒ ϕ ϕ is S-derivable
The following theorem states the soundness of this simple proof system:

Theorem 5.1 If S is total then S |= ν SYSTEP.
Specifically, if one can construct a finite proof tree under SYSTEP for a given RL formula then the formula belongs to ν SYSTEP. Theorem 5.1 then says that the formula holds in the semantics S. An RL formula also holds if a infinite proof tree under SYSTEP can be built. We give below an example of an infinite proof tree, which we reuse in order to show how circular coinduction can "fold" infinite proof trees into finite ones in a stronger proof system.

Suppose that S is the set of RL formulas corresponding while language. A proof tree for

while (x!=0) {s=s+x; x=x-1;} P k x → a s → 0 env cfg ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2
is represented in Figure 5. T 1 corresponds to the case when the while condition is false. One can see that T 2 is infinite and corresponds to unfolding indefinitely of the while loop.

Circular Coinduction

In this section we show how to reduce infinite proof trees to finite ones in a stronger proof system, which adds to SYSTEP a circularity rule. The rule is thus called because it allows one to use conclusions, i.e., formulas to be proved (from a set G of goals) as hypotheses during proofs of formulas from the set G.

T 2

. . . [der]

while (x != 0) {s=s+x; x=x-1;

} P k x → a -Int 1 s → a env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 [der] x=x-1;while (x != 0) {s=s+x; x=x-1;} P k x → a s → a env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 [der] s=s+x; x=x-1;while (x != 0) {s=s+x; x=x-1;} P k x → a s → 0 env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 T 1 [impl] P k x → a s → 0 env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2
T 1 T 2 while (x!=0) {s=s+x; x=x-1;} P k x → a s → 0 env cfg ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2
Fig. 5. An infinite proof tree under SYSTEP Definition 5.3 (Symbolic Circular Coinduction) Let G be a finite set of S-derivable RL formulas. Then the set of rules SCC(G) consists of SYSTEP together with

[circ] ∆ {ϕc ⇒ ⇒ ⇒ ϕ c } (ϕ ⇒ ⇒ ⇒ ϕ ) ϕ ⇒ ⇒ ⇒ ϕ T |= ϕ → (∃var (ϕ c ))ϕ c , ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G
The rule [circ] can be seen as a "big symbolic step" that accelerate the proving process. It does not increase the proving power of the system SYSTEP, but it transform some infinite proof trees into finite ones, which can be built in finite time.

The following theorem, which we call circularity principle, states that when we add the circularity rule (and the circular reasoning that it allows) to SYSTEP it does not compromise soundness. The main reason is to start not with G, but with ∆ S (G), i.e., with the S-derivatives of the formulas in G.

We shall be using the notation S |= G for S |= ϕ ⇒ ⇒ ⇒ ϕ for all ϕ ⇒ ⇒ ⇒ ϕ ∈ G.

Theorem 5.2 (Circularity Principle) Assume S total and that for each

ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G, var (ϕ c ) ⊆ var (ϕ c ). If ∆ S (G) ⊆ ν SCC(G) then S |= G.
Note The advantage of using SCC(G) is that it generates finite proof trees for a substantially larger set of RL formulas then SYSTEP. Its efficiency depends on the sets G given to it as input. This is quite similar to what happens when proving programs in Hoare logics, where the program specification needs additional information (under the form of loop invariants) in order to be successful.

Such a procedure can be used in an interactive way: first, it can be run it for proof trees of bounded height, and if it does not successfully terminates, one can analyse the proof trees built in order to guess some additional RL formulas, which, if added to G, increases the chance to find finite proof trees.

The finite proof tree under SCC that corresponds to the infinite proof tree T 2 under SYSTEP is represented in Fig. 6.

As final comments in this section, we note that, on the one hand, our 3-rule proof system SCC is substantially simpler that the original 8-rule proof system for RL given in [START_REF] Ştefănescu | All-path reachability logic[END_REF]: a rule in SCC corresponds to many small reasoning steps in the original proof system. The downside is that we lose the theoretical relative completeness result of [START_REF] Ştefănescu | All-path reachability logic[END_REF], which says that all valid RL formulas can (in principle) be proved. We prefer to focus on practical examples (shown in Section 7.1) to illustrate the usefulness of SCC . On the other hand, SCC is a strict generalisation of a RL verification procedure presented in [START_REF] Lucanu | Verifying Reachability-Logic Properties on Rewriting-Logic Specifications[END_REF]: that procedure can be seen a a strategy in SCC, in which implication is always applied before circularity, which is itself always applied before derivation.

[impl]

(∃b) P k x → 0 s → b env cfg ∧ b = Int (a -Int 1)a 2 + Int (s 0 + Int a) ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 + Int s 0 [circ] while (x!=0) {s=s+x; x=x-1;} P k x → a -Int 1 s → s 0 + Int a env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 + Int s 0 . . . [der] s=s+x; x=x-1;while (x!=0) {s=s+x; x=x-1;} P k x → a s → s 0 env cfg ∧ a = Int 0 ⇒ (∃b) P k x → 0 s → b env cfg ∧ b = Int a(a + Int 1) 2 + Int s 0
Fig. 6. The finite proof tree under SCC corresponding to the infinite proof tree T 2 in Fig. 5 6

Symbolic Execution via Language Transformation

As seen in the previous section, the derivative operation is essential both for symbolic execution and RL formula verification. In this section we show how the operation, currently defined as a matching, resp. reachability-logic formula transformer -i.e., ∆ S (ϕ) {(∃var

(ϕ l , ϕ r ))(ϕ l ∧ ϕ) =? ∧ ϕ r | ϕ l ⇒ ⇒ ⇒ ϕ r ∈ S} for ML formulas ϕ, and, respectively ∆ S (ϕ ⇒ ⇒ ⇒ ϕ ) {ϕ 1 ⇒ ⇒ ⇒ ϕ | ϕ 1 ∈ ∆ S (ϕ)}
for RL formulas ϕ ⇒ ⇒ ⇒ ϕ -can, under reasonable restrictions, be expressed by means of matching and rewriting. This is essential when implementing the proposed symbolic execution and verification techniques in a rewriting-based framework such as K. We show that the language transformation technique proposed in [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF] can be extended to the more general framework proposed here. The enhanced implementation is discussed in the next section.

Computing Derivatives by Matching

Consider a language definition L = (Φ, T , S) over an ML signature Φ = (Σ, Π, Cfg). We assume a subsignature (Σ Data , Π Data ) of (Σ, Π) consisting of all data sorts and their corresponding operations and predicates, e.g., integers, maps, trees,. . . depending on the language L. We assume that the sort Cfg and the syntax of L are not data, i.e., they are defined by operations in Σ \ Σ Data .

We also assume that T interprets the data sorts (those included in the subsignature Σ Data ) according to some Σ Data -algebra D (in which, for technical reasons, constants in Σ Data are interpreted syntactically). Given the data model D we construct a signature Σ(D) by adding to Σ the elements of D as constants of the corresponding sorts. Moreover, we assume that the model T consists of equivalence classes of ground terms over Σ(D), modulo a congruence ∼ = A induced by a set of axioms A, e.g., any combination of associativity, commutativity and unity, for which there exists a finitary and complete unification algorithm, which moreover reduces to matching terms modulo the axioms in question.

In the sequel we shall mostly be concerned with pairs t, t of terms, where

• t is a term in T Σ(D),Cfg (Var Data ), i.e., a basic pattern over Σ with variables in a set Var Data ⊂ Var of data variables, corresponding to basic patterns of configurations that are states in symbolic execution paths; • t is a term in T l Σ\Σ Data ,Cfg (Var ), i.e., a linear basic pattern corresponding to the left-hand side of a rule in the semantics S of the language of interest.

We shall see later in this section that the constraints on t and t can be achieved by simple transformation on the rules S defining the semantics of the language. Definition 6.1 (A-unifier) With the above notations, we say that two terms t ∈ T Σ(D),Cfg (Var Data ) and t ∈ T l Σ\Σ Data ,Cfg (Var ) are A-unifiable if there is ρ : Var → T satisfying tρ ∼ = A t ρ. The valuation ρ is an A-unifier of t, t .

Remark 6.1 The congruence tρ ∼ = A t ρ in Definition 6.1 is just equality in the model T , hence, it can also be written tρ = t ρ.

Let us also define the A-matching between two terms of the above form. Definition 6.2 (A-matcher) With the above notations, given two terms t ∈ T Σ(D),Cfg (Var Data ) and t ∈ T l Σ\Σ Data ,Cfg (Var ), we say that a substitution σ :

var (t ) → T Σ(D) (Var Data ) is an A-matcher of t onto t if t ∼ = A t σ.
The next assumption requires that A-unification can be achieved by A-matching.

Assumption 6.1 We assume that for all terms t ∈ T Σ(D),Cfg (Var Data ) and t ∈ T l Σ\Σ Data ,Cfg (Var ), if t and t are A-unifiable, then there is a finite set µ(t , t) of A-matchers of t onto t, such that for each A-unifier ρ of t and t , there are σ 0 ∈ µ(t , t) and a valuation ρ : Var → T such that ρ = σ 0 ρ2 .

That is, each A-unifier is an instance of an A-matcher for the terms in question.

The assumption holds under reasonable requirements3 (i.e., the axioms are linear, regular, and non-collapsing). Combinations of the usual associativity, commutativity, and unity (ACU) axioms typically satisfy these requirements, and K language definitions intensively use these axioms (e.g., cells in configurations belong to ACU bags).

The second assumption restricts the class of RL formulas that can be used as program properties or as semantical rules to those that are actually useful in practice: left-hand sides are elementary patterns with linear basic patters over the signature Σ(D), whereas right-hand sides are quantified elementary patterns, such that there are no additional free variables in right-hand sides of formulas.

Assumption 6.2 We consider RL formulas ϕ 1 ⇒ ⇒ ⇒ ϕ 2 satisfying var (ϕ 2 ) ⊆ var (ϕ 1 ), ϕ 1 π 1 ∧ φ 1 with π 1 ∈ T Σ\Σ Data ,Cfg (Var ), and ϕ 2 (∃Y )π 2 ∧ φ 2 .
Lemma 6.1 (ML Derivatives by Matching) Under the given assumptions, consider an RL formula

ϕ 1 ⇒ ⇒ ⇒ ϕ 2 with ϕ 1 π 1 ∧ φ 1 , ϕ 2 (∃Y )π 2 ∧ φ 2 , and ϕ (∃X)π ∧ φ such that (X ∪ var (ϕ)) ∩ (Y ∪ var (ϕ 1 , ϕ 2 )) = ∅. Then, ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) = σ∈µ(π 1 ,π) (∃X, Y )π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ
In a nutshell the above lemma shows that semantically speaking, derivatives ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) are certain ML formulas in which matchers (in the set µ(π 1 , π)) are present.

Computing Derivatives by Rewriting: Language Transformation Lemma 6.1 shows how derivatives can equivalently be computed using matching. In this section we build on that result to show that derivatives can be computed by rewriting in a transformed language definition.

Consider a language definition L = (Φ, T , S) over an ML signature Φ = (Σ, Π, Cfg). The transformation consists in creating a so-called symbolic language L s = (Φ s , T s , S s ) over a symbolic ML signature Φ s = (Σ s , Π s , Cfg s ). Symbolic Model. The symbolic model T s interprets syntactically all operations in Σ s except for the list concatenation operation, which is interpreted according to its (standard) equational definition. T s interprets the single predicate symbol sat : Fol → Bool as the satisfiability of FOL formulas: the interpretation of sat (conveniently, also denoted by sat) returns true iff the FOL formula interpreting the input of sat is satisfiable.

Symbolic Rules. Creating the set S s consists of the two following sub-steps:

• linearisation and Σ Data -operation elimination: this transformation deals with the left-hand sides π 1 ∧ φ 1 of RL formulas in S, for which Assumption 6.2 requires π 1 ∈ T l Σ\Σ Data ,Cfg (Var ), that is, π 1 is linear and does not contain any operations in Σ Data (specifically, not even constants in Σ Data ). This is achieved by replacing in π 1 duplicated variables and subterms containing operations in Σ Data with fresh variables, and by adding constraints to φ 1 that equate the newly introduced variables with the subterms they replaced. • definition of the symbolic rules: for each rule

π 1 ∧ φ 1 ⇒ ⇒ ⇒ (∃Y )π 2 ∧ φ 2 ∈ S, a rule (∃L)(π 1 ∧ s ψ) ∧ sat(φ 1 ∧ ψ) ⇒ ⇒ ⇒ (∃L, Y )π 2 ∧ s (φ 2 ∧ φ 1 ∧ ψ) (11)
is created in S s , where ψ is a variable of the sort Fol , L is a variable of sort IdList, and _, _ is the concatenation operation over IdList.

The symbolic language L s is now defined. Then we have a main result of this section, which says that derivatives can be computing by rewriting in L s . Theorem 6.1 (Derivatives by Rewriting in L s ) Let S be a set of RL formulas satisfying the assumptions of this section and ϕ (∃X)π ∧ φ be a quantified elementary pattern, such that X ∪ var (ϕ) is disjoint from the set of all variables (free or bound) occurring in S. Then, ∆ S (ϕ) = ϕ⇒ S s ϕ ϕ .

The theorem says that, semantically speaking, the derivation operation for configurations of a language L amounts to computing successors according to the transition relation in the symbolic language definition L s , which is computed by rewriting just as in any language definition in our framework.

The results in this section extend our own previous approach from [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF] with new features such as existentially quantified patterns and rewriting modulo axioms. The extensions are theoretically nontrivial and are also important from a practical point of view. Specifically, RL formulas for program specifications (ranging from simple ones such as (2) to complex ones shown in the next section) do require quantifiers for expressiveness issues, and axioms are intensively used in K language definitions as discussed earlier in the paper.

7 Implementation in the K Framework

In this section we present a prototype tool implementing our symbolic execution approach. We first briefly describe the tool and its integration within the K framework. Then we illustrate the tool, as well as its extension that performs deductive verification of RL formulas, on some nontrivial programs.

7.1 Symbolic Execution within the K Framework 3.4

We have integrated our symbolic execution framework in version 3.4 of the K framework [START_REF] Roşu | An overview of the K semantic framework[END_REF]. In K, the definition of a language, say, L, is compiled into a Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF] rewrite theory using the technique described in [START_REF] Rusu | Language definitions as rewrite theories[END_REF]. Then, the K runner executes programs in L by applying the resulting rewrite rules to configurations containing programs. Our implementation follows the same process, as it is described in [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF]. The main difference is that our new K compiler includes the additional transformations steps: rule linearisation, replacing the data subterms in left-hand-sides of rules with fresh variables and adding constraints to the rule's condition equating the fresh variables to the terms they replaced, adding a cell for path condition, and modifying semantical rules into symbolic rules of the form (11) according to the technique described in Section 6. The effect is that the compiled rewrite theory we obtain defines a symbolic semantics of L in the sense of Section 4 instead of its concrete semantics. We note that the symbolic semantics can execute programs with concrete inputs as well. For user convenience we have also improved the K runtime environment with some specific options which are useful for providing programs with symbolic input and setting up an initial path condition. A conservative approximation of the predicate sat is implemented using the K's interface to the Z3 SMT solver [START_REF] De | Z3: An efficient SMT solver[END_REF].

Given a K language definition, our tool automatically generates its symbolic semantics. Thus, users that already have a K language definition can sym-

void init(int a[], int n, int x, int j) { int i = 0; int *p = & a[0]; a[j] = x; while (*p != x && i < n) { *(p++) = 2 * i; i = i + 1; } if (i > j) { cout << "error"; } } void main() {
int n, j, x, i; cin >> n >> j >> x; int a[n]; i = 0; while(i < n) { cin >> a[i]; i = i + 1; } init(a, n, x, j); } Fig. 7. CinK program: init-arrays bolically execute their programs without having to change anything in them. Actually, symbolic execution using the transformed definition amounts to applying the set of rules SYSTEP.

Bounded model checking

We illustrate symbolic execution with CinK and show how the K runner can directly be used for performing bounded model checking. In the program in Figure 7, the function init assigns the value x to the array a at an index j, then fills the array with ascending even numbers until it encounters x in the array; it prints error if the index i went beyond j in that process. The i-th array element is accessed using the pointer p. The function init is called in the function main with arguments read from the standard input. In [START_REF] Armando | Model checking linear programs with arrays[END_REF] it has been shown, using model checking and abstractions on arrays, that this program never prints error. It is worth noting that the CinK program used here is trickier than the one in [START_REF] Armando | Model checking linear programs with arrays[END_REF][START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF] since it uses conversions between arrays and pointers. We obtain the same result as [START_REF] Armando | Model checking linear programs with arrays[END_REF][START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF] by running the program with symbolic inputs and using the K runner as a bounded model checker:

$ krun init-arrays.cink -cPC="n > Int 0" -search -cIN="n j x a1 a2 a3" -pattern="<T> <out> error </out> B:Bag </T>" Search results: No search results

The initial path condition is n > Int 0. The symbolic inputs for n,j,x are entered as n j x, and the array elements a1 a2 a3 are also symbolic. The -pattern option specifies a pattern to be searched in the final configuration: the text error should be in the configuration's output buffer. The above command thus performs a bounded model-checking with symbolic inputs; the bound is implicitly set by the number of array elements given as inputs, but it can be specified by the initial path condition as well, e.g., n < Int 4. It does not return any solution, meaning that that the program will never print error.

The result was obtained using symbolic execution without any additional tools or techniques. We note that array size is symbolic as well, a feature that, to our best knowledge, is not present in other symbolic execution frameworks.

Reachability-Logic Verification

In this section we illustrate the usage of our verification prototype on the Knuth-Morris-Pratt [START_REF] Knuth | Fast pattern matching in strings[END_REF] string matching algorithm. The current implementation is an extension of both our K symbolic compiler and the K runner. In order to verify whether a set of reachability formulas (goals) G holds, given language semantics S, the tool completes two stages during its execution: it builds a new definition and then performs verification. Given a language definition L and a set of RL formulas G, the tool produces a new definition consisting of the symbolic semantics L s of L enriched with the rules from G. This new definition is used to perform symbolic execution of the patterns in left-hand sides of formulas in ∆ S (G). Actually, symbolic execution using the enriched definition amounts to applying the set of rules SCC(G). The tool gives priority to rules in G in order to accelerate the process of finding a proof.

Verifying the Knuth-Morris-Pratt string matching algorithm: KMP

The Knuth-Morris-Pratt algorithm [START_REF] Knuth | Fast pattern matching in strings[END_REF] searches for occurrences of a word P , usually called pattern, within a given text T by making use of the fact that when a mismatch occurs, the pattern contains sufficient information to determine where the next search should begin. A detailed description of the algorithm, whose CinK code is shown in Figure 8, can be found in [START_REF] Thomas | Introduction to Algorithms[END_REF].

The KMP algorithm optimises the naive search of a pattern into a given string by using some additional information collected from the pattern. For instance, let us consider T = ABADABCDA and P = ABAC. It can be easily observed that ABAC does not match ABADABCDA starting with the first position because there is a mismatch on the fourth position, namely C = D.

The KMP algorithm uses a prefix function π, which, for each position j in P , returns the length of the longest proper prefix of the subpattern up to position j which is also a suffix of it. For our example, π[3] = 1 and π[j] = 0 for j = 1, 2, 4. In the case of a mismatch between the position i in T and the position j in P , the algorithm proceeds with the comparison of the positions i and π[j]. For the above mismatch, the next comparison is between the B in ABAC and the first instance of D ABADABCDA, which saves a comparison of the characters preceding them, since the algorithm "already knows" that they are equal (here, they are both A). contrast, we do not modify the algorithm from [START_REF] Thomas | Introduction to Algorithms[END_REF]. We also prove that KMP finds all the occurrences of the pattern in the string, not only the first one. We use P i to denote the prefix of P of size i (e.g., if P c 1 c 2 . . . c m then P i c 1 . . . c i ), and P [i] to denote its i-th element (i.e., P [i] c i ). Also, we denote by P T the fact that P is a suffix of T . Definition 7.1 Let P be a pattern of size m ≥ 1 and T a string of characters of size n ≥ 1. We define the following functions and predicate:

• π(i) is the length of the longest proper prefix of P i which is also a suffix for P i , for all 1 ≤ i ≤ m; also, π * (i) {π(i), π(π(i)), . . . , 0} (cf. [START_REF] Thomas | Introduction to Algorithms[END_REF]) • θ(i) is the length of the longest prefix of P that matches T on the final position i, i.e., P θ(i) T i , where 1 ≤ i ≤ n; • allOcc(Out, P, T, i) holds iff the list Out contains all the occurrences of P in T i , where

1 ≤ i ≤ n.
The specification of the kmp_matcher function is the following RL formula:

kmp_matcher(p, t,m,n); k • out p →l 1 t →l 2 env l 1 → P l 2 → T store . . . cfg ∧ ∧ ∧ n ≥ 1 ∧m ≥ 1 ⇒ ⇒ ⇒ • k Out out . . . env . . . store . . . cfg ∧ ∧ ∧ allOcc(Out, P, T, n)
This formula says that from a configuration where the program variables p and t are bound to the values P , T , respectively, the output cell is empty, and the kmp_matcher function has to be executed, one reaches a configuration where the function has been executed and the output cell contains all the occurrences of P in T . Note that we passed the symbolic values m and n as actual parameters to the function which are the sizes of P , and T , respectively. An advantage of RL with respect to Hoare Logic is, in addition to language independence, the fact that RL formulas may refer to all the language's configuration, whereas Hoare Logic formulas may only refer to program variables. A Hoare Logic formula for the kmp_matcher function would require the addition of assignments to a new variable playing the role of our output cell.

There are some additional issues concerning the way users write the RL formulas. These may be quite large depending on the size of the K configuration of the language. To handle that, we have created an interactive tool for generating such formulas. Users can annotate their programs with preconditions and postconditions and then use our tool to generate RL formulas from those annotations. For instance, the above specification for KMP is generated from the following annotation:

//@pre: m >= 1 /\ n >= 1 kmp_matcher(p, t, m, n) { ... } //@post: allOcc(Out, p, t, n)

In the annotations we use the program variables (e.g. pi, p, m) and a special variable Out which is meant to refer the content of the out cell. This variable gives us access to the output cell, which is essential in proving that the algorithm computes all the occurrences of the pattern in the text.

Loops can be annotated with invariants using a syntax as follows:

while (COND) { //@inv: INV ... }

where INV is the invariant (see Figure 8 for examples of invariants). For each annotated loop, the tool generates an RL formula which states that by starting with a configuration where the entire loop remains to be executed and INV holds, one reaches a configuration where the loop was completely executed and INV ∧ ¬COND holds.

From the annotations shown in Figure 8 the tool generates all the RL formulas that we need to prove KMP. Since KMP has four loops and two pairs of pre/postconditions, the tool generates and proves a total number of six RL formulas.

Finally, every particular verification problem requires problem-specific constructions and properties about them. For verifying KMP we have enriched the symbolic definition of CinK with functional symbols for π, π * , θ, and allOcc, and we independently prove the following facts:

If P is a pattern of length m, π is its prefix function, and T a string of length n, then (1) for all q ∈ {1, . . . , m}, π * (q) = {j | 0 ≤ j < q ∧ P j P q };4 (2) for all q ∈ {1, . . . , m}, 0 ≤ π(q) < q;

(3) for all q ∈ {1, . . . , m}, if π(q) > 0 then π(q) -1 ∈ π * (q -1);5 (4) for all q ∈ {1, . . . , m}, for all k ∈ {1, . . . , m -1}, for all j ∈ π * (q -1), if (j ≥ k → P [j + 1] = P [q]) then π(q) ≤ π(k) + 1; (5) for all q ∈ {1, . . . , m}, if u ∈ π * (q) and P q T then P u T ; (6) for all u, j ∈ {1, . . . , m}, if u < j, P u T , and P j T then P u P j . ( 7) for all i ≥ 1, θ(i + 1) ≤ θ(i) + 1.

In the case of KMP, we had to figure out first the needed functions and predicates specific to the problem domain to write the RL specifications and the invariants for loops. For this, we followed the insightful and very intuitive comments about the algorithm from [START_REF] Thomas | Introduction to Algorithms[END_REF]. Second, we identified the properties listed above using a trial and error process, which also required manual labour. Essentially, this can be described in a few steps: use the tool to prove the formulas directly; in case of failure, get the translation of the formula for the solver and ask the solver to simplify the formula; then use the simplified formula and eventually some counterexamples returned by the solver to guess the needed property; check if this property holds; if it does, then append it to the set of axioms and reiterate the process until the tool finishes successfully.

The above example shows that the verification based on the circular coinduction technique proposed in Section 5.1 can be effective. The KMP example illustrate well that the program verification process also assumes the enrichment of the semantic domain, over which the language is defined, with additional reasoning in the problem domain. This can also be seen as a conservative extension of the language definition.

Conclusion and Future Work

We have presented a formal and generic framework for the symbolic execution of programs in languages definable in a matching-logic and term-rewriting setting. Symbolic execution is performed by applying the operation called derivative, which, under reasonable assumptions, can be computed by rewriting in a modified language definition. We prove that the symbolic execution thus defined has the naturally expected properties with respect to concrete execution: coverage, meaning that to each concrete execution there is a (feasible) symbolic one on the same path of instructions, and precision, meaning that each (feasible) symbolic execution has a concrete execution on the same path. Comparing with [START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF], these properties are set for a more general case and are expressed in terms of coinduction and mutual simulations. The incorporation of symbolic execution into a deductive system for program verification with respect to Reachability-Logic specifications is also presented. Finally, we present the implementation of a prototype tool based on the above theory and its applications to the bounded model checking and deductive verification of nontrivial programs written in a subset of C ++ also formally defined in K.

Future Work

We are planning to expand our tool, to make it able to seamlessly perform a wide range of program analyses, from testing and debugging to formal verifications, following ideas presented in related work, but with the added value of being language independent and grounded in formal methods. For this, we shall develop a rich domain of symbolic values, able to handle various kinds of data types. Formalising the interaction of symbolic-domain computations with symbolic execution is also a matter for future work.

Another future research direction is specifically targeted at our RL-formulas verifier, and aims at certifying its executions. The idea is to generate proof scripts for the Coq proof assistant [START_REF]The Coq proof assistant reference manual[END_REF], in order to obtain certificates that, despite any (inevitable) bugs in our tool, the proofs it generates are indeed correct. This amounts to, firstly, encoding our RL proof system in Coq, and proving its soundness with respect to the original proof system of RL (which have already been proved sound in Coq [START_REF] Roşu | Onepath reachability logic[END_REF]). Secondly, our verifier must be enhanced to return, for any successful execution, the rules of our system it has applied and the substitutions it has used. From this information a Coq script is built that, if successfully run by Coq, generates a proof term that constitutes a correctness certificate for the verifier's original execution. A longer-term objective is to turn our verifier into an external proof tactic for Coq, resulting in a powerful mixed interactive/automatic program verification tool.

(τ, ρ), ϕ ∈ ν R} is backward closed w.r.t. [START_REF] Cadar | Klee: unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF][START_REF] Cadar | EXE: automatically generating inputs of death[END_REF], that is, Y ⊆ (7, 8)(Y ) (♣), where [START_REF] Cadar | Klee: unassisted and automatic generation of high-coverage tests for complex systems programs[END_REF][START_REF] Cadar | EXE: automatically generating inputs of death[END_REF]

(Y ) = { ϕ, (γ, ρ) | (γ, ρ) |= ϕ} ∪ { ϕ 0 ⇒ s S τ s , (γ 0 ⇒ S τ, ρ) | (γ 0 , ρ) |= ϕ 0 , τ s , (τ, ρ) ∈ Y }
We choose an arbitrary sp( (τ , ρ ), ϕ ), (τ , ρ ) ∈ Y . Note that (τ , ρ ), ϕ ∈ ν R. If (τ , ρ ), ϕ was obtained using (A.1), then τ is an execution path consisting of a single concrete configuration, say τ γ , such that (γ , ρ ) |= ϕ . Moreover, ϕ = sp( (γ , ρ ), ϕ ) and thus, (γ , ρ ) |= sp( (τ , ρ ), ϕ ) which implies sp( (τ , ρ ), ϕ ), (τ , ρ ) ∈ (7, 8)(Y ).

On the other hand, if (τ , ρ ), ϕ was generated using (A.2) then there are γ , τ , and ϕ such that τ γ ⇒ S τ , (γ , ρ ) |= ϕ , ϕ ⇒ s S ϕ , and (τ , ρ ), ϕ ∈ ν R. From (τ , ρ), ϕ ∈ ν R we have sp( (τ , ρ ), ϕ ), (τ , ρ ) ∈ Y , which, combined with (γ , ρ ) |= ϕ and the fact that sp( (τ , ρ ), ϕ ) = ϕ ⇒ s S sp( (τ , ρ ), ϕ ), implies sp( (τ , ρ ), ϕ ), (τ , ρ ) ∈ (7, 8)(Y ).

Since sp( (τ , ρ ), ϕ ), (τ , ρ ) ∈ Y was arbitrarily chosen we obtain (♣).

Second, we show that X = {((τ, ρ), ϕ)|(hd (τ ), ρ) |= ϕ} (i.e, the set of all pairs

((τ, ρ), ϕ) such that (τ, ρ) starts from ϕ) is backward closed w.r.t R, that is, X ⊆ R(X), where R(X) is: {((γ, ρ), ϕ) | (γ, ρ) |= ϕ} ∪ {((γ 0 ⇒ S τ, ρ), ϕ 0 ) | (γ 0 , ρ) |= ϕ, ϕ 0 ⇒ s S ϕ, (hd (τ ), ρ) |= ϕ}.
Consider ((τ, ρ), ϕ) ∈ X. We distinguish the following cases:

• τ = γ, γ -irreducible. Since ((τ, ρ), ϕ) ∈ X we have (hd (τ ), ρ) |= ϕ which becomes (γ, ρ) |= ϕ. Using (A.1) we obtain ((τ, ρ), ϕ) ∈ R(X). • τ = γ 0 ⇒ S τ . From ((τ, ρ), ϕ) ∈ X we obtain (hd (τ ), ρ) |= ϕ, that is, (γ 0 , ρ) |= ϕ. On the other hand, γ 0 ⇒ S hd (τ ). By Lemma 4.1, there is ϕ such that (hd (τ ), ρ) |= ϕ and ϕ ⇒ s S ϕ . Since (hd (τ ), ρ) |= ϕ then ((τ , ρ), ϕ ) ∈ X. Thus, using (A.2) we obtain ((τ, ρ), ϕ) ∈ R(X).

Using the coinduction principle we obtain X ⊂ ν R. Thus, we started with an arbitrary pair ((τ, ρ), ϕ) such that (τ, ρ) starts from ϕ and proved that the pair also has the property that there is a symbolic path that starts with ϕ and covers (τ, ρ), which proves the lemma.

Proof of Lemma 4.2, Page 24. From ϕ 1 ⇒ s {ϕ l ⇒ ⇒ ⇒ ϕr} ϕ 2 we have ϕ 2 = ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ 1 ) (∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r . From (γ 2 , ρ) |= (∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r we obtain that there is ρ : Var → T such that (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ ϕ r and ρ | Var \var (ϕ l ,ϕr) = ρ| Var \var (ϕ l ,ϕr) . From (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ ϕ r we obtain in particular ρ |= (ϕ l ∧ ϕ 1 ) =? , hence, by Proposition 3.5 there exists γ 1 such that (γ 1 , ρ ) |= ϕ l ∧ ϕ 1 . Since we can assume w.r.g. var (ϕ 1 ) ∩ var (ϕ l , ϕ r ) = ∅ we obtain in τ = γ 0 ⇒ S τ , and γ

0 ⇒ ρ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } hd (τ ). We prove that f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) ⇒ ⇒ ⇒ ϕ , (τ , ρ)) ∈ Y in a similar we proceeded for showing that f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) ⇒ ⇒ ⇒ ϕ , (τ , ρ)), ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) ⇒ ⇒ ⇒ ϕ ∈ X. From f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), (τ, ρ) ∈ Y
we obtain (τ, ρ) starts from ϕ, i.e., (γ 0 , ρ) |= ϕ. By using (8) it follows that f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), (τ, ρ) ∈ (B.1, 8)(Y ).

We have Y ⊆ (B.1, 8)(Y ), and by the coinduction principle we obtain Y ⊆ ν (B.1, 8), i.e. f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)) (τ, ρ) for each f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), (τ, ρ) ∈ Y . Now f is completely defined and has the desired properties.

If ϕ ⇒ ⇒ ⇒ ϕ ∈ ν SYSTEP then there is a proof tree P of ϕ ⇒ ⇒ ⇒ ϕ under SYSTEP. If (τ, ρ) is a complete execution path starting from ϕ, then f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)) describes a symbolic path that covers (τ, ρ) and satisfies ϕ ⇒ ⇒ ⇒ ϕ , which, by Lemma B.1, implies that (τ, ρ) satisfies ϕ ⇒ ⇒ ⇒ ϕ . Since (τ, ρ) is arbitrarily chosen, it follows that S |= ϕ ⇒ ⇒ ⇒ ϕ by Definition 3.17.

Proof of Theorem 5.2, Page 27. We start with some intermediary lemmas, then prove the theorem, which we re-state here for the sake of clarity:

Assume S total and that for each

ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G, var (ϕ c ) ⊆ var (ϕ c ). If ∆ S (G) ⊆ ν SCC(G) then S |= G.
Lemma B.2 For all ML formulas ϕ and ϕ , and for all RL formulas

ϕ l ⇒ ⇒ ⇒ ϕ r , if T |= ϕ → ϕ then T |= ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ) → ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ ).
Proof Consider an arbitrary (γ , ρ) such that (γ , ρ) |= ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ). Using Lemma 4.2 we obtain a configuration γ such that (γ, ρ) |= ϕ and γ ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} γ . From T |= ϕ → ϕ we obtain (γ, ρ) |= ϕ , which, together with γ ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} γ gives us using Lemma 4.1 the ML formula ϕ ∆ {ϕ l ⇒ ⇒ ⇒ ϕr} (ϕ ) such that (γ , ρ) |= ϕ , which proves the lemma. We write τ s τ iff there exists ρ : Var → T such that τ s (τ, ρ). The relation can be extended to symbolic paths, too: Definition B.2 Let τ s and τ s be two symbolic execution paths. Then τ s τ s iff τ s τ implies τ s τ , for all execution paths τ .

The following technical lemma states a property of (one-step) symbolic execution paths regarding the relation: Proof We show that each rule applied in the construction of P ϕc ⇒ ⇒ ⇒ ϕ c (whose existence is known by Lemma B.4) can be used to construct P as well, provided that the left-hand side of the current node in P is satisfiable. Each time the same rule is applied for two corresponding nodes in P respectively P ϕc ⇒ ⇒ ⇒ ϕ c , there is a bijection between the children of the two nodes that preserves the way each child is obtained.

Lemma B.3 Let ϕ 1 ⇒ s S ϕ
c ⇒ ⇒ ⇒ ϕ c ∈ G, var (ϕ c ) ⊆ var (ϕ c ); and ∆ S (G) ⊆ ν SCC(G). Lemma B.4 G ⊆ ν SCC(G). Proof Each ϕ ⇒ ⇒ ⇒ ϕ c ∈ ∆ S (ϕ c ⇒ ⇒ ⇒ ϕ c )
At the end we shall obtain an injective tree homomorphism from P to P ϕc ⇒ ⇒ ⇒ ϕ c that maps the root of P into the root of P ϕc ⇒ ⇒ ⇒ ϕ c and each child of a node x in P into its correspondent given by the bijection between the children of x and the children of its homomorphic image. The only exception when different rules are applied is that in which for a node in P the inference rule [impl] is applied and for its homomorphic image [der] is applied; in those cases the Since f has to "visit" a collection of proof trees, f has now three arguments: f (ϕ, St, (τ, ρ)), where St is a list (stack) of pairs ϕ , P such that P ∈ PT (G) and if ϕ , P is the first pair in St then ϕ ⇒ ⇒ ⇒ ϕ is the current node in P . The definition of f is as follows:

(1) the current ϕ ⇒ ⇒ ⇒ ϕ in P corresponds to [impl], i.e. T |= ϕ → ϕ : (a) P is the proof tree of the initial goal:

f (ϕ, ϕ , T , (τ, ρ)) = ϕ (B.2) (b) P is the proof tree of a circularity. In this case f goes back to the proof tree that used the circularity:

f (ϕ, ϕ , P St, (τ, ρ)) = f (ϕ, St, (τ, ρ))

(B.3)
where St is not empty; (2) the current ϕ ⇒ ⇒ ⇒ ϕ in P corresponds to [der], i.e. ϕ is S-derivable, τ = γ 0 ⇒ S τ , and γ 0 ⇒ ρ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } hd (τ ). This case is similar to the proof of Theorem 5. The fact that function f is well-defined is ensured by the fact that the equations of the form f (. . .) = f (. . .) cannot be consecutively applied infinitely times:

• the equation (B.3)) decreases the length of the finite list St;

• the equation (B.5)) can be applied only once because the first rule used in

P ϕ ⇒ ⇒ ⇒ ϕ is [der].
Consequently, the rewriting relation defined by (B.3)) and (B.5)), seen as rewrite rules, is terminating.

In the sequel we prove that the symbolic path computed by the function call f (ϕ c , ϕ c , P ϕc ⇒ ⇒ ⇒ ϕ c , (τ, ρ)) satisfies ϕ c ⇒ ⇒ ⇒ ϕ c and partially covers (τ, ρ), for all ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G and (τ, ρ) starting from ϕ c . We assume that these symbolic paths are represented by expressions that are -irreducible. We write ϕ ∈ St if St includes a pair ϕ , P and let ST (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)) be the set of the lists St occurring in the proof tree of f (nil , ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)). Proof Let f (ϕ, St, (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ be in X and assume that St = ϕ , T St , where St is a possibly empty list. We distinguish the following cases:

• f (ϕ, ϕ , P , (τ, ρ)) = ϕ and T |= ϕ → ϕ . We obtain f (ϕ, ϕ , P , (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ ∈ (9, 10)(X) by ( 9). • f (ϕ, St, (τ, ρ)) = ϕ ⇒ s S f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)), ϕ is S-derivable, τ = γ 0 ⇒ S τ , and γ 0 ⇒ ρ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } hd (τ ). Since f (ϕ, ϕ , T , (τ, ρ)) is a suffix of a symbolic path f (ϕ c , ϕ c , T ϕc ⇒ ⇒ ⇒ ϕ c , (τ, ρ)) with ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G it follows that f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)) is a suffix as well. We obtain f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)), ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) ⇒ ⇒ ⇒ ϕ in X by further noticing that (τ , ρ) a complete execution path starting from ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) by the definition of γ 0 ⇒ ρ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } hd (τ ) and (γ 0 , ρ) |= ϕ ∧ ϕ 1 . Since T |= ϕ → ϕ we obtain f (ϕ, St, (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ ∈ (9, 10)(X) by [START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF]. Proof Let f (ϕ, St, (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ be in X. We distinguish the following cases:

• f (ϕ, ϕ , P , (τ, ρ)) = ϕ and T |= ϕ → ϕ . We obtain f (ϕ, ϕ , T , (τ, ρ)), (τ, ρ) ∈ (B.1, 8)(X) by (B.1). • f (ϕ, St, (τ, ρ)) = ϕ ⇒ s S f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)), ϕ is S-derivable, τ = γ 0 ⇒ S τ , and γ 0 ⇒ ρ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } hd (τ ). The fact that f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)), (τ , ρ) is in Y is proved in a similar way to the proof of the membership f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)), ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) ⇒ ⇒ ⇒ ϕ ∈ X. From the hypothesis f (ϕ, St, (τ, ρ)), (τ, ρ) ∈ Y we obtain that (τ, ρ) starts from ϕ, i.e., (γ 0 , ρ) |= ϕ. By using the rule (8) it follows that f (ϕ, St, (τ, ρ)), (τ, ρ) belongs to (B.1, 8)(Y ), which conclude this case.

In both cases we obtained that f (ϕ, St, (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ ∈ (B.1, 8)(X), which shows that X is backward closed. If ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G then there is a proof three P c of ϕ c ⇒ ⇒ ⇒ ϕ c under SCC. For each node ∆ ϕ d ⇒ ⇒ ⇒ ϕ d (ϕ ⇒ ⇒ ⇒ ϕ c ) in P c corresponding to the [circ] inference rule, there is a proof tree P for ϕ ⇒ ⇒ ⇒ ∆ ϕ d ⇒ ⇒ ⇒ ϕ d (ϕ ) under SCC(G) by Lemma B.5. If (τ, ρ) is a complete execution path starting from ϕ, then f (ϕ c , ϕ c , P ϕc ⇒ ⇒ ⇒ ϕ c , (τ, ρ)) is defined and describes a symbolic path that par-(⊇) Assume γ ∈ π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ , i.e., (γ , η) |= π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ for some σ ∈ µ(π 1 , π) and η : Var → T , and let ρ ση, where σ is the identity everywhere except perhaps on var (π 1 ). We prove (γ , ρ) ∈ ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) .

For this, let γ = π 1 ρ. We shall first prove (♣): (γ, ρ) |= ϕ π ∧ φ.

• We prove γ = πρ: we have γ = π 1 ρ = π 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, πη = πρ. The above chain of equalities ensures γ = πρ. 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 variables6 , to the two members of the equality in the lemma's conclusion.

Fig. 2 .

 2 Fig. 2. CinK configuration structure

Fig. 3 .Figure 3 ,

 33 Fig. 3. Subset of rules from the K semantics of CinK Figure 3, represents the (concrete) rule

Fig. 4 .

 4 Fig. 4. Sample CinK Program: gcd

Definition 3 . 4 (

 34 Many-Sorted First-Order Logic (FOL)) Given a set S of sorts, a first-order signature (Σ, Π) consists of a S * × S-sorted set Σ of function symbols (i.e., a many-sorted signature), and a S * -sorted set Π of predicate symbols. A (Σ, Π)-model consists of a Σ-algebra T and a subset T p ⊆ T s 1 × • • • × T sn for each p ∈ Π s 1 ...sn . Let Var denote a S-sorted set of variables. The set of (Σ, Π)-formulas is defined by

  a,b) Definition 3.7 (ML Model) A model for ML signature Φ = (Σ, Π, Cfg) is a (Σ, Π) first-order model T . Concrete configurations (or simply configurations) are elements of T Cfg , i.e., T -interpretations of ground terms of sort Cfg.

Definition 3 . 8 (

 38 ML Satisfaction) The satisfaction relation |= relates pairs (γ, ρ), where γ ∈ T Cfg and ρ : Var → T , with Φ-formulas ϕ. For basic patterns π, (γ, ρ) |= π is defined by γ = πρ. For the remaining ML constructions satisfaction is defined as expected, e.g., (γ, ρ) |= ∃Xϕ iff (γ, ρ ) |= ϕ for some ρ : Var → T such that xρ = xρ for all x ∈ Var \ X. If ϕ is an ML formula then ϕ denotes the set of concrete configurations {γ | (γ, ρ) |= ϕ for some ρ}.

  has a proof tree P ϕ ⇒ ⇒ ⇒ ϕ c under SCC, for all ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G. It follows that there is a proof tree P ϕc ⇒ ⇒ ⇒ ϕ c under SCC for each ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G obtained by applying the rule [der]. Hence G ⊆ ν SCC(G). Lemma B.5 Let ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G. If ϕ is S-derivable and T |= ϕ → (∃var (ϕ c ))ϕ c then there is a proof tree P for ϕ ⇒ ⇒ ⇒ ∆ {ϕc ⇒ ⇒ ⇒ ϕ c } (ϕ) under SCC(G).

  1: f (ϕ, St, (τ, ρ)) = ϕ ⇒ s S f (∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ), St, (τ , ρ)) (B.4) (3) the current ϕ ⇒ ⇒ ⇒ ϕ in P corresponds to [circ], i.e. T |= ϕ → (∃var (ϕ c ))ϕ c , ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G, and ϕ = ∆ {ϕc ⇒ ⇒ ⇒ ϕ c } (ϕ).In this case f moves to the root of the proof tree of the circularity:f (ϕ, St, (τ, ρ)) = f (ϕ, ϕ , P ϕ ⇒ ⇒ ⇒ ϕ St, (τ, ρ)) (B.5)

Lemma B. 6

 6 The set X = { f (ϕ, St, (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ | f (ϕ, St, (τ, ρ)) a suffix of a symbolic path f (ϕ c , ϕ c , P ϕc ⇒ ⇒ ⇒ ϕ c , (τ, ρ)) with ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G, ϕ ∈ St, and(τ, ρ) a complete execution path starting from ϕ c } is backward closed w.r.t. to[START_REF] Clarke | Hardware verification using ANSI-C programs as a reference[END_REF][START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF].

Lemma B. 7

 7 The set Y = { f (ϕ, St, (τ, ρ)), (τ, ρ) | f (ϕ, St, (τ, ρ)) a suffix of a symbolic path f (ϕ c , ϕ c , P ϕc ⇒ ⇒ ⇒ ϕ c , (τ, ρ)) with ϕ c ⇒ ⇒ ⇒ ϕ c ∈ G, ϕ ∈ St, and (τ, ρ) a complete execution path starting from ϕ c } is backward closed w.r.t. to (B.1, 8), where (B.1,8) is the set of rules given by (B.1) and (8).

  We prove ρ |= φ: 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.The statement (♣) is now proved. Next, we prove (♦): (γ, ρ)|= ϕ 1 π 1 ∧ φ 1 . We have γ = π 1 ρ by the definition of γ. From (γ , η) |= π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ we get η |= φ 1 σ which implies ση |= φ 1 , hence, ρ = ση |= φ 1 , which proves (♦).

Finally, we

  prove (♥): (γ , ρ) |= ϕ 2 π 2 ∧ φ 2 . We prove ρ |= φ 2 by analogy with ρ |= φ 1 above, and from(γ , η) |= π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ we get γ = (π 2 σ)η = π 2 (ση) = π 2 ρ, which concludes the proof of (♥).Recapitulating, we have (♣): (γ, ρ) |= ϕ, (♦): (γ, ρ) |= ϕ 1 , and (♥) (γ , ρ) |= ϕ 2 . 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.

  Kleene's Theorem. The set of infinite lists over Z is the greatest fixed point of the system consisting only of rule [B], i.e. Z ω = ν [B]. The set of finite lists is the least fixed point µ LIST. Applying again Kleene's Theorem, we obtain

  Symbolic Signature. The algebraic signature Σ s adds new sorts Bool and Fol to Σ and, for each predicate p ∈ Π s 1 ,...,sn , a new operation o p : s 1 × • • • × s n → Bool . Σ s includes constructors for representing FOL formulas as terms of sort Fol . It also adds to Σ new sorts Id for identifiers and IdList for lists of identifiers, with a (standard) equationally defined concatenation operation _, _ : IdList × IdList → IdList. Finally, Σ s includes a sort Cfg s for symbolic configurations with its constructor (∃_)_ ∧ s _ : IdList × Cfg × Fol → Cfg s . The set Π s consists of one single new predicate symbol: sat : Fol → Bool .

  2 be a one-step symbolic execution path and ϕ 1 an S-derivable ML formula. If T |= ϕ 1 → (∃var (ϕ 1 ))ϕ 1 then there exists ϕ 2 such that ϕ 1 ⇒ s S ϕ 2 ϕ 1 ⇒ s S ϕ 2 and T |= ϕ 2 → ϕ 2 . if τ s τ then τ s τ (cf. Definition B.2). From τ s τ and Definition 4.2 we obtain a valuation ρ such that (γ 1 , ρ) |= ϕ 1 and (γ 2 , ρ) |= ϕ 2 . From T |= ϕ 1 → (∃var (ϕ 1 ))ϕ 1 and (γ 1 , ρ) |= ϕ 1 we obtain a valuation ρ such that (γ 1 , ρ ) |= ϕ 1 and xρ = xρ for all x ∈ var (ϕ 1 ). Let ρ : Var → T be a valuation defined as follows: xρ = xρ, for all x ∈ var (ϕ 1 ) and xρ = xρ for all x ∈ var (ϕ 1 ). From (γ 1 , ρ ) |= ϕ 1 we obtain (γ 1 , ρ ) |= ϕ 1 because ρ coincides with ρ on var (ϕ 1 ). On the other hand, from (γ 2 , ρ) |= ϕ 2 and the fact that var (ϕ 1 ) ∩ var (ϕ 1 , ϕ 2 ) = ∅ we obtain (γ 2 , ρ ) |= ϕ 2 since ρ coincides with ρ on variables not in var (ϕ 1 ), particularly on var (ϕ 2 ). From (γ 2 , ρ ) |= ϕ 2 and (♠) we obtain (γ 2 , ρ ) |= ϕ 2 .Thus, ϕ 1 ⇒ s S ϕ 2 (τ, ρ ), i.e., ϕ 1 ⇒ s S ϕ 2 τ , which proves the lemma. Let ϕ 1 ⇒ s S ϕ 2 be a one-step symbolic execution path and ϕ 1 an S-derivable ML formula. If T |= ϕ 1 → ϕ 1 then there exists ϕ 2 such that ϕ 1 ⇒ s S ϕ 2 ϕ 1 ⇒ s S ϕ 2 and T |= ϕ 2 → ϕ 2 . In the rest of this section we assume the hypotheses of our theorem: S is total; for each ϕ

	Corollary B.1 Remark B.1

Most existing operational semantics styles (small-step, big-step, reduction with evaluation contexts, . . . ) have been shown to be representable in this way in[START_REF] Şerbănuţă | A rewriting logic approach to operational semantics[END_REF].

ρ 1 = ρ 2 if for all x ∈ Var , xρ 1 = xρ 2 , where "=" denotes equality in the model T.

A proof of the assumption can be found in[START_REF] Rusu | Language definitions as rewrite theories[END_REF] (Th. 3: Unification by Matching).

Cf. Lemma 32.5 from[START_REF] Thomas | Introduction to Algorithms[END_REF]

Cf. Lemma 32.6 from[START_REF] Thomas | Introduction to Algorithms[END_REF]

The equality is a simple consequence of Def. 3.8 of the ML satisfaction relation.

/*@pre: m>=1 */ void compute_prefix(char p[],

int m, int pi[]) { int k, q; k = 0; pi [START_REF] Ahrendt | The KeY tool[END_REF] = 0; q = 2; while(q <= m) { /*@inv: 0 <= k /\ k < q /\ q <= m+1 /\ (forall u:1..k)(p[u]=p[q-1-k+u]) /\ (forall u:1..q-1)(pi[u]=Pi(u)) /\ (forall j)((j > k /\ j in Pi*(q-1)) implies p[j+1] != p[q]) /\ k in Pi*(q-1) /\ Pi(q)<=k+1 */ while (k > 0 && p[k+1] != p[q]) { /*@inv: 0 <= k /\ k < q /\ q <= m /\ (forall u:1..k)(p[u]=p[q-1-k+u]) /\ (forall u:1..q-1)(pi[u]=Pi(u)) /\ (forall j)((j > k /\ j in Pi*(q-1)) implies p[j+1] != p[q]) /\ k in Pi*(q-1) /\ Pi(q)<=k+1 */ k = pi[k]; } if (p[k + 1] == p[q]) { k = k + 1; } pi[q] = k; q++; } } /*@post: (forall u:1..m)(pi[u]=Pi(u)) */ /*@pre: m>=1 /\ n>=1 */ void kmp_matcher(char p[], char t[], int m, int n) { int q = 0, i = 1, pi[m]; compute_prefix(p, m, pi); while (i <= n) { /*@inv: 1 <= m /\ 0 <=q <= m /\ 1 <= i<= n+1 /\ (forall u:1..q)(p[u]=t[i-1-q+u]) /\ (forall u:1..m)(pi[u]=Pi(u)) /\ (exists v)((forall u:v+1..i-1) Theta(u)<m /\ allOcc(Out,p,t,v))/\ Theta(i)<=q+1 */ while (q > 0 && p[q + 1] != t[i]) { /*@inv: 1<=m /\ 0<=q<m /\ 1 <= i <= n/\ (forall u:1..q)(p[u]=t[i-1-q+u]) /\ (forall u:1..m)(pi[u]=Pi(u)) /\ (exists v)((forall u:v+1..i-1) Theta(u)<m /\ allOcc(Out,p,t,v))/\ Theta(i)<=q+1 */ q = pi[q]; } if (p[q + 1] == t[i]) { q = q + 1; } if (q == m) { cout << "shift: " << (i -m) << endl; q = pi[q]; } i++; }} /*@post: allOcc(Out, p, t, n) */ Fig. 8. The KMP algorithm annotated with pre-/post-conditions and invariants (syntactical sugar for RL formulas): prefix function (left) and the main function (right). In the annotations, Pi, Theta, Pi * , and allOcc denote functions π and θ, the set π * , and the predicate allOcc, respectively, which are defined axiomatically in an extension of CinK.

An implementation of KMP is shown in Figure 8. The comments include the specifications for preconditions, postconditions, and invariants, which will be explained later in this section (briefly, they are syntactic sugar for RL formulas, which are automatically generated from them). The program can be run either using the K semantics of CinK or the g++ GNU compiler. The compute_prefix function computes the prefix function π for each component of the pattern and stores it in a table, called pi. The kmp_matcher searches for all occurrences of the pattern in the string comparing characters one by one; when a mismatch is found on positions i in the string and q in the pattern, the algorithm shifts the search to the right as many positions as indicated by pi[q], and initiates a new search. The algorithm stops when the string is completely traversed.

For the proof of KMP we use the original algorithm as presented in [START_REF] Thomas | Introduction to Algorithms[END_REF]. Another formal proof of the algorithm is given in [START_REF] Christophe | Proof of kmp string searching algorithm[END_REF] by using Why3 [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF]. There, the authors collapsed the nested loops into a single one in order to reduce the number of invariants they have to provide. They also modified the algorithm to stop when the first occurrence of the pattern in the string was found. By

A Proofs of Results from Section 4

Proof of Lemma 4.1, Page 23.

Since variables of rules can always be renamed we can assume var (ϕ 1 ) ∩ var (ϕ l , ϕ r ) = ∅, thus, we can construct a valuation ρ such that ρ | var (ϕ 1 ) = ρ and ρ | var (ϕ l ,ϕr) = η, and then (γ 2 , ρ ) |= ϕ r and (γ 1 , ρ ) |= ϕ l ∧ ϕ 1 . Using Proposition 3.5 we obtain that ρ |= (ϕ l ∧ ϕ 1 ) =? . Finally, using the definition of the |= relation we obtain (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ ϕ r and (γ 2 , ρ) |= (∃var (ϕ l , ϕ 2 ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r , which proves the lemma.

Proof of Theorem 4.1, Page 23. In this proof we use the following set of rules R:

First, we show that ν R defines the set of all pairs of the form (τ, ρ), ϕ such that (τ, ρ) starts from ϕ and there is a symbolic path that starts with ϕ and covers (τ, ρ). For this we define coinductively a function sp over ν R:

, where ϕ is given by A.2.

It is easy to see that sp( (τ, ρ), ϕ ) is a symbolic path. Next, we coinductively prove that sp( (τ, ρ), ϕ ) (τ, ρ) by showing that Y { sp( (τ, ρ), ϕ ), (τ, ρ) | particular ρ | var (ϕ 1 ) = ρ| var (ϕ 1 ) , hence, (γ 1 , ρ) |= ϕ 1 . We choose this γ 1 to be the configuration whose existence is stated in the conclusion of our lemma.

To prove the lemma there remains to show (♠) γ 1 ⇒ {ϕ l ⇒ ⇒ ⇒ ϕr} γ 2 . From (γ 1 , ρ ) |= ϕ l ∧ϕ 1 we obtain in particular (γ 1 , ρ ) |= ϕ l , and from (γ 2 , ρ ) |= (ϕ l ∧ϕ 1 ) =? ∧ϕ r we obtain in particular (γ 2 , ρ ) |= ϕ r , which proves (♠) and the lemma.

Proof of Theorem 4.2, Page 24. Let R denote the following set of rules:

We first prove (♦) : µR ⊆ µR , where R is the set of rules from Definition 4.1.

We prove that X = µR is closed w.r.t. R, i.e., R(X ) ⊆ X and apply the Induction principle. Elements of R(X ) generated by the 1st rule of R consist of one (satisfiable) ML formula, hence, they are also obviously in X . Elements of R(X ) generated by the 2nd rule of R are of the form

Hence, the arbitrarily chosen τ s ∈ X generated by the 2nd rule of R satisfies the 2nd rule of R , which implies τ s ∈ R(X ), and we can conclude R(X ) ⊆ X . The proof of (♦) is now complete.

Next we prove (♠) that the set Y = {τ s ∈ µR|(∃τ, ρ)τ s (τ, ρ)} is closed w.r.t. R , i.e., R (Y ) ⊆ Y . Elements of R (Y ) generated by the 1st rule of R consist of one (satisfiable) ML formula ϕ, which covers the pair (γ, ρ) satisfying ϕ, hence, such ϕ are also obviously in Y . Elements of R (Y ) generated by the 2nd rule of R have the form τ s = ϕ ⇒ s S τ s where τ s ∈ Y (hence, τ s covers some (τ, ρ)), hd (τ s ) is satisfiable, and (∀γ )(γ , ρ) |= hd(τ s ) → (∃γ)(γ, ρ) |= ϕ∧ γ ⇒ S γ holds (from the condition of the 2nd rule of R ). We have (hd(τ ), ρ) |= hd(τ s ) from τ s (τ, ρ) thus, there exists γ such that (γ, ρ) |= ϕ and γ ⇒ S hd(τ ), which proves τ s = ϕ ⇒ s S τ s (γ ⇒ S τ, ρ) and thus the arbitrarily chosen τ s ∈ Y generated by the 2nd rule of R is in Y .

We conclude R (Y ) ⊆ Y , and thus µR ⊆ Y . From (♦) we obtain µR ⊆ Y , i.e., any symbolic path τ s satisfies (∃τ, ρ)τ s (τ, ρ), which proves the theorem.

B Proofs of Results from Section 5

We first introduce a definition and prove a lemma. If τ s (τ, ρ) then the concrete execution path can be longer than the symbolic one. We obviously have that τ s (τ, ρ) implies τ s (τ, ρ). We call the partial cover relation, by contrast to the cover relation .

Proof We proceed by coinduction by showing that the set [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF][START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF]. The set X includes all the pairs (τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ such that there is a symbolic path τ s which partially covers (τ, ρ) and τ s |= ϕ ⇒ ⇒ ⇒ ϕ .

We arbitrarily choose (τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ ∈ X. Then, there is τ s such that τ s (τ, ρ) and τ s |= ϕ ⇒ ⇒ ⇒ ϕ . We distinguish the following cases:

(1)

Also, from τ s (τ, ρ), that is, ϕ 0 (τ, ρ), we obtain (hd (τ ), ρ) |= ϕ 0 by (B.1), and thus, (hd (τ ), ρ) |= ϕ∧ϕ (cf. Definition 3.8). Hence (τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ ∈ (3, 4)(X) by using (3). ( 2)

On the other hand, from τ s (τ, ρ), we obtain τ = γ 0 ⇒ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } τ , (γ 0 , ρ) |= ϕ 0 , and τ s (τ , ρ) (♦) (cf. Definition 4.2). Using (♠) and (♦) we have that ((τ , ρ),

Since (τ, ρ), ϕ ⇒ ⇒ ⇒ ϕ ∈ X was chosen arbitrarily it follows that X ⊆ (3, 4)(X), i.e., X is backwards closed w.r.t. [START_REF] Arusoaie | A generic framework for symbolic execution[END_REF][START_REF] Arusoaie | Symbolic execution based on language transformation[END_REF]. By applying the coinduction principle we obtain X ⊆ ν (3, 4).

Proof of Theorem 5.1, Page 25. We start by recalling the theorem:

Let P be a proof tree of an RL formula under SYSTEP. We define a function f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), for ϕ ⇒ ⇒ ⇒ ϕ ∈ P and (τ, ρ) a complete execution path starting from ϕ, that computes a symbolic execution path that partially covers (τ, ρ) and satisfies ϕ ⇒ ⇒ ⇒ ϕ :

Since (τ, ρ) starts from ϕ and T |= ϕ → ϕ , we obtain (hd (τ ), ρ)

Note that γ 0 and ϕ 1 ⇒ ⇒ ⇒ ϕ 2 ∈ S exists because S is total and ϕ is Sderivable. If there is more than one rule ϕ 1 ⇒ ⇒ ⇒ ϕ 2 ∈ S that matches the step γ 0 ⇒ ρ S hd (τ ), then f chooses arbitrarily one of them. We have and(τ , ρ) is a complete execution path starting from ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ). Since τ = γ 0 ⇒ S τ starts from ϕ we have (γ 0 , ρ) |= ϕ. Also, by Definition 3.11 we obtain (γ 0 , ρ) |= ϕ 1 , and thus, (γ 0 , ρ) |= ϕ ∧ ϕ 1 .

In order to show that f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)) satisfies ϕ ⇒ ⇒ ⇒ ϕ we prove that the set [START_REF] Clarke | Hardware verification using ANSI-C programs as a reference[END_REF][START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF]. Let f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ be an arbitrarily chosen pair in X. We distinguish the following cases:

by the definition of proof trees under SYSTEP and (τ , ρ) is a complete execution path starting from ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) by the definition of γ 0 ⇒ ρ

hd (τ ) and (γ 0 , ρ) |= ϕ ∧ ϕ 1 . Since T |= ϕ → ϕ we obtain f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), ϕ ⇒ ⇒ ⇒ ϕ ∈ (9, 10)(X) by [START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF]. Now we have that X is backward closed w.r.t. to [START_REF] Clarke | Hardware verification using ANSI-C programs as a reference[END_REF][START_REF] Clavel | All About Maude -A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic[END_REF]. Using the coinduction principle we obtain X ⊆ ν (9, 10), i.e. f (ϕ

Next, we show that f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)) partially covers (τ, ρ) in order to apply Lemma B.1 and prove our theorem. We prove that the set [START_REF] Ahrendt | The KeY tool[END_REF][START_REF] Cadar | EXE: automatically generating inputs of death[END_REF]. We arbitrarily choose f (ϕ ⇒ ⇒ ⇒ ϕ , (τ, ρ)), (τ, ρ) in Y . We distinguish the following cases:

is in Y it follows that (τ, ρ) starts from ϕ, i.e., (hd (τ ), ρ) |= ϕ. We obtain

Proof We assume w.l.o.g. that var (ϕ 1 )∩var (ϕ 1 , ϕ 2 ) = ∅ (variables in formulas can be renamed if necessary).

By Definition 4.1 we have on the one hand that ϕ 2 ∈ ∆ S (ϕ 1 ), i.e., there is a rule α ϕ l ⇒ ⇒ ⇒ ϕ r ∈ S such that ϕ 2 (∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r (cf. Definition 3.14), and on the other hand that ϕ 2 is satisfiable since ϕ 1 is S-derivable as required by Definition 4.1.

Let us choose ϕ 2 (∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r . Obviously, ϕ 2 ∈ ∆ S (ϕ 1 ). In order to show that ϕ 1 ⇒ s S ϕ 2 is indeed a symbolic execution path (cf. Definition 4.1) we have to prove that ϕ 2 is a symbolic execution path itself, that is, that ϕ 1 is S-derivable and ϕ 2 is satisfiable. Note that for a symbolic execution path consisting of one transition the two above conditions are equivalent.

Hence, we prove that ϕ 2 is satisfiable. For this, we prove the following result:

Let (γ 2 , ρ) be an arbitrary pair such that (γ 2 , ρ) |= ϕ 2 , that is, (γ 2 , ρ) |= (∃var (ϕ l , ϕ r ))(ϕ l ∧ ϕ 1 ) =? ∧ ϕ r . By Definition 3.8, there is a valuation ρ with xρ = xρ for all x ∈ var (ϕ l , ϕ r ) such that (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ ϕ r . Hence, we have (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? and (γ 2 , ρ ) |= ϕ r . Since (ϕ l ∧ ϕ 1 ) =? is a FOL formula then we have ρ |= (ϕ l ∧ ϕ 1 ) =? . By Proposition 3.5, there is γ 0 such that (γ 0 , ρ ) |= (ϕ l ∧ ϕ 1 ), i.e., (γ 0 , ρ ) |= ϕ l and (γ 0 , ρ ) |= ϕ 1 .

From the hypothesis, T |= ϕ 1 → (∃var (ϕ 1 ))ϕ 1 , which implies that (γ 0 , ρ ) |= (∃var (ϕ 1 ))ϕ 1 , where from we obtain a valuation ρ such that xρ = xρ for all x ∈ var (ϕ 1 ) and (γ 0 , ρ ) |= ϕ 1 . Since var (ϕ 1 ) ∩ var (ϕ 1 , ϕ 2 ) = ∅ we can choose ρ (and hence ρ) such that xρ = xρ for x ∈ var (ϕ 1 ) and we obtain (γ 0 , ρ ) |= ϕ 1 .

It follows that (γ 0 , ρ ) |= (ϕ l ∧ ϕ 1 ) and (again, by Proposition 3.5) ρ |= (ϕ l ∧ ϕ 1 ) =? . Since (γ 2 , ρ ) |= ϕ r then (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ ϕ r . Now, we have a valuation ρ with xρ = xρ for all x ∈ var (ϕ l , ϕ r ) such that (γ 2 , ρ ) |= (ϕ l ∧ ϕ 1 ) =? ∧ϕ r . By Definition 3.8 we obtain (γ 2 , ρ) |= (∃var (ϕ l , ϕ r ))(ϕ l ∧ϕ 1 ) =? ∧ϕ r . Hence, (γ 2 , ρ) |= ϕ 2 . Note that (γ 2 , ρ) was arbitrarily chosen, and thus we have the satisfaction relation

Also, ϕ 2 -satisfiable implies that there are γ 2 and ρ 2 such that (γ 2 , ρ 2 ) |= ϕ 2 . Using ♣ we obtain (γ 2 , ρ 2 ) |= ϕ 2 which implies that ϕ 2 is satisfiable too, which proves (♠).

Thus, we conclude that ϕ 1 ⇒ s S ϕ 2 is indeed a symbolic execution path.

There remains to prove

We have to prove that for every execution path τ γ 1 ⇒ S γ 2 , corresponding node in P has no children.

Since ϕ is S-derivable, the rule [der] can be applied to the root of the proof tree P ϕ ⇒ ⇒ ⇒ ∆ {ϕc ⇒ ⇒ ⇒ ϕ c } (ϕ). Recall (cf. proof of Lemma B.4) that the first rule applied in the construction of P ϕc ⇒ ⇒ ⇒ ϕ c is [der] as well.

Thus, for the roots we may apply the same rule in S for building P and

We shall see that this relation will be maintained between the nodes of P and their homomorphic image in P ϕc ⇒ ⇒ ⇒ ϕ c , except the roots (where T |= ϕ → (∃var (ϕ c )ϕ c ), which allowed us above to apply Lemma B.3).

For the rest of the trees we distinguish the following cases (we assume that ϕ ⇒ ⇒ ⇒ ϕ c is the homomorphic image of ϕ ⇒ ⇒ ⇒ ∆ {ϕc ⇒ ⇒ ⇒ ϕ c } (ϕ) in each case):

Any S-derivable ML formula is satisfiable and hence there is (γ, ρ) |= ϕ.

The hypothesis T |= ϕ → (∃var (ϕ c ))ϕ c implies that there is ρ such that (γ, ρ ) |= ϕ c . We may assume w.l.o.g. that var (ϕ) ∩ var (ϕ c , ϕ c ) = ∅, which allows us to consider ρ = ρ and ρ(x) = ρ (x) for all x ∈ var (ϕ c ). It follows that (γ , ρ) |= ϕ c , which together with (γ, ρ) • the rule [der] is applied for ϕ ⇒ ⇒ ⇒ ϕ c , hence ϕ is S-derivable. If ϕ is not satisfiable, then we can apply [impl]. Otherwise, since S is total and T |= ϕ → ϕ , it follows that ϕ is S-derivable and hence [der] can be applied for ϕ ⇒ ⇒ ⇒ ϕ c as well. The conclusion is obtained using the same reasoning to that done for the roots, but using Lemma B.1 instead of Lemma B.3;

Now the proof of the lemma is finished.

We come back to the proof of the theorem. We show that the function f defined in the proof of Theorem 5.1 can be extended to the set of proof trees

tially covers (τ, ρ) by Lemma B.7 and its corollary, and it satisfies ϕ ⇒ ⇒ ⇒ ϕ by Lemma B.6. By Lemma B.1 it follows that (τ, ρ) satisfies ϕ ⇒ ⇒ ⇒ ϕ .

C Proofs of Results from Section 6

Proof of Lemma 6.1, Page 30. We first prove the lemma for X, Y = ∅ and then prove the general case.

for some valuation ρ :

we obtain using Lemma 4.2 (which says that concrete execution steps backward-simulate symbolic ones) that there exists a configuration γ such that (γ, ρ)

Using the hypothesis var (ϕ) ∩ var (ϕ 1 , ϕ 2 ) = ∅ we can choose ρ and ρ such that ρ = ρ .

We thus have γ = πρ = π 1 ρ, meaning that π 1 and π are A-unifiable (cf. Definition 6.1 and Remark 6.1). By Assumption 6.1 we obtain a substitution σ : var (π 1 ) → T Σ (var (π)) ∈ µ(π 1 , π) such that π ∼ = A π 1 σ and such that ρ = ση for some valuation η : Var → T . We extend σ to be the identity over Var \ var (π 1 ), and then η can be chosen to coincide with ρ over Var \ var (π 1 ). Thus, xρ ∼ = A xση for all x ∈ Var . But since ∼ = A is equality in the model T , denoted by "=", we obtain xρ = xση for all x ∈ Var .

To conclude this direction of the proof we show γ ∈ π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ ; specifically, we prove ( †) (γ , η) |= π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ:

• we have obtained (γ , ρ) |= ϕ 2 π 2 ∧ φ 2 above (since ρ = ρ), hence, (i) γ = π 2 ρ = π 2 (ση) = (π 2 σ)η, and ρ = ση |= φ 2 , thus, (ii) η |= φ 2 σ; • we have also obtained (γ, ρ) |= π 1 ∧ φ 1 , thus, ρ = ση |= φ 1 and then (iii) η |= φ 1 σ; • moreover, we have obtained (γ, ρ) |= π ∧ φ, thus, ρ = ση |= φ and then η |= φσ. But σ is the identity everywhere except perhaps on var (π 1 ) and using the hypothesis var (ϕ) ∩ var (ϕ 1 , ϕ 2 ) = ∅ we obtain var (φ) ∩ var (π 1 ) = ∅, thus, σ is the identity over var (φ) and from η |= φσ we obtain (iv) η |= φ.

From (i)-(iv) we obtain ( †) which concludes the proof of the ⊆ inclusion.

Proof of Theorem 6.1, Page 31. γ ∈ ∆ S (ϕ) iff there exists a rule ϕ 1 ⇒ ⇒ ⇒ ϕ 2 ∈ S, with ϕ 1 π 1 ∧ φ 1 , ϕ 2 (∃Y )π 1 ∧ φ 1 , such that γ ∈ ∆ {ϕ 1 ⇒ ⇒ ⇒ ϕ 2 } (ϕ) . Using Lemma 6.1 this happens if and only if γ ∈ (∃X, Y )π 2 σ ∧ φ 1 σ ∧ φ 2 σ ∧ φ for some σ ∈ µ(π 1 , π).

By construction of the symbolic language, the rule α ϕ 1 ⇒ ⇒ ⇒ ϕ 2 ∈ S induces a rule α s (∃L)(π 1 ∧ s ψ) ∧ sat(φ 1 ∧ ψ) ⇒ ⇒ ⇒ (∃L, Y )π 2 ∧ s (φ 2 ∧ φ 1 ∧ ψ) ∈ S s .

The rule α s and substitution σ (N.B. a valuation in T s ) generate the transition ϕ (∃X)π ∧ s φ ⇒ α s (∃X, Y )π 2 ∧ s (φ 2 σ ∧ φ 1 σ ∧ φ) ϕ . That is, ϕ interpreted as an element of T s Cfg s gives rise to a transition in S s to ϕ ∈ T s Cfg s , i.e., ϕ ⇒ S s ϕ .

Hence, γ ∈ ∆ S (ϕ) iff γ ∈ ϕ (now interpreted as an ML formula in the signature of L) for some transition ϕ ⇒ S s ϕ , which proves the theorem.