1525 LABEL:LastPageOct. 31, 2018Apr. 30, 2019

# All-Path Reachability Logic

Andrei Զtefănescua  aGalois, Inc., USA<EMAIL_ADDRESS>bAlexandru Ioan Cuza
University, Romania<EMAIL_ADDRESS>cRuntime
Verification, Inc., USA<EMAIL_ADDRESS>dUniversity of
Illinois at Urbana-Champaign, USA<EMAIL_ADDRESS>eUniversity of
Bucharest, Romania<EMAIL_ADDRESS>,  Stefan Ciobâcăb  ,  Radu
Mereutab,c  ,  Brandon M. Moorec  ,  Grigore RoԷud,c  and  Traian Florin
ԶerbănuԹăc,e

###### Abstract.

This paper presents a language-independent proof system for reachability
properties of programs written in non-deterministic (e.g., concurrent)
languages, referred to as all-path reachability logic. It derives partial-
correctness properties with all-path semantics (a state satisfying a given
precondition reaches states satisfying a given postcondition on all
terminating execution paths). The proof system takes as axioms any
unconditional operational semantics, and is sound (partially correct) and
(relatively) complete, independent of the object language. The soundness has
also been mechanized in Coq. This approach is implemented in a tool for
semantics-based verification as part of the $\mathbb{K}$ framework
(http://kframework.org).

*Most of the present work was done while still being PhD students at the University of Illinois at Urbana-Champaign.

##  1\. Introduction

Operational semantics are easy to define and understand. Giving a language an
operational semantics can be regarded as “implementing” a formal interpreter.
Operational semantics require little formal training, scale up well and, being
executable, can be tested. Thus, operational semantics are typically used as
trusted reference models for the defined languages. Despite these advantages,
operational semantics are rarely used directly for program verification (i.e.,
verifying properties of a given program, rather than performing meta-reasoning
about a given language), because such proofs tend to be low-level and tedious,
as they involve formalizing and working directly with the corresponding
transition system. Hoare or dynamic logics allow higher level reasoning at the
cost of (re)defining the language as a set of abstract proof rules, which are
harder to understand and trust. The state-of-the-art in mechanical program
verification is to develop and prove such language-specific proof systems
sound w.r.t to a trusted operational semantics [1, 2, 3], but that needs to be
done for each language separately.

Defining more semantics for the same language and proving the soundness of one
semantics in terms of another are highly uneconomical tasks where real
programming languages are concerned, often taking several years to complete.
Ideally, we would like to have only one semantics for a language, together
with a generic theory and a set of generic tools and techniques allowing us to
get all the benefits of any other semantics without paying the price of
defining other semantics. Recent work [4, 5, 6, 7] shows this is possible, by
proposing a language-independent proof system which derives program properties
directly from an operational semantics, at the same proof granularity and
compositionality as a language-specific axiomatic semantics. Specifically, it
introduces _(one-path) reachability rules_ , which generalize both operational
semantics reduction rules and Hoare triples, and gives a proof system which
derives new reachability rules (program properties) from a set of given
reachability rules (the language semantics).

However, the existing proof system has a major limitation: it only derives
reachability rules with a _one-path_ semantics, that is, it guarantees a
program property holds on one but not necessarily all execution paths, which
suffices for deterministic languages but not for non-deterministic
(concurrent) languages. Here we remove this limitation, proposing the first
generic all-path reachability proof system for program verification.

Using matching logic [8] as a configuration specification formalism (Section
2), where a pattern $\varphi$ specifies all program configurations that match
it, we first introduce the novel notion of an all-path reachability rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ (Section 3), where $\varphi$
and $\varphi^{\prime}$ are matching logic patterns. Rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ is valid iff any program
configuration satisfying $\varphi$ reaches, on any complete execution path,
some configuration satisfying $\varphi^{\prime}$. This subsumes Hoare-style
partial correctness in non-deterministic languages. We then present a proof
system for deriving an all-path reachability rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ from a set ${\mathcal{}S}$ of
semantics rules (Section 4). ${\mathcal{}S}$ consists of reduction rules
$\varphi_{l}\Rightarrow^{\exists}\varphi_{r}$, where $\varphi_{l}$ and
$\varphi_{r}$ are simple patterns as encountered in operational semantics
(Section 5), which can be non-deterministic. The proof system derives more
general sequents “${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$”,
with ${\mathcal{}A}$ and ${\mathcal{}C}$ two sets of reachability rules.
Intuitively, ${\mathcal{}A}$’s rules (axioms) are already established valid,
and thus can be immediately used. Those in ${\mathcal{}C}$ (circularities) are
only claimed valid, and can be used only after taking execution steps based on
the rules in ${\mathcal{}S}$ or ${\mathcal{}A}$. The most important proof
rules are

$\displaystyle\begin{array}[]{@{}l@{}}\textbf{Step}:\\\
\displaystyle\frac{{\displaystyle\begin{array}[]{@{}l@{}}\models\varphi\rightarrow\bigvee_{\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\
\in\ {\mathcal{}S}}\exists\textit{FreeVars}({\varphi_{l}})\ \varphi_{l}\\\
\models\exists c\
(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])\mathbin{\wedge}\varphi_{r}\rightarrow\varphi^{\prime}\qquad\mbox{
for each }\ \varphi_{l}\Rightarrow^{\exists}\varphi_{r}\ \in\ {\mathcal{}S}\\\
\end{array}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}$
$\displaystyle\begin{array}[]{@{}l@{}}\textbf{Circularity}:\\\\[4.30554pt]
\displaystyle\frac{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{{\mathcal{}C}\cup\\{\varphi\Rightarrow^{\forall}\varphi^{\prime}\\}}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}{{\displaystyle{\mathcal{}S},{{\mathcal{}A}}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}$

Step is the key proof rule which deals with non-determinism: it derives a
sequent where $\varphi$ reaches $\varphi^{\prime}$ in one step on all paths.
The first premise ensures that any configuration satisfying $\varphi$ has
successors, the second that all successors satisfy $\varphi^{\prime}$
($\square$ is the configuration placeholder). Circularity adds the current
goal to ${\mathcal{}C}$ at any point in a proof, and generalizes the various
language-specific axiomatic semantics invariant rules in a language-
independent way (this form was introduced in [4]).

We illustrate on examples how our proof system enables state exploration
(similar to symbolic model-checking), and verification of program properties
(Section 5). We show that our proof system is sound (Section 7) and relatively
complete (Section 8). We describe our implementation of the proof system as
part of the $\mathbb{K}$ framework [9] (Section 6).

#### Contributions

This paper makes the following specific contributions:

  1. (1)

A language-independent proof system for deriving all-path reachability
properties, with (complete) proofs of its soundness and relative completeness;
the soundness result has also been mechanized in Coq, to serve as a foundation
for certifiable verification.

  2. (2)

An implementation of it as part of the $\mathbb{K}$ framework
(http://kframework.org).

An earlier, shorter version of this paper appeared at RTA-TCLA 2014 [10]. The
main differences are the inclusion of proofs for soundness (Section 7), and
relative completeness (Section 8).

##  2\. Topmost Matching Logic

Matching logic [11, 12] is a first-order logic (FOL) variant designed for
specifying and reasoning about structure by means of patterns and pattern
matching. In this section, we briefly recall topmost matching logic [8], a
subset of the full matching logic theory described in [11, 12]. We employ
topmost matching logic to specify and reason about arbitrary program
configurations. For simplicity, we use “matching logic” instead of “topmost
matching logic” in this paper. A matching logic formula, called a pattern, is
a first-order logic (FOL) formula with special predicates, called basic
patterns. A basic pattern is a configuration term with variables. Intuitively,
a pattern specifies both structural and logical constraints: a configuration
satisfies the pattern iff it matches the structure (basic patterns) and
satisfies the constraints.

Matching logic is parametric in a signature and a model of configurations,
making it a prime candidate for expressing state properties in a language-
independent verification framework. The configuration signature can be as
simple as that of IMP (Fig. 2), or as complex as that of the C language [13,
14] (with more than 100 semantic components).

We use basic concepts from multi-sorted first-order logic. Given a signature
$\Sigma$ which specifies the sorts and arities of the function symbols
(constructors or operators) used in configurations, let
$T_{\Sigma}(\textit{Var})$ denote the free $\Sigma$-algebra of terms with
variables in Var. $T_{\Sigma,s}(\textit{Var})$ is the set of $\Sigma$-terms of
sort $s$. A valuation $\rho\\!:\\!\textit{Var}\\!\rightarrow\\!{\mathcal{}T}$
with $\mathcal{}T$ a $\Sigma$-algebra extends uniquely to a (homonymous)
$\Sigma$-algebra morphism
$\rho\\!:\\!T_{\Sigma}(\textit{Var})\\!\rightarrow\\!{\mathcal{}T}$. Many
mathematical structures needed for language semantics have been defined as
$\Sigma$-algebras, including: boolean algebras, natural/integer/rational
numbers, lists, sets, bags (or multisets), maps (e.g., for states, heaps),
trees, queues, stacks, etc.

Let us fix the following: (1) an algebraic signature $\Sigma$, associated to
some desired configuration syntax, with a distinguished sort ${\it Cfg}$, (2)
a sort-wise infinite set Var of variables, and (3) a $\Sigma$-algebra
$\mathcal{}T$, the configuration model, which may but need not be a term
algebra. As usual, ${\mathcal{}T}_{\\!\\!{\it Cfg}}$ denotes the elements of
$\mathcal{}T$ of sort ${\it Cfg}$, called configurations.

[[8]] A matching logic formula, or a pattern, is a first-order logic (FOL)
formula which additionally allows terms in $T_{\Sigma,{\it
Cfg}}(\textit{Var})$, called basic patterns, as predicates. A pattern is
structureless if it contains no basic patterns.

We define satisfaction $({\gamma},{\rho})\models{\varphi}$ over configurations
$\gamma\\!\in\\!{{\mathcal{}T}_{\\!\\!{\it Cfg}}}$, valuations
$\rho\\!:\\!\textit{Var}\\!\rightarrow\\!{\mathcal{}T}$ and patterns $\varphi$
as follows (among the FOL constructs, we only show $\exists$):

$\begin{array}[]{l}({\gamma},{\rho})\models{\exists X\ \varphi}\ \ \mbox{iff}\
\ ({\gamma},{\rho^{\prime}})\models{\varphi}\mbox{ \ for some
$\rho^{\prime}\\!:\\!\textit{Var}\\!\rightarrow\\!{\mathcal{}T}$}\ \mbox{with
$\rho^{\prime}(y)=\rho(y)$ for all $y\in\textit{Var}\backslash X$
}\\\\[-1.29167pt]
\\!\hbox{\pagecolor{Grey}\\!$\begin{array}[]{@{}lcl}({\gamma},{\rho})\models{\pi}&\,\mbox{\
\ \ \ \ \, iff}&\gamma=\rho(\pi)\end{array}$ \\!\\!\\!}\mbox{\ \ \ \ where
$\pi\in T_{\Sigma,{\it Cfg}}(\textit{Var})$}\\\ \end{array}$

We write $\models\varphi$ when $({\gamma},{\rho})\models{\varphi}$ for all
$\gamma\in{\mathcal{}T}_{{\it Cfg}}$ and all
$\rho:\textit{Var}\rightarrow{\mathcal{}T}$.

A basic pattern $\pi$ is satisfied by all the configurations $\gamma$ that
_match_ it; in $({\gamma},{\rho})\models{\\!\pi}$ the $\rho$ can be thought of
as the “witness” of the matching, and can be further constrained in a pattern.
For instance, the pattern from Section 5

$\langle{\tt x\\!:=\\!x\\!+\\!1\ ||\ x\\!:=\\!x\\!+\\!1},\ {{\tt
x}\\!\mapsto\\!n}\rangle\mathbin{\wedge}(n=0\mathbin{\vee}n=1)$

is matched by the configurations with code “${\tt x\\!:=\\!x\\!+\\!1\ ||\
x\\!:=\\!x\\!+\\!1}$” and state mapping program variable x into integer $n$
with $n$ being either $0$ or $1$. We use italic for mathematical variables in
Var and typewriter for program variables (program variables are represented in
matching logic as constants of sort ${\it PVar}$, see Section 5).

The “topmost” matching logic variant that we use in this paper is a fragment
of the general matching logic approach proposed in [11, 12], where terms are
regarded as predicates only at the top level, where they have the sort ${\it
Cfg}$. The general matching logic approach in [11, 12] allows the distinctive
terms-as-predicates view as well as the mix of logical and structural
constraints at all levels, for any terms of any sorts. As an example, the
pattern above may be equivalently written as

$\langle{\tt x\\!:=\\!x\\!+\\!1\ ||\ x\\!:=\\!x\\!+\\!1},\ {{\tt
x}\\!\mapsto\\!n\mathbin{\wedge}(n=0\mathbin{\vee}n=1)}\rangle$

thus localizing the logical constraints to the actual place in the
configuration where they matter. We remind the reader that in this paper we
limit ourselves to “topmost” matching logic, and that we take the freedom to
drop the “topmost” and just call it “matching logic”.

Next, we recall how matching logic formulae can be translated into FOL
formulae, so that its satisfaction becomes FOL satisfaction in the model of
configurations, $\mathcal{}T$. Then, we can use conventional theorem provers
or proof assistants for pattern reasoning.

[[8]] Let $\square$ be a fresh ${\it Cfg}$ variable. For a pattern $\varphi$,
let $\varphi^{\square}$ be the FOL formula formed from $\varphi$ by replacing
basic patterns $\pi\in{\mathcal{}T}_{\\!\\!\Sigma,{\it Cfg}}(\textit{Var})$
with equalities $\square=\pi$. If
$\rho\\!:\\!\textit{Var}\\!\rightarrow\\!{\mathcal{}T}$ and
$\gamma\\!\in\\!{\mathcal{}T}_{\\!\\!{\it Cfg}}$ then let the valuation
$\rho^{\gamma}:\textit{Var}\cup\\{\square\\}\rightarrow{\mathcal{}T}$ be such
that $\rho^{\gamma}(x)=\rho(x)$ for $x\in\textit{Var}$ and
$\rho^{\gamma}(\square)=\gamma$.

With the notation in Definition 2, $({\gamma},{\rho})\models{\varphi}$ iff
$\rho^{\gamma}\models\varphi^{\square}$, and $\models\varphi$ iff
${\mathcal{}T}\models\varphi^{\square}$. Thus, matching logic is a
methodological fragment of the FOL theory of ${\mathcal{}T}$. We drop
$\square$ from $\varphi^{\square}$ when it is clear in context that we mean
the FOL formula instead of the matching logic pattern. It is often technically
convenient to eliminate $\square$ from $\varphi$, by replacing $\square$ with
a ${\it Cfg}$ variable c and using ${\varphi}[{\textit{c}}/\square]$ instead
of $\varphi$. We use the FOL representation in the Step proof rule in Fig. 1,
and to establish relative completeness in Section 8.

##  3\. Specifying Reachability

In this section we define one-path and all-path reachability. We begin by
recalling some matching logic reachability [6] notions that we need for
specifying reachability.

[[6]] A (one-path) reachability rule is a pair
$\varphi\Rightarrow^{\exists}\varphi^{\prime}$, where $\varphi$ and
$\varphi^{\prime}$ are patterns (which can have free variables). Rule
$\varphi\Rightarrow^{\exists}\varphi^{\prime}$ is weakly well-defined iff for
any $\gamma\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$ and
$\rho:\textit{Var}\rightarrow{\mathcal{}T}$ with
$({\gamma},{\rho})\models{\varphi}$, there exists
$\gamma^{\prime}\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$ with
$({\gamma^{\prime}},{\rho})\models{\varphi^{\prime}}$. A reachability system
is a set of reachability rules. Reachability system ${\mathcal{}S}$ is weakly
well-defined iff each rule is weakly well-defined. ${\mathcal{}S}$ induces a
transition system
$({\mathcal{}T},\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}})$ on the
configuration model:
$\gamma\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma^{\prime}$ for
$\gamma,\gamma^{\prime}\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$ iff there is some
rule $\varphi\Rightarrow^{\exists}\varphi^{\prime}$ in ${\mathcal{}S}$ and
some valuation $\rho:\textit{Var}\rightarrow{\mathcal{}T}$ with
$({\gamma},{\rho})\models{\varphi}$ and
$({\gamma^{\prime}},{\rho})\models{\varphi^{\prime}}$. A
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path is a finite
sequence
$\gamma_{0}\\!\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\\!\gamma_{1}\\!\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\\!...\\!\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\\!\gamma_{n}$
with $\gamma_{0},\\!...,\\!\gamma_{n}\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$. A
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path is complete iff it
is not a strict prefix of any other
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path.

We assume an operational semantics is a set of (unconditional) reduction rules
“$l\Rightarrow^{\exists}r\ {\sf if}\ b$”, where $l,r\in T_{\Sigma,{\it
Cfg}}(\textit{Var})$ are program configurations with variables and $b\in
T_{\Sigma,{\it Bool}}(\textit{Var})$ is a condition constraining the variables
of $l,r$. Styles of operational semantics using only such (unconditional)
rules include evaluation contexts [15], the chemical abstract machine [16] and
$\mathbb{K}$ [9] (see Section 5 for an evaluation contexts semantics). Several
large languages have been given semantics in such styles, including C [13]
(more than 3000 rules) and R5RS Scheme [17]. The reachability proof system
works with any set of rules of this form, being agnostic to the particular
style of semantics.

Such a rule “$l\Rightarrow^{\exists}r\ {\sf if}\ b$” states that a ground
configuration $\gamma$ which is an instance of $l$ and satisfies the condition
$b$ reduces to an instance $\gamma^{\prime}$ of $r$. Matching logic can
express terms with constraints: $l\mathbin{\wedge}b$ is satisfied by exactly
the $\gamma$ above. Thus, we can regard such a semantics as a particular
weakly well-defined reachability system ${\mathcal{}S}$ with rules of the form
“$l\mathbin{\wedge}b\Rightarrow^{\exists}r$”. The weakly well-defined
condition on ${\mathcal{}S}$ guarantees that if $\gamma$ matches the left-
hand-side of a rule in ${\mathcal{}S}$, then the respective rule induces an
outgoing transition from $\gamma$. The transition system induced by
${\mathcal{}S}$ describes precisely the behavior of any program in any given
state. In [6, 5, 4] we show that reachability rules capture one-path
reachability properties and Hoare triples for deterministic languages.

Formally, let us fix an operational semantics given as a reachability system
${\mathcal{}S}$. Then, we can specify reachability in the transition system
induced by ${\mathcal{}S}$, both all-path and one-path, as follows:

An all-path reachability rule is a pair
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ of patterns $\varphi$ and
$\varphi^{\prime}$.

An all-path reachability rule $\varphi\Rightarrow^{\forall}\varphi^{\prime}$
is satisfied,
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$, iff for
all complete $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-paths
$\tau$ starting with $\gamma\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$ and for all
$\rho:\textit{Var}\rightarrow{\mathcal{}T}$ such that
$({\gamma},{\rho})\models{\varphi}$, there exists some
$\gamma^{\prime}\in\tau$ such that
$({\gamma^{\prime}},{\rho})\models{\varphi^{\prime}}$.

A one-path reachability rule $\varphi\Rightarrow^{\exists}\varphi^{\prime}$ is
satisfied, ${\mathcal{}S}\models\varphi\Rightarrow^{\exists}\varphi^{\prime}$,
iff for all $\gamma\in{\mathcal{}T}_{\\!\\!{\it Cfg}}$ and
$\rho:\textit{Var}\rightarrow{\mathcal{}T}$ such that
$({\gamma},{\rho})\models{\varphi}$, there is either a
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path from $\gamma$ to
some $\gamma^{\prime}$ such that
$({\gamma^{\prime}},{\rho})\models{\varphi^{\prime}}$, or there is a diverging
execution
$\gamma\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma_{1}\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma_{2}\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\cdots$
from $\gamma$.

The racing increment example in Section 5 can be specified by

$\langle{\tt x\\!:=\\!x\\!+\\!1\ ||\ x\\!:=\\!x\\!+\\!1},\ {{\tt
x}\\!\mapsto\\!m}\rangle\Rightarrow^{\forall}\exists n\ (\langle{\text{\tt
skip}},\ {{\tt x}\\!\mapsto\\!n}\rangle\mathbin{\wedge}(n=m+_{\it
Int}1\mathbin{\vee}n=m+_{\it Int}2)$

which states that every terminating execution reaches a state where execution
of both threads is complete and the value of ${\tt x}$ has increased by $1$ or
$2$ (this code has a race).

A Hoare triple describes the resulting state after execution finishes, so it
corresponds to a reachability rule where the right side contains no remaining
code. However, all-path reachability rules are strictly more expressive than
Hoare triples, as they can also specify intermediate configurations (the code
in the right-hand-side need not be empty). Reachability rules provide a
unified representation for both language semantics and program specifications:
$\varphi\Rightarrow^{\exists}\varphi^{\prime}$ for semantics and
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ for all-path reachability
specifications. Note that, like Hoare triples, reachability rules can only
specify properties of complete paths (that is, terminating execution paths).
One can use existing Hoare logic techniques to break reasoning about a non-
terminating program into reasoning about its terminating components.

##  4\. Reachability Proof System

$\begin{array}[]{@{}l@{\hspace*{-15ex}}r@{}}\begin{array}[]{@{}l@{}}\textbf{Step}:\\\
\displaystyle\frac{{\displaystyle\begin{array}[]{@{}l@{}}\models\varphi\rightarrow\bigvee_{\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\
\in\ {\mathcal{}S}}\exists\textit{FreeVars}({\varphi_{l}})\ \varphi_{l}\\\
\models\exists c\
(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])\mathbin{\wedge}\varphi_{r}\rightarrow\varphi^{\prime}\qquad\mbox{
for each }\ \varphi_{l}\Rightarrow^{\exists}\varphi_{r}\ \in\ {\mathcal{}S}\\\
\end{array}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}&\begin{array}[]{@{}l@{}}\textbf{Axiom}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle\varphi\Rightarrow^{\forall}\varphi^{\prime}\
\ \in\ {\mathcal{}A}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}\\\\[19.37492pt]
\begin{array}[]{@{}l@{}}\textbf{Reflexivity}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle\cdot}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\varphi}\Rightarrow^{\forall}{\varphi}}}\end{array}&\begin{array}[]{@{}l@{}}\textbf{Transitivity}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}}\Rightarrow^{\forall}{\varphi_{2}}\qquad{\mathcal{}S},{{\mathcal{}A}\cup{\mathcal{}C}}\
\mathrel{\vdash}{\varphi_{2}}\Rightarrow^{\forall}{\varphi_{3}}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}}\Rightarrow^{\forall}{\varphi_{3}}}}\\\
\end{array}\\\\[19.37492pt] \begin{array}[]{@{}l@{}}\textbf{Case
Analysis}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}}\Rightarrow^{\forall}{\varphi}\qquad{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{2}}\Rightarrow^{\forall}{\varphi}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}\mathbin{\vee}\varphi_{2}}\Rightarrow^{\forall}{\varphi}}}\\\
\end{array}&\begin{array}[]{@{}l@{}}\textbf{Abstraction}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}\qquad
X\cap\textit{FreeVars}({\varphi^{\prime}})=\emptyset}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\exists X\
\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}\\\\[19.37492pt]
\begin{array}[]{@{}l@{}}\textbf{Consequence}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle\models\varphi_{1}\rightarrow\varphi_{1}^{\prime}\qquad\
{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}^{\prime}}\Rightarrow^{\forall}{\varphi_{2}^{\prime}}\qquad\models\varphi_{2}^{\prime}\rightarrow\varphi_{2}}}{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi_{1}}\Rightarrow^{\forall}{\varphi_{2}}}}\end{array}&\begin{array}[]{@{}l@{}}\textbf{Circularity}:\\\\[3.87498pt]
\displaystyle\frac{{\displaystyle{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{{\mathcal{}C}\cup\\{\varphi\Rightarrow^{\forall}\varphi^{\prime}\\}}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}{{\displaystyle{\mathcal{}S},{{\mathcal{}A}}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}}}\end{array}\\\
\end{array}$ Figure 1.  Proof system for reachability. We make the standard
assumption that the free variables of
$\varphi_{l}\Rightarrow^{\exists}\varphi_{r}$ in the Step proof rule are fresh
(e.g., disjoint from those of $\varphi\Rightarrow^{\forall}\varphi^{\prime}$).

Fig. 1 shows our novel proof system for all-path reachability. The target
language is given as a weakly well-defined reachability system
${\mathcal{}S}$. The soundness result (Thm. 1) guarantees that
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ if
${\mathcal{}S}\
\mathrel{\vdash}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$ is
derivable. Note that the proof system derives more general sequents of the
form ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$,
where ${\mathcal{}A}$ and ${\mathcal{}C}$ are sets of reachability rules. The
rules in ${\mathcal{}A}$ are called axioms and rules in ${\mathcal{}C}$ are
called circularities. If either ${\mathcal{}A}$ or ${\mathcal{}C}$ does not
appear in a sequent, it means the respective set is empty: ${\mathcal{}S}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$
is a shorthand for ${\mathcal{}S},{\emptyset}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$,
and ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$ is a
shorthand for ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\emptyset}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$,
and ${\mathcal{}S}\
\mathrel{\vdash}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$ is a
shorthand for ${\mathcal{}S},{\emptyset}\
\mathrel{\vdash}_{\emptyset}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$.
Initially, both ${\mathcal{}A}$ and ${\mathcal{}C}$ are empty. Note that
“$\rightarrow$” in Step and Consequence denotes logical implication.

The intuition is that the reachability rules in ${\mathcal{}A}$ can be assumed
valid, while those in ${\mathcal{}C}$ have been postulated but not yet
justified. After making progress from $\varphi$ (at least one derivation by
Step or by Axiom with the rules in ${\mathcal{}A}$), the rules in
${\mathcal{}C}$ become (coinductively) valid (can be used in derivations by
Axiom). During the proof, circularities can be added to ${\mathcal{}C}$ via
Circularity, flushed into ${\mathcal{}A}$ by Transitivity, and used via Axiom.
The desired semantics for sequent ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$
(read “${\mathcal{}S}$ with axioms ${\mathcal{}A}$ and circularities
$\mathcal{}C$ proves $\varphi\Rightarrow^{\forall}\varphi^{\prime}$”) is:
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ holds if the rules in
${\mathcal{}A}$ hold and those in ${\mathcal{}C}$ hold after taking at least
one step from $\varphi$ in the transition system
$(\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}},{\mathcal{}T})$, and if
${\mathcal{}C}\neq\emptyset$ then $\varphi$ reaches $\varphi^{\prime}$ after
at least one step on all complete paths. As a consequence of this definition,
any rule $\varphi\Rightarrow^{\forall}\varphi^{\prime}$ derived by Circularity
has the property that $\varphi$ reaches $\varphi^{\prime}$ after at lest one
step, due to Circularity having a prerequisite ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{{\mathcal{}C}\cup\\{\varphi\Rightarrow^{\forall}\varphi^{\prime}\\}}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$
(with a non-empty set of circularities). We next discuss the proof rules.

Step derives a sequent where $\varphi$ reaches $\varphi^{\prime}$ in one step
on all paths. The first premise ensures any configuration matching $\varphi$
matches the left-hand-side $\varphi_{l}$ of some rule in ${\mathcal{}S}$ and
thus, as ${\mathcal{}S}$ is weakly well-defined, can take a step. Formally, if
$({\gamma},{\rho})\models{\varphi}$, then there exists some rule
$\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$ and some
valuation $\rho^{\prime}$ of the free variables of $\varphi_{l}$ such that
$({\gamma},{\rho^{\prime}})\models{\varphi_{l}}$, and thus $\gamma$ has at
least one $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-successor
generated by the rule $\varphi_{l}\Rightarrow^{\exists}\varphi_{r}$. The
second premise ensures that each
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-successor of a
configuration matching $\varphi$ matches $\varphi^{\prime}$. Formally, if
$\gamma\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma^{\prime}$ and
$\gamma$ matches $\varphi$ then there is some rule
$\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$ and
$\rho:\textit{Var}\rightarrow{\mathcal{}T}$ such that
$({\gamma},{\rho})\models{\varphi\land\varphi_{l}}$ and
$({\gamma^{\prime}},{\rho})\models{\varphi_{r}}$; then the second premise
implies $\gamma^{\prime}$ matches $\varphi^{\prime}$.

Designing a proof rule for deriving an execution step along all paths is non-
trivial. For instance, one might expect Step to require as many premises as
there are transitions going out of $\varphi$, as is the case for the examples
presented later in this paper. However, that is not possible, as the number of
successors of a configuration matching $\varphi$ may be unbounded even if each
matching configuration has a finite branching factor in the transition system.
Step avoids this issue by requiring only one premise for each rule by which
some configuration $\varphi$ can take a step, even if that rule can be used to
derive multiple transitions. To illustrate this situation, consider a language
defined by
${\mathcal{}S}\equiv\\{\langle{n_{1}}\rangle\mathbin{\wedge}n_{1}>_{\it
Int}n_{2}\Rightarrow^{\exists}\langle{n_{2}}\rangle\\}$, with $n_{1}$ and
$n_{2}$ non-negative integer variables. A configuration in this language is a
singleton with a non-negative integer. Intuitively, a positive integer
transits into a strictly smaller non-negative integer, in a non-deterministic
way. The branching factor of a non-negative integer is its value. Then
${\mathcal{}S}\models\langle{m}\rangle\Rightarrow^{\forall}\langle{0}\rangle$.
Deriving it reduces (by Circularity and other proof rules) to deriving
$\langle{m_{1}}\rangle\mathbin{\wedge}m_{1}>_{\it
Int}0\Rightarrow^{\forall}\exists m_{2}\
(\langle{m_{2}}\rangle\mathbin{\wedge}m_{1}>_{\it Int}m_{2})$. The left-hand-
side is matched by any positive integer, and thus its branching factor is
infinity. Deriving this rule with Step requires only two premises,
$\models(\langle{m_{1}}\rangle\mathbin{\wedge}m_{1}>_{\it
Int}0)\rightarrow\exists n_{1}n_{2}\
(\langle{n_{1}}\rangle\mathbin{\wedge}n_{1}>_{\it Int}n_{2})$ and
$\models\exists\textit{c}\
(\textit{c}=\langle{m_{1}}\rangle\mathbin{\wedge}m_{1}>_{\it
Int}0\mathbin{\wedge}\textit{c}=\langle{n_{1}}\rangle\mathbin{\wedge}n_{1}>_{\it
Int}n_{2})\mathbin{\wedge}\langle{n_{2}}\rangle\rightarrow\exists m_{2}\
(\langle{m_{2}}\rangle\mathbin{\wedge}m_{1}>_{\it Int}m_{2})$. A similar
situation arises in real life for languages with thread pools of arbitrary
size.

Axiom applies a trusted rule. Reflexivity and Transitivity capture the
corresponding closure properties of the reachability relation. Reflexivity
requires ${\mathcal{}C}$ to be empty to ensure that all-path rules derived
with non-empty ${\mathcal{}C}$ take at least one step. Transitivity enables
the circularities as axioms for the second premise, since if ${\mathcal{}C}$
is not empty, the first premise is guaranteed to take at least one step.
Consequence, Case Analysis and Abstraction are adapted from Hoare logic.
Ignoring circularities, these seven rules discussed so far constitute formal
infrastructure for symbolic execution.

Circularity has a coinductive nature, allowing us to make new circularity
claims. We typically make such claims for code with repetitive behaviors, such
as loops, recursive functions, jumps, etc. If there is a derivation of the
claim using itself as a circularity, then the claim holds. This would
obviously be unsound if the new assumption was available immediately, but
requiring progress (taking at least one step in the transition system
$({\mathcal{}T},\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}})$) before
circularities can be used ensures that only diverging executions can
correspond to endless invocation of a circularity.

One important aspect of concurrent program verification, which we do not
address in this paper, is proof compositionality. Our focus here is limited to
establishing a sound and complete language-independent proof system for all-
path reachability rules, to serve as a foundation for further results and
applications, and to discuss our current implementation of it. We only mention
that we have already studied proof compositionality for earlier one-path
variants of reachability logic [5], showing that there is a mechanical way to
translate any Hoare logic proof derivation into a reachability proof of
similar size and structure, but based entirely on the operational semantics of
the language. The overall conclusion of our previous study, which we believe
will carry over to all-path reachability, was that compositional reasoning can
be achieved methodologically using our proof system, by proving and then using
appropriate reachability rules as lemmas. However, note that this works only
for theoretically well-behaved languages which enjoy a compositional
semantics. For example, a language whose semantics assumes a bounded heap
size, or which has constructs whose semantics involve the entire program,
e.g., call/cc, will lack compositionality.

##  5\. Verifying Programs

$\begin{array}[]{|l|}\hline\cr\begin{array}[]{@{}c|c@{}}\begin{array}[]{rcl}\lx@intercol\hbox{\pagecolor{Grey}{\rm
IMP} language syntax}\hfil\lx@intercol\\\ {\it PVar}&\Coloneqq&\mbox{program
variables}\\\ {\it Exp}&\Coloneqq&{\it PVar}\hskip 0.75pt\ \ \mid\ \ {\it
Int}\ \ \mid\ \ {\it Exp}\ {\tt op}\ {\it Exp}\\\ {\it Stmt}&\Coloneqq&{\tt
skip}\ \ \mid\ \ {\it PVar}\ {\tt:=}\ {\it Exp}\\\ &\mid&{\it Stmt}{\tt;}\
{\it Stmt}\ \ \mid\ \ {\it Stmt}\ {\tt||}\ {\it Stmt}\\\ &\mid&{\tt if}({\it
Exp})\ {\it Stmt}\ {\tt else}\ {\it Stmt}\\\ &\mid&{\tt while}({\it Exp})\
{\it Stmt}\\\
\end{array}\par&\begin{array}[]{rcl}\lx@intercol\hbox{\pagecolor{Grey}{\rm
IMP} evaluation contexts syntax}\hfil\lx@intercol\\\
\textit{Context}&\Coloneqq&\rule{5.69054pt}{5.69054pt}\\\
&\mid&\langle{\textit{Context}},\ {{\it State}}\rangle\\\
&\mid&\textit{Context}\ {\tt op}\ {\it Exp}\ \ \mid\ \ {\it Int}\ {\tt op}\
\textit{Context}\\\ &\mid&{\it PVar}\ {\tt:=}\ \textit{Context}\\!\\!\ \ \mid\
\ \textit{Context}{\tt;}\ {\it Stmt}\\\ &\mid&\textit{Context}\ {\tt||}\ {\it
Stmt}\ \hskip 1.5pt\ \ \mid\ \ \ {\it Stmt}\ {\tt||}\ \textit{Context}\\\
&\mid&{\tt if}(\textit{Context})\ {\it Stmt}\ {\tt else}\ {\it Stmt}\\\
\end{array}\par\end{array}\par\\\
\hline\cr\begin{array}[]{ll@{\qquad}ll}\lx@intercol\hbox{\pagecolor{Grey}{\rm
IMP} operational semantics}\hfil\lx@intercol\\\ \textbf{lookup}&\langle{C},\
{\sigma}\rangle[x]\Rightarrow^{\exists}\langle{C},\
{\sigma}\rangle[\sigma(x)]&\textbf{op}&i_{1}\,{\tt
op}\,i_{2}\Rightarrow^{\exists}i_{1}\,{\it op}_{\it Int}\,i_{2}\\\
\textbf{asgn}&\langle{C},\
{\sigma}\rangle[x\,{\tt:=}\,i]\Rightarrow^{\exists}\langle{C},\
{\sigma[x\leftarrow i]}\rangle[{\tt skip}]&\textbf{seq}&{\tt
skip}{\tt;}\,s\Rightarrow^{\exists}s\\\ \textbf{cond}_{1}&{\tt
if}(i)\,\,s_{1}\,{\tt else}\,s_{2}\Rightarrow^{\exists}s_{1}\qquad\textsf{if}\
\ i\neq 0&\textbf{cond}_{2}&{\tt if}(0)\,s_{1}\,{\tt
else}\,s_{2}\Rightarrow^{\exists}s_{2}\\\ \textbf{while}&{\tt
while}(e)\,s\Rightarrow^{\exists}{\tt if}(e)\,s{\tt;}\,{\tt while}(e)\,s\,{\tt
else}\ {\tt skip}&\textbf{finish}&{\tt skip\ ||\
skip}\Rightarrow^{\exists}{\tt skip}\end{array}\par\\\ \hline\cr\end{array}$
Figure 2. IMP language syntax and operational semantics based on evaluation
contexts.

In this section we show a few examples of using our proof system to verify
programs based on an operational semantics. In a nutshell, the proof system
enables generic symbolic execution combined with circular reasoning. Symbolic
execution is achieved by rewriting modulo domain reasoning.

First, we introduce a simple parallel imperative language, IMP. Fig. 2 shows
its syntax and an operational semantics based on evaluation contexts [15] (we
choose evaluation contexts for presentation purposes only). IMP has only
integer expressions. When used as conditions of if and while, zero means false
and any non-zero integer means true (like in C). Expressions are formed with
integer constants, program variables, and conventional arithmetic constructs.
Arithmetic operations are generically described as op. IMP statements are
assignment, if, while, sequential composition and parallel composition. IMP
has shared memory parallelism without explicit synchronization. The examples
use the parallel construct only at the top-level of the programs. The second
example shows how to achieve synchronization using the existing language
constructs.

The program configurations of IMP are pairs $\langle{\tt code},\
{\sigma}\rangle$, where code is a program fragment and $\sigma$ is a state
term mapping program variables into integers. As usual, we assume appropriate
definitions for the integer and map domains available, together with
associated operations like arithmetic operations ($i_{1}\,{\it op}_{\it
Int}\,i_{2}$, etc.) on the integers and lookup ($\sigma(x)$) and update
($\sigma[x\leftarrow i]$) on the maps. We also assume a context domain with a
plugging operation ($C[t]$) that composes a context and term back into a
configuration. A configuration context consists of a code context and a state.
The definition in Fig. 2 consists of eight reduction rules between program
configurations, which make use of first-order variables: $x$ is a variable of
sort ${\it PVar}$; $e$ is a variable of sort ${\it Exp}$; $s,s_{1},s_{2}$ are
variables of sort ${\it Stmt}$; $i,i_{1},i_{2}$ are variables of sort ${\it
Int}$; $\sigma$ is a variable of sort ${\it State}$; $C$ is a variable of sort
Context. A rule reduces a configuration by splitting it into a context and a
redex, rewriting the redex and possibly the context, and then plugging the
resulting term into the resulting context. As an abbreviation, a context is
not mentioned if not used; e.g., the rule op is in full $\langle{C},\
{\sigma}\rangle[i_{1}\,{\tt op}\,i_{2}]\Rightarrow^{\exists}\langle{C},\
{\sigma}\rangle[i_{1}\,{\it op}_{\it Int}\,i_{2}]$. For example, configuration
$\langle{{\tt x:=}\,(2+5)-4},\ {\sigma}\rangle$ reduces to $\langle{{\tt
x:=}\,7-4},\ {\sigma}\rangle$ by applying the ${\bf op}_{+}$ rule with
$C\equiv{\tt x:=}\,\rule{5.69054pt}{5.69054pt}-4$, $\sigma\equiv\sigma$,
$i_{1}\equiv 2$ and $i_{2}\equiv 5$. We can regard the operational semantics
of IMP above as a set of reduction rules of the form
“$l\Rightarrow^{\exists}r\ {\sf if}\ b$”, where $l$ and $r$ are program
configurations with variables constrained by boolean condition $b$. As
discussed in Section 3, our proof system works with any rules of this form.

${{\left\langle{}^{\text{\tt x}:=\text{\tt x}+1\mathop{\mathbf{||}}\text{\tt
x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=\text{\tt
x}+1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=\text{\tt
x}+1\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=\text{\tt
x}+1\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1+1\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}1,}_{\text{\tt x}\mapsto
m}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}2\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m+_{\it Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}1,}_{\text{\tt x}\mapsto
m+_{\it Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}1+1,}_{\text{\tt x}\mapsto
m+_{\it Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt x}:=m+_{\it Int}2,}_{\text{\tt x}\mapsto
m+_{\it Int}1}\right\rangle}}$${{\left\langle{}^{\text{\tt
skip}\mathop{\mathbf{||}}\text{\tt skip},}_{\text{\tt x}\mapsto m+_{\it
Int}2}\right\rangle}}$ Figure 3. State space of the racing increment example

Next, we illustrate the proof system on a few examples. The first example
shows that our proof system enables exhaustive state exploration, similar to
symbolic model-checking but based on the operational semantics. Although
humans prefer to avoid such explicit proofs and instead methodologically use
abstraction or compositional reasoning whenever possible (and such
methodologies are not excluded by our proof system), a complete proof system
must nevertheless support them. The code ${\tt x}\\!:=\\!{\tt x}\\!+\\!1\ ||\
{\tt x}\\!:=\\!{\tt x}\\!+\\!1$ exhibits a race on ${\tt x}$: the value of
${\tt x}$ increases by $1$ when both reads happen before either write, and by
$2$ otherwise. The all-path rule that captures this behavior is

$\langle{{\tt x}\\!:=\\!{\tt x}\\!+\\!1\ ||\ {\tt x}\\!:=\\!{\tt x}\\!+\\!1},\
{{\tt x}\\!\mapsto\\!m}\rangle\Rightarrow^{\forall}\exists n\ (\langle{\tt
skip},\ {{\tt x}\\!\mapsto\\!n}\rangle\mathbin{\wedge}(n=m+_{\it
Int}1\mathbin{\vee}n=m+_{\it Int}2)$

We show that the program has exactly these behaviors by deriving this rule in
the proof system. Call the right-hand-side pattern $G$. The proof contains
subproofs of $c\Rightarrow^{\forall}G$ for every reachable configuration $c$,
tabulated in Fig. 3. The subproofs for $c$ matching $G$ use Reflexivity and
Consequence, while the rest use Transitivity, Step, and Case Analysis to
reduce to the proofs for the next configurations. For example, the proof
fragment below shows how $\langle{{\tt x}:=m+1\mathop{\mathbf{||}}{\tt
x}:={\tt x}+1},\ {{\tt x}\mapsto m}\rangle\Rightarrow^{\forall}G$ reduces to
$\langle{{\tt x}:=m+_{\it Int}1\mathop{\mathbf{||}}{\tt x}:={\tt x}\\!+\\!1},\
{{\tt x}\mapsto m}\rangle\Rightarrow^{\forall}G$ and $\langle{{\tt
x}:=m\\!+\\!1\mathop{\mathbf{||}}{\tt x}:=m\\!+\\!1},\ {{\tt x}\mapsto
m}\rangle\Rightarrow^{\forall}G$:

$\displaystyle\displaystyle{\hbox{\hskip
147.64502pt\vbox{\hbox{\hskip-147.645pt\hbox{\hbox{$\displaystyle\displaystyle{\raise
16.69pt\hbox{$\displaystyle\hbox{$\displaystyle\hbox{\small\small{{Step}}}\;$}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
5.25pt\vbox{\hbox{\hskip-5.25pt\hbox{\hbox{$\displaystyle\displaystyle...$}}}\vbox{}}}\over\hbox{\hskip
65.64308pt\vbox{\vbox{}\hbox{\hskip-65.64307pt\hbox{\hbox{$\displaystyle\displaystyle\mbox{$\displaystyle\begin{array}[]{rl}{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}\Rightarrow^{\forall}&{\left\langle{}^{\text{\tt x}:=m+_{\it
Int}1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}\\\ \lor&{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}\end{array}$}$}}}}}}$}}\hbox{}$}\hskip 9.00002pt\raise
11.345pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
67.5019pt\vbox{\hbox{\hskip-67.5019pt\hbox{\hbox{$\displaystyle\displaystyle\raise
11.345pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
5.25pt\vbox{\hbox{\hskip-5.25pt\hbox{\hbox{$\displaystyle\displaystyle...$}}}\vbox{}}}\over\hbox{\hskip
34.22966pt\vbox{\vbox{}\hbox{\hskip-34.22966pt\hbox{\hbox{$\displaystyle\displaystyle{\left\langle{}^{\text{\tt
x}:=m+_{\it Int}1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt
x}\mapsto
m}\right\rangle}\\!\\!\Rightarrow^{\forall}\\!G$}}}}}}$}}\hbox{}$}\raise
11.345pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
5.25pt\vbox{\hbox{\hskip-5.25pt\hbox{\hbox{$\displaystyle\displaystyle...$}}}\vbox{}}}\over\hbox{\hskip
33.27225pt\vbox{\vbox{}\hbox{\hskip-33.27223pt\hbox{\hbox{$\displaystyle\displaystyle{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}\\!\\!\Rightarrow^{\forall}\\!G$}}}}}}$}}\hbox{}$}$}}}\vbox{}}}\over\hbox{\hskip
63.56378pt\vbox{\vbox{}\hbox{\hskip-63.56378pt\hbox{\hbox{$\displaystyle\displaystyle{\left\langle{}^{\text{\tt
x}:=m+_{\it Int}1\mathop{\mathbf{||}}\text{\tt x}:=\text{\tt x}+1,}_{\text{\tt
x}\mapsto m}\right\rangle}\\!\lor\\!{\left\langle{}^{\text{\tt
x}:=m+1\mathop{\mathbf{||}}\text{\tt x}:=m+1,}_{\text{\tt x}\mapsto
m}\right\rangle}\Rightarrow^{\forall}G$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{{CA}}}$\hss}}$}}$}}}\vbox{}}}\over\hbox{\hskip
69.97923pt\vbox{\vbox{}\hbox{\hskip-69.97922pt\hbox{\hbox{$\displaystyle\displaystyle\langle{{\tt
x}:=m+1\mathop{\mathbf{||}}{\tt x}:={\tt x}+1},\ {{\tt x}\mapsto
m}\rangle\Rightarrow^{\forall}G$}}}}}}$ Trans

For the rule hypotheses of Step above, note that all rules but lookup and
$\mbox{{op}}_{+}$ make the overlap condition $\exists c\
\left({\left\langle{}^{\text{\tt x}:=m+1\mathop{\mathbf{||}}\text{\tt
x}:=\text{\tt x}+1,}_{\text{\tt x}\mapsto
m}\right\rangle}[c/\square]\land\varphi_{l}[c/\square]\right)$ unsatisfiable,
and only one choice of free variables works for the lookup and
$\mbox{{op}}_{+}$ rules. For lookup, $\varphi_{l}$ is $\langle
C,\sigma\rangle[x]$ and the overlap condition is only satisfiable if the
logical variables $C$, $\sigma$ and $x$ are equal to $({\tt
x}:=m+1\mathop{\mathbf{||}}{\tt x}:=\rule{5.69054pt}{5.69054pt}+1)$, $({\tt
x}\mapsto m)$, and ${\tt x}$, respectively. Under this assignment, the pattern
$\varphi_{r}=\langle C,\sigma\rangle[\sigma(x)]$ is equivalent to
$\langle{{\tt x}:=m+1\mathop{\mathbf{||}}{\tt x}:=m+1},\ {{\tt x}\mapsto
m}\rangle$, the right branch of the disjunction. The $\mbox{{op}}_{+}$ rule is
handled similarly. The assignment for lookup can also witness the existential
in the progress hypothesis of Step. Subproofs for other states in Fig. 3 can
be constructed similarly.

⬇

f0 = 1;

turn = 1;

while (f1 && turn)

skip

x = x + 1;

f0 = 0;

⬇

f1 = 1;

turn = 0;

while (f0 && (1 - turn))

skip

x = x + 1;

f1 = 0;

Figure 4. Peterson’s algorithm (threads ${\tt T_{0}}$ and ${\tt T_{1}}$)

The next two examples use loops and thus need to state and prove invariants.
As discussed in [4], Circularity generalizes the various language-specific
invariant proof rules encountered in Hoare logics. One application is reducing
a proof of $\varphi\Rightarrow^{\forall}\varphi^{\prime}$ to proving
$\varphi_{\rm inv}\Rightarrow^{\forall}\varphi_{\rm inv}\lor\varphi^{\prime}$
for some pattern invariant $\varphi_{\rm inv}$. We first show
$\models\varphi\rightarrow\varphi_{\rm inv}$, and use Consequence to change
the goal to $\varphi_{\rm inv}\Rightarrow^{\forall}\varphi^{\prime}$. This is
claimed as a circularity, and then proved by transitivity with $\varphi_{\rm
inv}\lor\varphi^{\prime}$. The second hypothesis $\\{\varphi_{\rm
inv}\Rightarrow^{\forall}\varphi^{\prime}\\}\vdash\varphi_{\rm
inv}\lor\varphi^{\prime}\Rightarrow^{\forall}\varphi^{\prime}$ is proved by
Case Analysis, Axiom, and Reflexivity.

Next, we can use Peterson’s algorithm for mutual exclusion to eliminate the
race as shown in Fig. 4. The all-path rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ that captures the new behavior
is

$\begin{array}[]{rl}&\langle{{\tt T_{0}}\mathop{\mathbf{||}}{\tt T_{1}}},\
{(\text{\tt f0}\mapsto 0,\ \text{\tt f1}\mapsto 0,\ \text{\tt x}\mapsto
N)}\rangle\\\ \Rightarrow^{\forall}&\exists t\ \langle{\texttt{skip}},\
{(\text{\tt f0}\mapsto 0,\ \text{\tt f1}\mapsto 0,\ \text{\tt x}\mapsto
N+_{\it Int}2,\ \text{\tt turn}\mapsto t)}\rangle\\\ \end{array}$

Similarly to the unsynchronized example, the proof contains subproofs of
$c\Rightarrow^{\forall}\varphi^{\prime}$ for every configuration $c$ reachable
from $\varphi$. The main difference is that Circularity is used with each of
these rules $c\Rightarrow^{\forall}\varphi^{\prime}$ with one of the two
threads of $c$ in the while loop (these rules capture the invariants). Thus,
when we reach a configuration $c$ visited before, we use the rule added by
Circularity to complete the proof.

The final example is the program SUM $\equiv$ “s := 0; LOOP” (where LOOP
stands for “while (n>0) (s := s+n; n := n-1)”), which computes in s the sum of
the numbers from $1$ up to n. The all-path reachability rule
$\varphi\Rightarrow^{\forall}\\!\varphi^{\prime}$ capturing this behavior is

$\langle{\texttt{SUM}},\ {(\texttt{s}\mapsto s,\ \texttt{n}\mapsto
n)}\rangle\mathbin{\wedge}n\geq_{\it Int}0\ \Rightarrow^{\forall}\
\langle{{\tt skip}},\ {(\texttt{s}\mapsto n*_{\it Int}(n+_{\it Int}1)/_{\it
Int}2,\ \texttt{n}\mapsto 0)}\rangle$

We derive the above rule in our proof system by using Circularity with the
invariant rule

$\exists n^{\prime}(\langle{\texttt{LOOP}},\
{(\texttt{s}\\!\mapsto\\!(n\\!-_{\it Int}\\!n^{\prime})\\!*_{\it
Int}\\!(n\\!+_{\it Int}\\!n^{\prime}\\!+_{\it Int}\\!1)/_{\it Int}2,\
\texttt{n}\\!\mapsto\\!n^{\prime})}\rangle\mathbin{\wedge}n^{\prime}\\!\geq_{\it
Int}\\!0)\Rightarrow^{\forall}\varphi^{\prime}$

Previous work [6, 5, 4, 7] presented a proof system able to derive similar
rules, but which hold along some execution path, requiring a separate proof
that the program is deterministic.

##  6\. Implementation

Here we briefly discuss our prototype implementation of the proof system in
Fig. 1 in $\mathbb{K}$ [9]. We choose $\mathbb{K}$ because it is a modular
semantic language design framework, it is used for teaching programming
languages at several universities, and there are several languages defined in
it including C [13], PHP [18], Python, and Java. For brevity, we do not
present $\mathbb{K}$ here. We refer the reader to http://kframework.org for
language definitions, a tutorial, and our prototype. As discussed in Section
3, we simply view a $\mathbb{K}$ semantics as a set of reachability rules of
the form “$l\mathbin{\wedge}b\Rightarrow^{\exists}r$”.

The prototype is implemented in Java, and uses Z3 [19] for domain reasoning.
It takes an operational semantics and uses it to perform concrete or symbolic
execution. At its core, it performs narrowing of a conjunctive pattern with
reachability rules between conjunctive patterns, where a conjunctive pattern
is a pattern of the form $\exists X(\pi\mathbin{\wedge}\psi)$, with $X$ a set
of variables, $\pi$ a basic pattern (program configurations with variables),
and $\psi$ a structureless formula. Narrowing is necessary when a conjunctive
pattern is too abstract to match the left-hand side of any rule, but is
unifiable with the left-hand sides of some rules. For instance, consider the
IMP code fragment “$\texttt{if (}b\texttt{) then x = 1; else x = 0;}$”. This
code does not match the left-hand sides of either of the two rules giving
semantics to if (similar to $\textbf{cond}_{1}$ and $\textbf{cond}_{2}$ in
Fig. 2), but it is unifiable with the left-hand sides of both rules.
Intuitively, if we use the rules of the semantics, taking steps of rewriting
on a ground configuration yields concrete execution, while taking steps of
narrowing on a conjunctive pattern yields symbolic execution. In our practical
evaluation, we found that conjunctive patterns tend to suffice to specify both
the rules for operational semantics and program specifications.

For each step of narrowing, the $\mathbb{K}$ engine uses unification modulo
theories. In our implementation, we distinguish a number of mathematical
theories (e.g. booleans, integers, sequences, sets, maps, etc) which the
underlying SMT solver can reason about. Specifically, when unifying a
conjunctive pattern $\exists X(\pi\mathbin{\wedge}\psi)$ with the left-hand
side of a rule $\exists X_{l}(\pi_{l}\mathbin{\wedge}\psi_{l})$ (we assume
$X\cap X_{l}=\emptyset$), the $\mathbb{K}$ engine begins with the syntactic
unification of the basic patterns $\pi$ and $\pi_{l}$. Upon encountering
corresponding subterms ($\pi^{\prime}$ in $\pi$ and $\pi_{l}^{\prime}$ in
$\pi_{l}$) which are both terms of one of the theories above, it records an
equality $\pi^{\prime}=\pi_{l}^{\prime}$ rather than decomposing the subterms
further (if one is in a theory, and the other one is in a different theory or
is not in any theory, the unification fails). If this stage of unification is
successful, we end up with a conjunction $\psi_{u}$ of constraints, some
having a variable in one side and some with both sides in one of the theories.
Satisfiability of $\exists X\cup
X_{l}(\psi\mathbin{\wedge}\psi_{u}\mathbin{\wedge}\psi_{l})$ is then checked
by the SMT solver. If it is satisfiable, then narrowing takes a step from
$\exists X(\pi\mathbin{\wedge}\psi)$ to $\exists X\cup X_{l}\cup
X_{r}(\pi_{r}\mathbin{\wedge}\psi\mathbin{\wedge}\psi_{u}\mathbin{\wedge}\psi_{l}\mathbin{\wedge}\psi_{r})$,
where $\exists X_{r}(\pi_{r}\mathbin{\wedge}\psi_{r})$ is the right-hand side
of the rule. Intuitively, “collecting” the constraints
$\psi_{u}\mathbin{\wedge}\psi_{l}\mathbin{\wedge}\psi_{r}$ is similar to
collecting the path constraint in traditional symbolic execution (but is done
in a language-generic manner). For instance, in the if case above, narrowing
with the two semantics rules results in collecting the constraints
$b=\texttt{true}$ and $b=\texttt{false}$.

The $\mathbb{K}$ engine accepts a set of user provided rules to prove
together, which capture the behavior of the code being verified. Typically,
these rules specify the behavior of recursive functions and while loops. For
each rule, the $\mathbb{K}$ engine searches starting from the left-hand side
for formulae which imply the right-hand side, starting with ${\mathcal{}S}$
the semantics and ${\mathcal{}C}$ all the rules it attempts to prove. By a
derived proof rule called _Set Circularity_ , this suffices to show that each
rule is valid. As an optimization, Axiom is given priority over Step (use
specifications rather than stepping into the code).

Most work goes into implementing the Step proof rule, and in particular
calculating how $\rho\models\exists c\
(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])$ can be satisfied.
This holds when $\rho^{\gamma}\models\varphi$ and
$\rho^{\gamma}\models\varphi_{l}$, which can be checked with unification
modulo theories. To use Step in an automated way, the $\mathbb{K}$ tool
constructs $\varphi^{\prime}$ for a given $\varphi$ as a disjunction of
$\varphi_{r}\mathbin{\wedge}\psi_{u}\mathbin{\wedge}\psi\mathbin{\wedge}\psi_{l}$
over each rule $\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$
and each way $\psi_{u}$ of unifying $\varphi$ with $\varphi_{l}$. As discussed
in Section 4, in general this disjunction may not be finite, but it is
sufficient for the examples that we considered. The Consequence proof rule
also requires unification modulo theories, to check validity of the
implication hypothesis $\models\varphi_{1}\rightarrow\varphi_{1}^{\prime}$.
The main difference from Step is that the free variables of $\varphi^{\prime}$
become universality quantified when sending the query to the SMT solver. The
implementation of the other proof rules is straight-forward.

##  7\. Soundness

Here we discuss the soundness of our proof system. Unlike the similar results
for Hoare logics and dynamic logics, which are separately proved for each
language taking into account the particularities of that language, we prove
soundness once and for all languages.

Soundness states that a syntactically derivable sequent holds semantically.
Because of the utmost importance of the result below, we have also mechanized
its proof. Our complete Coq formalization can be found at
http://fsl.cs.illinois.edu/rl.

######  Theorem 1 (Soundness).

If ${\mathcal{}S}\vdash\varphi\Rightarrow^{\forall}\varphi^{\prime}$ then
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$.

######  Proof 7.1.

Due to Circularity and Transitivity the sets $\mathcal{}A$ and $\mathcal{}C$
may not remain empty, so we need to prove a more general statement (Lemma 2
below), including hypotheses making some semantic assumptions about the rules
in $\mathcal{}A$ and $\mathcal{}C$.

To express the different assumptions needed about the available rules in
$\mathcal{}A$ and the still-unavailable rules in $\mathcal{}C$ we define a
more specific satisfaction relation. Let $\delta\in\\{+,*\\}$ be a flag and
let $n\in\mathbb{N}$ be a natural number. We define the new satisfaction
relation
${\mathcal{}S}\models_{n}^{\delta}\varphi\Rightarrow^{\forall}\varphi^{\prime}$
by restricting the paths in the definition of
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ to length
at most $n$, and requiring that $\varphi$ be reached after at least one step
if $\delta=+$. Formally, we define
${\mathcal{}S}\models_{n}^{\delta}\varphi\Rightarrow^{\forall}\varphi^{\prime}$
to hold iff for any complete path $\tau=\gamma_{1}...\gamma_{k}$ of length
$k\leq n$ and for any $\rho$ such that
$({\gamma_{1}},{\rho})\models{\varphi}$, there exists $i\in\\{1,...,k\\}$ such
that $({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$ and also that this $i$
is not 1 (i.e. $\gamma_{1}$ makes progress) if $\delta=+$.

Observe that
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ iff
${\mathcal{}S}\models^{*}_{n}\varphi\Rightarrow^{\forall}\varphi^{\prime}$ for
all $n\in\mathbb{N}$. The forward implication holds because a complete path
$\tau=\gamma_{1}...\gamma_{k}$ of length $k\leq n$ is a complete path
simpliciter. The reverse implication holds because given any complete path
$\tau=\gamma_{1}...\gamma_{k}$ there are choices (such as $k$) of
$n\in\mathbb{N}$ with $k\leq n$. Theorem 1 then follows from Lemma 2 by noting
that the hypotheses about $\mathcal{}A$ and $\mathcal{}C$ are vacuously true
when those sets are empty.

######  Lemma 2.

If ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$
then for any $n$, ${\mathcal{}S}\models^{+}_{n}{\mathcal{}A}$ and
${\mathcal{}S}\models^{+}_{n-1}{\mathcal{}C}$ imply that
${\mathcal{}S}\models_{n}^{*}\varphi\Rightarrow^{\forall}\varphi^{\prime}$,
and also that
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$ if
$\mathcal{}C$ is not empty.

######  Proof 7.2.

To state the conclusion of the lemma more concisely we define flag
$\Delta_{C}$ to be $*$ if $C$ is an empty set and $+$ otherwise. The
conclusion is
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi\Rightarrow^{\forall}\varphi^{\prime}$.
The proof proceeds by induction on the proof tree showing
${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\varphi}\Rightarrow^{\forall}{\varphi^{\prime}}$
(keeping induction hypotheses universally quantified over $n$), using an inner
induction over $n$ in the Circularity case.

Circularity: The induction hypothesis states that for any $m\in\mathbb{N}$.

$\mbox{if }{\mathcal{}S}\models_{m}^{+}{\mathcal{}A}\mbox{ and
}{\mathcal{}S}\models_{m-1}^{+}{\mathcal{}C}\cup\\{\varphi\Rightarrow^{\forall}\varphi^{\prime}\\}\mbox{
then
}{\mathcal{}S}\models_{m}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}.$
(1)

We will strengthen $\Delta_{\mathcal{}C}$ to ${+}$ and prove that for any
$n\in\mathbb{N}$, if ${\mathcal{}S}\models_{n}^{+}{\mathcal{}A}$ and
${\mathcal{}S}\models_{n-1}^{+}{\mathcal{}C}$ then
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$.
Proceed by induction on $n$.

  1. (1)

if $n=0$, the conclusion
${\mathcal{}S}\models_{0}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$ of
the implication is vacuously true.

  2. (2)

for $n>0$, we have an inner induction hypothesis that
${\mathcal{}S}\models_{n-1}^{+}{\mathcal{}A}$ and
${\mathcal{}S}\models_{n-2}^{+}{\mathcal{}C}$ together imply
${\mathcal{}S}\models_{n-1}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$,
and must prove that ${\mathcal{}S}\models_{n}^{+}{\mathcal{}A}$ and
${\mathcal{}S}\models_{n-1}^{+}{\mathcal{}C}$ together imply
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$,
Instantiating the inner hypothesis with the stronger assumptions about
$\mathcal{}A$ and $\mathcal{}C$ gives
${\mathcal{}S}\models_{n-1}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$.
With other assumptions this gives
${\mathcal{}S}\models_{n-1}^{+}{\mathcal{}C}\cup\\{\varphi\Rightarrow^{\forall}\varphi^{\prime}\\}$.
Now we apply the outer induction hypothesis, Equation (1), with $m=n$ to
conclude
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$.

This was the only case that made essential use of the quantification over $n$
in the conclusion. For the remaining cases, we assume that $n\in\mathbb{N}$ is
already fixed, and assumptions ${\mathcal{}S}\models_{n}^{+}{\mathcal{}A}$ and
$\models^{+}_{n-1}{\mathcal{}C}$ are given in addition to the assumptions and
inductive hypotheses coming from the specific proof rule. Inductive hypotheses
with the same $\mathcal{}A$ and $\mathcal{}C$ as the conclusion will be stated
in the form
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi_{a}\Rightarrow^{\forall}\varphi_{b}$,
already specialized to $n$ and applied to the semantic assumptions on
$\mathcal{}A$ and $\mathcal{}C$. Furthermore, the remaining cases all prove
the conclusion
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$
directly from the definition, so we also assume that a complete path
$\tau=\gamma_{1},...,\gamma_{k}$ with $k\leq n$ and a $\rho$ with
$({\gamma_{1}},{\rho})\models{\varphi}$ are fixed. This leaves the obligation
to find an $i\in\\{1,...,k\\}$ such that
$({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$ and that $i>1$ if
$\mathcal{}C$ is nonempty.

Transitivity: We have inductive hypotheses that
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi\rightarrow\varphi_{2}$,
and for any $m\in\mathbb{N}$, ${\mathcal{}S}\models_{m}^{+}{\mathcal{}A\cup
C}$ implies
${\mathcal{}S}\models_{m}^{*}\varphi_{2}\rightarrow\varphi^{\prime}$. Applying
the first inductive hypothesis to $\tau$ and $\rho$, we receive an $i$ such
that $({\gamma_{i}},{\rho})\models{\varphi_{2}}$. Now we make separate cases
on whether $i=1$.

  * •

When $i=1$, $\mathcal{}C$ must be empty, so our assumption
${\mathcal{}S}\models_{n}^{+}{\mathcal{}A}$ suffices to instantiate the second
inductive hypothesis at $m=n$ to obtain
${\mathcal{}S}\models_{n}^{*}\varphi_{2}\rightarrow\varphi^{\prime}$. As
$({\gamma_{1}},{\rho})\models{\varphi_{2}}$ we can apply this to $\tau$ and
$\rho$ to obtain a $j$ such that
$({\gamma_{j}},{\rho})\models{\varphi^{\prime}}$, concluding this case.

  * •

Otherwise, the suffix of $\tau$ beginning with $\gamma_{i}$ has length
strictly less than $n$, so it suffices to instantiate the second inductive
hypothesis at $m=n-1$. Our assumptions on $\mathcal{}C$ and $\mathcal{}A$
suffice to conclude ${\mathcal{}S}\models_{n-1}^{+}{\mathcal{}A\cup C}$. We
obtain
${\mathcal{}S}\models_{n-1}^{*}\varphi_{2}\Rightarrow^{\forall}\varphi^{\prime}$.
Applying this to $\rho$ and the complete path $\gamma_{i},...,\gamma_{k}$
yields $j$ such that $({\gamma_{i+j-1}},{\rho})\models{\varphi^{\prime}}$. As
$i+j-1>1$, we can conclude this case with $i+j-1$ whether or not $\mathcal{}C$
is empty.

Step: This rule has assumptions
$\models\varphi\rightarrow\bigvee_{\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\
\in\ {\mathcal{}S}}\exists\textit{FreeVars}({\varphi_{l}})\varphi_{l}$, and
for any $\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$
$\models\exists c\
(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])\mathbin{\wedge}\varphi_{r}\rightarrow\varphi^{\prime}$
. By the first assumption $\gamma_{1}$ is not stuck, so complete path $\tau$
has a second entry $\gamma_{2}$. By the definition of a path,
$\gamma_{1}\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma_{2}$. By
the definition of $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$, there
exists $\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in S$ and valuation
$\rho^{\prime}$ such that $({\gamma_{1}},{\rho^{\prime}})\models{\varphi_{l}}$
and $({\gamma_{2}},{\rho^{\prime}})\models{\varphi_{r}}$. Let
$X=\textit{FreeVars}({\varphi,\varphi^{\prime}})$ and
$Y=\textit{FreeVars}({\varphi_{l},\varphi_{r}})$. We assume without loss of
generality that $X\cap Y=\emptyset$. Fix any $\rho^{\prime\prime}$ which
agrees with $\rho$ on $X$ and with $\rho^{\prime}$ on $Y$. With this choice
$({\gamma_{1}},{\rho^{\prime\prime}})\models{\varphi}$,
$({\gamma_{1}},{\rho^{\prime\prime}})\models{\varphi_{l}}$, and
$({\gamma_{2}},{\rho^{\prime\prime}})\models{\varphi_{r}}$. By the definition
of satisfaction and the FOL translation, then also
$({\gamma_{2}},{\rho^{\prime\prime}})\models{\exists
c.(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])}$ and finally
$({\gamma_{2}},{\rho^{\prime\prime}})\models{\exists
c.(\varphi[c/\square]\mathbin{\wedge}\varphi_{l}[c/\square])\mathbin{\wedge}\varphi_{r}}$.
By the second assumption this implies
$({\gamma_{2}},{\rho^{\prime\prime}})\models{\varphi^{\prime}}$. As
$\rho^{\prime\prime}$ agrees with $\rho$ on $X$,
$({\gamma_{2}},{\rho})\models{\varphi^{\prime}}$ (and $2>1$), so taking $i=2$
concludes this case.

Reflexivity: This rule requires $\mathcal{}C$ be empty, and
$\varphi=\varphi^{\prime}$, so $i=1$ suffices by
$({\gamma_{1}},{\rho})\models{\varphi}$.

Axiom: This rule has assumption
$\varphi\Rightarrow^{\forall}\varphi^{\prime}\in\mathcal{}{A}$. By the
assumption on $\mathcal{}{A}$,
${\mathcal{}S}\models_{n}^{+}\varphi\Rightarrow^{\forall}\varphi^{\prime}$.
Applying this to $\tau$ and $\rho$ gives an $i>1$ with
$({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$, concluding this case.

Consequence: We have inductive hypothesis that
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi_{1}\Rightarrow^{\forall}\varphi_{1}^{\prime}$,
and assumptions $\models\varphi\rightarrow\varphi_{1}$ and
$\models\varphi_{1}^{\prime}\rightarrow\varphi^{\prime}$. By the first
implication $({\gamma_{1}},{\rho})\models{\varphi_{1}}$ as well, so we can
apply the inductive hypothesis with $\tau$ and $\rho$ to obtain some $i$ such
that $({\gamma_{i}},{\rho})\models{\varphi_{1}^{\prime}}$ and $i>1$ if
$\mathcal{}C$ is nonempty. By the second implication,
$({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$ as well, so this $i$
concludes this case.

Case Analysis: This rule requires $\varphi$ have the form
$\varphi_{1}\mathbin{\vee}\varphi_{2}$, and we have inductive hypotheses
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi_{1}\Rightarrow^{\forall}\varphi^{\prime}$
and
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi_{2}\Rightarrow^{\forall}\varphi^{\prime}$.
Because $({\gamma_{1}},{\rho})\models{\varphi}$, either
$({\gamma_{1}},{\rho})\models{\varphi_{1}}$ or
$({\gamma_{1}},{\rho})\models{\varphi_{2}}$. In either case we can use the
respective inductive hypotheses with $\tau$ and $\rho$ to obtain an $i$ such
that $({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$ and $i>1$ if
$\mathcal{}C$ is nonempty, concluding this case.

Abstraction: This rule requires $\varphi$ have the form $\exists X\varphi_{1}$
with $X\not\in\textit{FreeVars}({\varphi^{\prime}})$, and we have the
inductive hypothesis
${\mathcal{}S}\models_{n}^{\Delta_{\mathcal{}C}}\varphi_{1}\Rightarrow^{\forall}\varphi^{\prime}$.
Because $({\gamma_{1}},{\rho})\models{\exists X\varphi_{1}}$ there exists a
$\rho^{\prime}$ which agrees with $\rho$ except on $X$ such that
$({\gamma_{1}},{\rho^{\prime}})\models{\varphi_{1}}$. Using the inductive
hypothesis with $\tau$ and this $\rho^{\prime}$ gives an $i$ such that
$({\gamma_{i}},{\rho^{\prime}})\models{\varphi^{\prime}}$, and $i>1$ if
$\mathcal{}C$ is nonempty. As $X\not\in\textit{FreeVars}({\varphi^{\prime}})$,
then also $({\gamma_{i}},{\rho})\models{\varphi^{\prime}}$, so this $i$
concludes this case.

##  8\. Relative Completeness

Here we show relative completeness: any valid all-path reachability property
of any program in any language with an operational semantics given as a
reachability system ${\mathcal{}S}$ is derivable with the proof system in Fig.
1 from ${\mathcal{}S}$. As with Hoare and dynamic logics, “relative” means we
assume an oracle capable of establishing validity in the first-order theory of
the state, which here is the configuration model ${\mathcal{}T}$. Unlike the
similar results for Hoare logics, which are separately proved for each
language taking into account the particularities of that language, we prove
relative completeness once and for all languages. An immediate consequence of
relative completeness is that Circularity is sufficient to derive any
repetitive behavior occurring in any program written in any language, and that
Step is also sufficient to derive any non-deterministic behavior!

We establish the relative completeness under the following assumptions:

Framework: The semantics reachability system ${\mathcal{}S}$ is — finite; The
configuration signature $\Sigma$ has — a sort $\mathbb{N}$; — constant symbols
$0$ and $1$ of $\mathbb{N}$; — binary operation symbols $+$ and $\times$ on
$\mathbb{N}$; — an operation symbol $\alpha:{\it Cfg}\rightarrow\mathbb{N}$.
The configuration model $\mathcal{}T$ interprets — $\mathbb{N}$ as the natural
numbers; — constant and operation symbols on $\mathbb{N}$ as corresponding
operations; — $\alpha:{\it Cfg}\rightarrow\mathbb{N}$ as an injective
function.

The assumption that ${\mathcal{}S}$ is finite ensures Step has a finite number
of prerequisites. The assumption that the model ${\mathcal{}T}$ includes
natural numbers with addition and multiplication is a standard assumption
(also made by Hoare and dynamic logic completeness results) which allows the
definition of Gödel’s $\beta$ predicate. The assumption that the model
${\mathcal{}T}$ includes some injective function
$\alpha:{\mathcal{}T}_{\\!\\!{\it Cfg}}\rightarrow\mathbb{N}$ (that is, the
set of configurations ${\mathcal{}T}_{\\!\\!{\it Cfg}}$ is countable) allows
the encoding of a sequence of configurations into a sequence of natural
numbers. We expect the operational semantics of any reasonable language to
satisfy these conditions. Formally, we have the following

######  Theorem 3 (Relative Completeness).

For any semantics ${\mathcal{}S}$ satisfying the assumptions above, if
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ then
${\mathcal{}S}\vdash\varphi\Rightarrow^{\forall}\varphi^{\prime}$.

We present an informal proof sketch before going into the formal details, Our
proof relies on the fact that pattern reasoning in first-order matching logic
reduces to FOL reasoning in the model ${\mathcal{}T}$. A key component of the
proof is defining the $\textit{coreach}({\varphi})$ predicate in plain FOL.
This predicate states that every complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path $\tau$ starting at
c includes some configuration satisfying $\varphi$. We express
$\textit{coreach}({\varphi})$ using the auxiliary predicate that encodes the
one step transition relation
($\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$). Fig. 5 shows both
definitions. As it is, $\textit{coreach}({\varphi})$ is not a proper FOL
formula, as it quantifies over a sequence of configurations. This is addressed
using the injective function $\alpha$ to encode universal quantification over
a sequence of configurations into universal quantification over a sequence of
integers, which is in turn encoded into quantification over two integer
variables using Gödel’s $\beta$ predicate (encoding shown in Fig. 6).

Next, using the definition above we encode the semantic validity of an all-
path reachability rule as FOL validity:
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ iff
$\models\varphi\rightarrow\textit{coreach}({\varphi^{\prime}})$. Therefore,
the theorem follows by Consequence from the sequent ${\mathcal{}S}\
\mathrel{\vdash}{\textit{coreach}({\varphi^{\prime}})}\Rightarrow^{\forall}{\varphi^{\prime}}$.
We derive this sequent by using Circularity to add the rule to the set of
circularities, then by using Step to derive one
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-step, and then by using
Transitivity and Axiom with the rule itself to derive the remaining
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-steps (circularities can
be used after Transitivity). The formal derivation uses all eight proof rules.

Also recall that, as discussed in Section 2, matching logic is a
methodological fragment of the FOL theory of the model ${\mathcal{}T}$. For
technical convenience, in this section we work with the FOL translations
$\varphi^{\square}$ instead of the matching logic formulae $\varphi$. We
mention that in all the formulae used in this section, $\square$ only occurs
in the context $\square=t$, thus we stay inside the methodological fragment.
For the duration of the proof, we let
$\textit{c},\textit{c}^{\prime},\textit{c}_{0},...,\textit{c}_{n}$ be distinct
variables of sort ${\it Cfg}$ which do not appear free in the rules in
${\mathcal{}S}$). We also let
$\gamma,\gamma^{\prime},\gamma_{0},...,\gamma_{n}$ range over (not necessarily
distinct) configurations in the model ${\mathcal{}T}$, that is, over elements
in ${\mathcal{}T}_{\\!\\!{\it Cfg}}$, and let $\rho,\rho^{\prime}$ range over
valuations $\textit{Var}\rightarrow{\mathcal{}T}$.

###  8.1. Encoding Transition System Operations in FOL

$\begin{array}[]{@{}r@{ \ \ }c@{ \ \
}l@{}}\step{\textit{c}}{\textit{c}^{\prime}}&\equiv&\displaystyle\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\mu})\
({\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}{\varphi_{r}}[{\textit{c}^{\prime}}/\square])\\\
\textit{coreach}({\varphi})&\equiv&\displaystyle\forall
n\forall\textit{c}_{0}...\textit{c}_{n}\Bigg{(}\square=\textit{c}_{0}\rightarrow\\!\\!\bigwedge\limits_{0\leq
i<n}\\!\\!\step{\textit{c}_{i}}{\textit{c}_{i+1}}\rightarrow\neg\exists\textit{c}_{n+1}\
\step{\textit{c}_{n}}{\textit{c}_{n+1}}\rightarrow\\!\\!\bigvee\limits_{0\leq
i\leq n}\\!\\!{\varphi}[{\textit{c}_{i}}/\square]\Bigg{)}\end{array}$ Figure
5. FOL encoding of one step transition relation and all-path reachability.

Fig. 5 shows the definition of the one step transition relation
($\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$) and of the
configurations that reach $\varphi$ on all and complete paths. The former is a
(proper) FOL formula, while the later is not, as it quantifies over a sequence
of configuration. In Section 8.2 we use Gödel’s $\beta$ predicate to define
$\overline{\textit{coreach}}({\varphi})$, a FOL formula equivalent to
$\textit{coreach}({\varphi})$.

First, we establish the following general purpose lemma

######  Lemma 4.

$({\rho(\textit{c})},{\rho})\models{\varphi^{\square}}$ iff
$\rho\models{\varphi^{\square}}[{\textit{c}}/\square]$.

######  Proof 8.5.

With the notation in Definition 2,
$({\rho(c)},{\rho})\models{\varphi^{\square}}$ iff
$\rho^{\rho(c)}\models\varphi^{\square}$. Notice that if a valuation agrees on
two variables, then it satisfies a formula iff it satisfies the formula
obtained by substituting one of the two variables for the other. In
particular, since $\rho^{\rho(c)}(\square)=\rho^{\rho(c)}(c)$, it follows that
$\rho^{\rho(c)}\models\varphi^{\square}$ iff
$\rho^{\rho(c)}\models\varphi^{\square}[c/\square]$. We notice that $\square$
does not occur in $\varphi^{\square}[c/\square]$, thus
$\rho^{\rho(c)}\models\varphi^{\square}[c/\square]$ iff
$\rho\models\varphi^{\square}[c/\square]$, and we are done.

The following lemma states that actually has the semantic properties its name
suggests.

######  Lemma 5.

$\rho\models$ iff
$\rho(\textit{c})\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\rho(\textit{c}^{\prime})$.

######  Proof 8.8.

Assume $\rho\models$. Then, by the definition of , there exists some rule
$\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$ such
that $\rho\models\exists\textit{FreeVars}({\mu})\
(\varphi_{l}[\textit{c}/\square]\mathbin{\wedge}\varphi_{r}[\textit{c}^{\prime}/\square])$.
Further, since c and $\textit{c}^{\prime}$ do not occur in $\mu$, there exists
some $\rho^{\prime}$ which agrees with $\rho$ on c and $\textit{c}^{\prime}$
such that $\rho^{\prime}\models\varphi_{l}[\textit{c}/\square]$ and
$\rho^{\prime}\models\varphi_{r}[\textit{c}^{\prime}/\square]$. By Lemma 4,
$\rho^{\prime}\models\varphi_{l}[c/\square]$ iff
$({\rho^{\prime}(\textit{c})},{\rho^{\prime}})\models{\varphi_{l}}$ and
$\rho^{\prime}\models\varphi_{r}[\textit{c}^{\prime}/\square]$ iff
$({\rho^{\prime}(\textit{c}^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$,
so $({\rho^{\prime}(\textit{c})},{\rho^{\prime}})\models{\varphi_{l}}$ and
$({\rho^{\prime}(\textit{c}^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$.
Since $\rho$ and $\rho^{\prime}$ agree on c and $\textit{c}^{\prime}$, it
follows that $({\rho(c)},{\rho^{\prime}})\models{\varphi_{l}}$ and
$({\rho(c^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$. By Definition 3,
we conclude
$\rho(\textit{c})\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\rho(\textit{c}^{\prime})$.

Conversely, assume
$\rho(\textit{c})\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\rho(\textit{c}^{\prime})$.
Then, by Definition 3, there exist some rule
$\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$ and
some $\rho^{\prime}$ for which
$({\rho(\textit{c})},{\rho^{\prime}})\models{\varphi_{l}}$ and
$({\rho(\textit{c}^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$. Further,
since c and $\textit{c}^{\prime}$ do not occur in $\mu$, we can choose
$\rho^{\prime}$ to agree with $\rho$ on c and $\textit{c}^{\prime}$. Hence,
$({\rho^{\prime}(\textit{c})},{\rho^{\prime}})\models{\varphi_{l}}$ and
$({\rho^{\prime}(\textit{c}^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$.
By Lemma 4,
$({\rho^{\prime}(\textit{c})},{\rho^{\prime}})\models{\varphi_{l}}$ iff
$\rho^{\prime}\models\varphi_{l}[\textit{c}/\square]$ and
$({\rho^{\prime}(\textit{c}^{\prime})},{\rho^{\prime}})\models{\varphi_{r}}$
iff $\rho^{\prime}\models\varphi_{r}[\textit{c}^{\prime}/\square]$, so
$\rho^{\prime}\models\varphi_{l}[\textit{c}/\square]$ and
$\rho^{\prime}\models\varphi_{r}[\textit{c}^{\prime}/\square]$. Since the free
variables occurring in
$\varphi_{l}[\textit{c}/\square]\mathbin{\wedge}\varphi_{r}[\textit{c}^{\prime}/\square]$
are $\textit{FreeVars}({\mu})\cup\\{\textit{c},\textit{c}^{\prime}\\}$ and
$\rho$ and $\rho^{\prime}$ agree on c and $\textit{c}^{\prime}$, it follows
that $\rho\models\exists\textit{FreeVars}({\mu})\
(\varphi_{l}[\textit{c}/\square]\mathbin{\wedge}\varphi_{r}[\textit{c}^{\prime}/\square])$.
By the definition of , we conclude $\rho\models$.

The following lemma introduces a formula encoding a complete path of fixed
length.

######  Lemma 6.

$\rho\models\bigwedge\limits_{0\leq i<n}$ iff
$\rho(\textit{c}_{0}),...,\rho(\textit{c}_{n+1})$ is a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path.

######  Proof 8.15.

By Lemma 5, we have that
$\rho(\textit{c}_{i})\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\rho(\textit{c}_{i+1})$
iff $\rho^{\prime}\models$, for each $0\leq i<n$. Further,
$\rho(\textit{c}_{0}),...,\rho(\textit{c}_{n+1})$ is complete, iff there does
not exist $\gamma$ such that
$\rho(\textit{c}_{n})\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma$.
Again, by Lemma 5, that is iff $\rho\models\not\exists\textit{c}_{n+1}\ $. We
conclude that $\rho\models\bigwedge\limits_{0\leq i<n}$ iff
$\rho(\textit{c}_{0}),...,\rho(\textit{c}_{n+1})$ is a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path, and we are done.

The following lemma states that $\textit{coreach}({\varphi})$ actually has the
semantic properties its name suggests.

######  Lemma 7.

$({\gamma},{\rho})\models{\textit{coreach}({\varphi})}$ iff for all complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-paths $\tau$ starting
with $\gamma$ it is the case that $({\gamma^{\prime}},{\rho})\models{\varphi}$
for some $\gamma^{\prime}\in\tau$.

######  Proof 8.20.

First we prove the direct implication. Assume
$({\gamma},{\rho})\models{\textit{coreach}({\varphi})}$, and let
$\tau\equiv\gamma_{0},...,\gamma_{n}$ be a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path starting with
$\gamma$. Then let $\rho^{\prime}$ agree with $\rho$ on
$\textit{FreeVars}({\varphi})$ such that $\rho^{\prime}(n)=n$ and
$\rho^{\prime}(\textit{c}_{i})=\gamma_{i}$ for each $0\leq i\leq n$. According
to the definition of $\textit{coreach}({\varphi})$, we have that

$({\gamma},{\rho^{\prime}})\models{\square=\textit{c}_{0}\mathbin{\wedge}\bigwedge\limits_{0\leq
i<n}\step{\textit{c}_{i}}{\textit{c}_{i+1}}\mathbin{\wedge}\not\exists\textit{c}_{n+1}\
\step{\textit{c}_{n}}{\textit{c}_{n+1}}\rightarrow\bigvee\limits_{0\leq i\leq
n}{\varphi}[{\textit{c}_{i}}/\square]}$

Since, $\gamma=\gamma_{0}$ and $\rho^{\prime}(\textit{c}_{0})=\gamma_{0}$, it
follows that $\rho^{\prime}\models\square=\textit{c}_{0}$. Further, by Lemma
6, since $\rho^{\prime}(\textit{c}_{0}),...,\rho^{\prime}(\textit{c}_{n})$ is
a complete $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path, it must
be the case that

$\rho^{\prime}\models\bigwedge\limits_{0\leq i<n}$

Thus, as $\square$ does not occur in any
${\varphi}[{\textit{c}_{i}}/\square]$, we conclude that
$\rho^{\prime}\models\bigvee\limits_{0\leq i\leq
n}{\varphi}[{\textit{c}_{i}}/\square]$, that is,
$\rho^{\prime}\models{\varphi}[{\textit{c}_{i}}/\square]$ for some $0\leq
i\leq n$. By Lemma 4,
$\rho^{\prime}\models{\varphi}[{\textit{c}_{i}}/\square]$ iff
$({\gamma_{i}},{\rho^{\prime}})\models{\varphi}$. Since $\rho$ agrees with
$\rho^{\prime}$ on $\textit{FreeVars}({\varphi})$, we conclude that
$({\gamma_{i}},{\rho})\models{\varphi}$.

Conversely, assume that if $\tau$ is a finite and complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path starting with
$\gamma$. Then $({\gamma^{\prime}},{\rho})\models{\varphi}$ for some
$\gamma^{\prime}\in\tau$. Let $\rho^{\prime}$ agree with $\rho$ on
$\textit{FreeVars}({\varphi})$. Then we prove that

$({\gamma},{\rho^{\prime}})\models{\square=\textit{c}_{0}\mathbin{\wedge}\bigwedge\limits_{0\leq
i<n}\step{\textit{c}_{i}}{\textit{c}_{i+1}}\mathbin{\wedge}\not\exists\textit{c}_{n+1}\
\step{\textit{c}_{n}}{\textit{c}_{n+1}}\rightarrow\bigvee\limits_{0\leq i\leq
n}{\varphi}[{\textit{c}_{i}}/\square]}$

Specifically, assume
$({\gamma},{\rho^{\prime}})\models{\square=\textit{c}_{0}\mathbin{\wedge}\bigwedge\limits_{0\leq
i<n}\step{\textit{c}_{i}}{\textit{c}_{i+1}}\mathbin{\wedge}\not\exists\textit{c}_{n+1}\
\step{\textit{c}_{n}}{\textit{c}_{n+1}}}$. As $\square$ does not occur in any
$\textit{c}{\textit{c}_{i}}{\textit{c}_{i+1}}$, by Lemma 6, it follows that
$\rho^{\prime}(\textit{c}_{0}),...,\rho^{\prime}(\textit{c}_{n})$ is a
complete $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path. Further,
$({\gamma},{\rho^{\prime}})\models{\square=\textit{c}}$, implies that
$\rho^{\prime}(\textit{c}_{0}),...,\rho^{\prime}(\textit{c}_{n})$ starts with
$\gamma$. Thus, there exists some $0\leq i\leq n$ such that
$({\rho^{\prime}(\textit{c}_{i})},{\rho})\models{\varphi}$, or equivalently,
since $\rho$ and $\rho^{\prime}$ agree on $\textit{FreeVars}({\varphi})$, such
that $({\rho^{\prime}(\textit{c}_{i})},{\rho^{\prime}})\models{\varphi}$. By
Lemma 4, $({\rho^{\prime}(\textit{c}_{i})},{\rho^{\prime}})\models{\varphi}$
iff $\rho^{\prime}\models{\varphi}[{\textit{c}_{i}}/\square]$. Therefore, we
have that $({\gamma},{\rho^{\prime}})\models{\bigvee\limits_{0\leq i\leq
n}{\varphi}[{\textit{c}_{i}}/\square]}$. Finally, since $\rho^{\prime}$ is an
arbitrary valuation which agrees with $\rho$ on
$\textit{FreeVars}({\varphi})$, by the definition of
$\textit{coreach}({\varphi})$ we can conclude that
$({\gamma},{\rho})\models{\textit{coreach}({\varphi})}$, and we are done.

The following lemma establishes a useful property of
$\textit{coreach}({\varphi})$.

######  Lemma 8.

$\models\textit{coreach}({\varphi})\rightarrow\varphi\mathbin{\vee}(\exists\textit{c}^{\prime}\
$

######  Proof 8.31.

We prove that if $({\gamma},{\rho})\models{\textit{coreach}({\varphi})}$ then

$({\gamma},{\rho})\models{\varphi\mathbin{\vee}(\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square]))}$

By Lemma 7, we have that for all complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-paths $\tau$ starting
with $\gamma$ it is the case that
$({\gamma^{\prime\prime}},{\rho})\models{\varphi}$ for some
$\gamma^{\prime\prime}\in\tau$. We distinguish two cases

  * •

$({\gamma},{\rho})\models{\varphi}$. We are trivially done.

  * •

$({\gamma},{\rho})\not\models{\varphi}$. Then $\gamma$ must have
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-successors. Indeed,
assume the contrary. Then $\tau\equiv\gamma$ is a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path. It follows that
$({\gamma},{\rho})\models{\varphi}$, which is a contradiction. Thus, there
exists some $\gamma^{\prime}$ such that
$\gamma\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}\gamma^{\prime}$. By
Lemma 5, that is iff $\rho\models\exists\textit{c}^{\prime}\ $. Further, let
$\gamma^{\prime}$ be a
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-successor of $\gamma$
and $\tau^{\prime}$ a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path starting with
$\gamma^{\prime}$. Then, $\gamma\tau$ is a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path starting with
$\gamma$. Thus, there exists some
$\gamma^{\prime\prime}\in\gamma\tau^{\prime}$ such that
$({\gamma^{\prime\prime}},{\rho})\models{\varphi}$. Since
$({\gamma},{\rho})\not\models{\varphi}$, it follows that
$\gamma^{\prime\prime}\in\tau^{\prime}$. Notice that $\gamma^{\prime}$ is an
arbitrary configuration and $\tau^{\prime}$ an arbitrary
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path, therefore by Lemma
7 and Lemma 4, we can conclude that $\rho\models\forall\textit{c}^{\prime}\
($.

###  8.2. Formula Gödelization

$\begin{array}[]{rcl}\overline{\textit{coreach}}({\varphi})&\equiv&\forall
n\forall a\forall b\ (\exists\textit{c}\
(\beta({a},{b},{0},{\alpha(\textit{c})})\mathbin{\wedge}\square=\textit{c})\\\
&&\hskip 9.10623pt\mathbin{\wedge}\forall i\ (0\leq
i\mathbin{\wedge}i<n\rightarrow\exists\textit{c}\exists\textit{c}^{\prime}\
(\beta({a},{b},{i},{\alpha(\textit{c})})\mathbin{\wedge}\beta({a},{b},{i+1},{\alpha(\textit{c}^{\prime})})\mathbin{\wedge}\step{\textit{c}}{\textit{c}^{\prime}}))\\\
&&\hskip 9.10623pt\mathbin{\wedge}\exists\textit{c}\
(\beta({a},{b},{n},{\alpha(\textit{c})})\mathbin{\wedge}\not\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}})\\\ &&\hskip
9.10623pt\rightarrow\exists i\ (0\leq i\mathbin{\wedge}i\leq
n\mathbin{\wedge}\exists\textit{c}\
(\beta({a},{b},{i},{\alpha(\textit{c})})\mathbin{\wedge}{\varphi}[{\textit{c}}/\square])))\end{array}$
Figure 6. FOL definition of $\textit{coreach}({\varphi})$

Fig. 6 defines $\overline{\textit{coreach}}({\varphi})$, the FOL equivalent of
$\textit{coreach}({\varphi})$ using Gödel’s $\beta$ predicate. Formally, we
have the following

######  Lemma 9.

$\models\textit{coreach}({\varphi})\leftrightarrow\overline{\textit{coreach}}({\varphi})$.

######  Proof 8.38.

Let us choose some arbitrary but fixed values for $n$, $a$ and $b$, and let
$\rho^{\prime}$ such that $\rho$ and $\rho^{\prime}$ agree on
$\textit{Var}\setminus\\{n,a,b\\}$ and $\rho^{\prime}(n)=n$ and
$\rho^{\prime}(a)=a$ and $\rho^{\prime}(b)=b$. According to the definition of
the $\beta$ predicate, there exists a unique integer sequence
$j_{0},...,j_{n}$ such that $\beta({a},{b},{i},{j_{i}})$ holds for each $0\leq
i\leq n$. Since $\alpha$ is injective, we distinguish two cases

  * •

there exists some $0\leq i\leq n$ such that there is not any $\gamma_{i}$ with
$\alpha(\gamma_{i})=j_{i}$

  * •

there exists a unique sequence $\gamma_{0},...,\gamma_{n}$ such that
$\alpha(\gamma_{i})=j_{i}$ for each $0\leq i\leq n$.

In the former case, if $i=n$ we get that
$\rho^{\prime}\not\models\exists\textit{c}\
(\beta({a},{b},{n},{\alpha(\textit{c})})\mathbin{\wedge}\not\exists\textit{c}^{\prime}\
$ while if $0\leq i<n$ we get that
$\rho^{\prime}\not\models\exists\textit{c}\exists\textit{c}^{\prime}\
(\beta({a},{b},{i},{\alpha(\textit{c})})\mathbin{\wedge}\beta({a},{b},{i+1},{\alpha(\textit{c}^{\prime})})\mathbin{\wedge}$
as in both cases we can not pick a value for c. Thus, $(\gamma,\rho^{\prime})$
does not satisfy left-hand-side of the implication in
$\overline{\textit{coreach}}({\varphi})$, and we conclude that
$(\gamma,\rho^{\prime})$ satisfies the implication.

In the later case, we have that there is a unique way of instantiating the
existentially quantified variables c and $\textit{c}^{\prime}$ in each sub-
formula in which they appear, as they are always arguments of the $\beta$
predicate. Thus, $({\gamma},{\rho^{\prime}})\models{\exists\textit{c}\
(\beta({a},{b},{0},{\alpha(\textit{c})})\mathbin{\wedge}\square=\textit{c})}$
iff $\gamma=\gamma_{0}$. By Lemma 6, we have that

$\begin{array}[]{rcl}\rho^{\prime}&\models&\forall i\ (0\leq
i\mathbin{\wedge}i<n\rightarrow\exists\textit{c}\exists\textit{c}^{\prime}\
(\beta({a},{b},{i},{\alpha(\textit{c})})\mathbin{\wedge}\beta({a},{b},{i+1},{\alpha(\textit{c}^{\prime})})\mathbin{\wedge}\step{\textit{c}}{\textit{c}^{\prime}}))\\\
&&\mathbin{\wedge}\exists\textit{c}\
(\beta({a},{b},{n},{\alpha(\textit{c})})\mathbin{\wedge}\not\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}})\end{array}$

iff $\gamma_{0}...\gamma_{n}$ is a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path. Finally, by Lemma
4

$\rho^{\prime}\models\exists i\ (0\leq i\mathbin{\wedge}i\leq
n\mathbin{\wedge}\exists\textit{c}\
(\beta({a},{b},{i},{\alpha(\textit{c})})\mathbin{\wedge}{\varphi}[{\textit{c}}/\square]))$

iff $({\gamma_{i}},{\rho^{\prime}})\models{\varphi}$ for some $0\leq i\leq n$.

We conclude that $(\gamma,\rho^{\prime})$ satisfies the implication in
$\overline{\textit{coreach}}({\varphi})$ iff

  * •

there is no sequence $\gamma_{0},...,\gamma_{n}$ such that
$\alpha(\gamma_{i})=j_{i}$ for each $0\leq i\leq n$

  * •

the unique sequence $\gamma_{0},...,\gamma_{n}$ such that
$\alpha(\gamma_{i})=j_{i}$ for each $0\leq i\leq n$ is either not starting at
$\gamma$, not a complete
$\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-path or contains some
$\gamma^{\prime}$ such that $({\gamma^{\prime}},{\rho})\models{\varphi}$, as
$\rho$ and $\rho^{\prime}$ agree on $\textit{Var}\setminus\\{n,a,b\\}$.

According to the property of $\beta$, for each sequence $j_{0},...,j_{n}$
there exist some values for $a$ and $b$. Since $n$, $a$ and $b$ are chosen
arbitrary, we conclude that
$({\gamma},{\rho})\models{\overline{\textit{coreach}}({\varphi})}$ iff for all
complete $\mathrel{{\Rightarrow}_{\mathcal{}S}^{\mathcal{}T}}$-paths $\tau$
starting at $\gamma$, there exists some $\gamma^{\prime}\in\tau$ such that
$({\gamma^{\prime}},{\rho})\models{\varphi}$. By Lemma 7, we have that the
above iff $({\gamma},{\rho})\models{\textit{coreach}({\varphi})}$, and we are
done.

###  8.3. Encoding Semantic Validity in FOL

Now we can use the coreach predicate to encode the semantic validity of a rule
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ in FOL. Formally

######  Lemma 10.

If ${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$ then
$\models\varphi\rightarrow\textit{coreach}({\varphi^{\prime}})$.

######  Proof 8.43.

Follows from the definition of semantic validity of
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ and Lemma 7.

###  8.4. Relative Completeness

A matching logic formula $\psi$ is patternless iff $\square$ does not occur in
$\psi$. Then we have the following lemma stating that we can derive one step
on all paths

######  Lemma 11.

${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\mathcal{}C}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\psi}\Rightarrow^{\forall}{\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}\step{\textit{c}}{\textit{c}^{\prime}})\mathbin{\wedge}\psi}$
where $\psi$ is a patternless formula.

######  Proof 8.46.

We derive the rule by applying the Step proof rule with the following
prerequisites

$\models\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\ $

and for each $\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\ \in\ {\mathcal{}S}$
(since $\square$ does not occur in $\psi$)

$\models\exists\textit{c}^{\prime\prime}\
(\textit{c}^{\prime\prime}=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
$

For the first prerequisite, we have the following (using the definition of )

$\begin{array}[]{cl}&\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\psi\\\
\rightarrow&\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\\\
\leftrightarrow&\displaystyle\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\mu})\
({\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}{\varphi_{r}}[{\textit{c}^{\prime}}/\square])\\\
\rightarrow&\displaystyle\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\mu})\
{\varphi_{l}}[{\textit{c}}/\square]\\\
\rightarrow&\displaystyle\square=\textit{c}\mathbin{\wedge}\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\varphi_{l}})\
{\varphi_{l}}[{\textit{c}}/\square]\\\
\rightarrow&\displaystyle\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\varphi_{l}})\
\varphi_{l}\\\ \end{array}$

For the second prerequisite, let
$\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}$. Then we have
that

$\begin{array}[]{cl}&\exists\textit{c}^{\prime\prime}\
(\textit{c}^{\prime\prime}=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}{\varphi_{l}}[{\textit{c}^{\prime\prime}}/\square])\mathbin{\wedge}\varphi_{r}\mathbin{\wedge}\psi\\\
\rightarrow&{\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}\varphi_{r}\mathbin{\wedge}\psi\\\
\rightarrow&\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}{\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}{\varphi_{r}}[{\textit{c}^{\prime}}/\square])\mathbin{\wedge}\psi\\\
\rightarrow&\displaystyle\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}({\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}{\varphi_{r}}[{\textit{c}^{\prime}}/\square]))\mathbin{\wedge}\psi\\\
\rightarrow&\displaystyle\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}\bigvee_{\mu\equiv\varphi_{l}\Rightarrow^{\exists}\varphi_{r}\in{\mathcal{}S}}\exists\textit{FreeVars}({\mu})\
({\varphi_{l}}[{\textit{c}}/\square]\mathbin{\wedge}{\varphi_{r}}[{\textit{c}^{\prime}}/\square])\mathbin{\wedge}\psi\\\
\rightarrow&\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}\step{\textit{c}}{\textit{c}^{\prime}})\mathbin{\wedge}\psi\\\
\end{array}$

and we are done.

The following three lemmas show that we can derive a rule stating that all the
configurations reaching $\varphi$ in the transition system actually reach
$\varphi$.

######  Lemma 12.

If

${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square])}\Rightarrow^{\forall}{\varphi}$

then ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\textit{coreach}({\varphi})}\Rightarrow^{\forall}{\varphi}$.

######  Proof 8.57.

By Lemma 8

$\models\textit{coreach}({\varphi})\leftrightarrow\varphi\mathbin{\vee}(\exists\textit{c}^{\prime}\
$

Thus, by Consequence and Case Analysis, it suffices to derive

$\begin{array}[]{l}{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\varphi}\Rightarrow^{\forall}{\varphi}\\\
{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square])}\Rightarrow^{\forall}{\varphi}\\\
\end{array}$

The first sequent follows by Reflexivity. The second sequent is part of the
hypothesis, and we are done.

######  Lemma 13.

${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square])}\Rightarrow^{\forall}{\varphi}$

######  Proof 8.64.

Let $\mu$ be the rule we want to derive, namely

$\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\ $

Then ${\mathcal{}S},{\mathcal{}A}\ \mathrel{\vdash}{\mu}$ follows by
Circularity from ${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\\{\mu\\}}{\mu}$. Hence, by Transitivity, it suffices to
derive the two sequents below

$\begin{array}[]{l}{\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}_{\\{\mu\\}}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square])}\Rightarrow^{\forall}{\varphi^{\prime}}\\\
{\mathcal{}S},{{\mathcal{}A}\cup\\{\mu\\}}\
\mathrel{\vdash}{\varphi^{\prime}}\Rightarrow^{\forall}{\varphi}\\\
\end{array}$

where $\varphi^{\prime}\equiv\exists\textit{c}^{\prime}\
(\square=\textit{c}^{\prime}\mathbin{\wedge}$. The first sequent follows by
Lemma 11 with $\psi\equiv\forall\textit{c}^{\prime}\ ($. For the second
sequent, by Abstraction with $\\{\textit{c}^{\prime}\\}$ and Consequence with

$\models\square=\textit{c}^{\prime}\mathbin{\wedge}$

it suffices to derive ${\mathcal{}S},{{\mathcal{}A}\cup\\{\mu\\}}\
\mathrel{\vdash}{\textit{coreach}({\varphi})}\Rightarrow^{\forall}{\varphi}$.
Then, by Lemma 12, we are left to derive

${\mathcal{}S},{{\mathcal{}A}\cup\\{\mu\\}}\
\mathrel{\vdash}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow{\textit{coreach}({\varphi})}[{\textit{c}^{\prime}}/\square])}\Rightarrow^{\forall}{\varphi}$

that is, ${\mathcal{}S},{{\mathcal{}A}\cup\\{\mu\\}}\ \mathrel{\vdash}{\mu}$,
which trivially follows by Axiom and we are done.

######  Lemma 14.

${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\textit{coreach}({\varphi})}\Rightarrow^{\forall}{\varphi}$.

######  Proof 8.76.

By Lemma 12, it suffices to derive

${\mathcal{}S},{\mathcal{}A}\
\mathrel{\vdash}{\square=\textit{c}\mathbin{\wedge}\exists\textit{c}^{\prime}\
\step{\textit{c}}{\textit{c}^{\prime}}\mathbin{\wedge}\forall\textit{c}^{\prime}\
(\step{\textit{c}}{\textit{c}^{\prime}}\rightarrow\textit{coreach}({\varphi}))}\Rightarrow^{\forall}{\varphi}$

which follows by Lemma 13.

Finally, we can establish the main result. Assume
${\mathcal{}S}\models\varphi\Rightarrow^{\forall}\varphi^{\prime}$. By Lemma
10, we have that
$\models\varphi\rightarrow\textit{coreach}({\varphi^{\prime}})$. Further, by
Lemma 14, we have that
${\mathcal{}S}\vdash\textit{coreach}({\varphi^{\prime}})\Rightarrow^{\forall}\varphi^{\prime}$.
Then, by Consequence, it follows that
${\mathcal{}S}\vdash\varphi\Rightarrow^{\forall}\varphi^{\prime}$.

##  9\. Related Work

Using Hoare logic [20] to prove concurrent programs correct dates back to
Owicki and Gries [21]. In the rely-guarantee method proposed by Jones [22]
each thread relies on some properties being satisfied by the other threads,
and in its turn, offers some guarantees on which the other threads can rely.
O’Hearn [23] advances a Separation Hypothesis in the context of separation
logic [24] to achieve compositionality: the state can be partitioned into
separate portions for each process and relevant resources, respectively,
satisfying certain invariants. More recent research focuses on improvements
over both of the above methods and even combinations of them (e.g., [25, 26,
27, 28]).

The satisfaction of all-path-reachability rules can also be understood
intuitively in the context of temporal logics. Matching logic formulae can be
thought of as state formulae, and reachability rules as temporal formulae.
Assuming $\text{CTL}^{\ast}$ on finite traces, the semantics rule
$\varphi\Rightarrow^{\exists}\varphi^{\prime}$ can be expressed as
$\varphi\rightarrow E\bigcirc\varphi^{\prime}$, while an all-path reachability
rule $\varphi\Rightarrow^{\forall}\varphi^{\prime}$ can be expressed as
$\varphi\rightarrow A\Diamond\varphi^{\prime}$. However, unlike in
$\text{CTL}^{\ast}$, the $\varphi$ and $\varphi^{\prime}$ formulae of
reachability rules $\varphi\Rightarrow^{\exists}\varphi^{\prime}$ or
$\varphi\Rightarrow^{\forall}\varphi^{\prime}$ share their free variables.
Thus, existing proof systems for temporal logics (e.g., the
$\text{CTL}^{\ast}$ one by Pnueli and Kesten [29]) are not directly comparable
with our approach. In general, $\text{CTL}^{\ast}$ formulae only have atomic
predicates, while in our approach we consider only a specific temporal
structure ($\varphi\rightarrow A\Diamond\varphi^{\prime}$), but the matching
logic formulae $\varphi$ and $\varphi^{\prime}$ can express more complex state
properties.

This approach has been extended to handle safety properties of distributed
system, specified as rewrite theories [30]. Specifically, it can verify that
$\varphi$ is an invariant, or a co-invariant, of a non-terminating distributed
system by checking that $\varphi$ holds after each application of the Step
proof rule. The soundness of the approach is proved by transforming the
underlying transition system from non-terminating to terminating by adding a
transition from each state to a newly-introduced end state (where $\varphi$
does not hold).

Bae et al. [31], Rocha and Meseguer [32], and Rocha et al. [33] use narrowing
to perform symbolic reachability analysis in a transition system associated to
a unconditional rewrite theory for the purposes of verification. There are two
main differences between their work and ours. First, they express state
predicates in equational theories. Matching logic is more general, being
first-order logic over a model of configurations ${\mathcal{}T}$.
Consequently, the Step proof rule takes these issues into account when
considering the successors of a state. Second, they use rewrite systems for
symbolic model checking. Our work is complementary, in the sense that we use
the operational semantics for program verification, and check properties more
similar to those in Hoare logic.

Dynamic logic [34] adds modal operators to FOL to embed program fragments
within specifications. For example, $\psi\rightarrow[{\tt s}]\psi^{\prime}$
means “after executing s in a state satisfying $\psi$, a state may be reached
which satisfies $\psi^{\prime}$”. KeY [35] offers automatic verification for
Java based on dynamic logic. Dynamic logic has been extended to support
reasoning about cyber-physical systems, where the transitions may have a
continuous or probabilistic component [36]. Matching logic also combines
programs and specifications for static properties, but dynamic properties are
expressed in reachability logic which has a language-independent proof system
that works with any operational semantics, while dynamic logic still requires
language-specific proof rules (e.g., invariant rules for loops).

#### Language-independent proof systems

A first proof system is introduced in [6], while [5] presents a mechanical
translation from Hoare logic proof derivations for IMP into derivations in the
proof system. The Circularity proof rule is introduced in [4]. Finally, [7]
supports operational semantics given with conditional rules, like small-step
and big-step. All these previous results can only be applied to deterministic
programs. The coinductive nature of this proof system was clarified in [37],
which presents a coinduction principle that captures the essence of the
Circularity rule, and which is sufficient for program verification when used
within a system such as ZFC or Coq that already supports basic logical
reasoning and working with collections of configurations.

##  10\. Conclusion and Future Work

This paper introduces a sound and (relatively) complete language-independent
proof system which derives program properties holding along all execution
paths (capturing partial correctness for non-deterministic programs), directly
from an operational semantics. The proof system separates reasoning about
deterministic language features (via the operational semantics) from reasoning
about non-determinism (via the proof system). Thus, all we need in order to
verify programs in a language is an operational semantics for the respective
language.

We believe that existing techniques such as rely-guarantee and concurrent
separation logic could be used in conjunction with our proof system to achieve
semantically grounded and compositional verification.

Our approach handles operational semantics given with unconditional rules,
like in the $\mathbb{K}$ framework, PLT-Redex, and CHAM, but it cannot handle
operational semantics given with conditional rules, like big-step and small-
step (rules with premises). Extending the presented results to work with
conditional rules would boil down to extending the Step proof rule, which
derives the fact that $\varphi$ reaches $\varphi^{\prime}$ in one step along
all execution paths. Such an extended Step would have as prerequisites whether
the left-hand side of a semantics rule matches (like the existing Step) and
additionally whether its premises hold. The second part would require an
encoding of reachability in first-order logic, which is non-trivial and most
likely would result in a first-order logic over a richer model than
$\mathcal{}T$. The difficulty arises from the fact that Step must ensure all
successors of $\varphi$ are in $\varphi^{\prime}$. Thus, this extension is
left as future work.

#### Acknowledgements

We would like to thank the anonymous reviewers and the FSL members for their
valuable feedback on an early version of this paper. The work presented in
this paper was supported in part by the Boeing grant on "Formal Analysis Tools
for Cyber Security" 2014-2015, the NSF grant CCF-1218605, the NSA grant
H98230-10-C-0294, the DARPA HACMS program as SRI subcontract 19-000222, the
Rockwell Collins contract 4504813093, and the (Romanian) SMIS-CSNR 602-12516
contract no. 161/15.06.2010.

## References

  * [1] Nipkow, T.:  Winskel is (almost) right: Towards a mechanized semantics textbook.  Formal Aspects of Computing 10 (1998) 171–186
  * [2] Jacobs, B.:  Weakest pre-condition reasoning for Java programs with JML annotations.  J. Logic and Algebraic Programming 58(1-2) (2004) 61–88
  * [3] Appel, A.W.:  Verified software toolchain.  In: ESOP. Volume 6602 of LNCS. (2011) 1–17
  * [4] RoԷu, G., Զtefănescu, A.:  Checking reachability using matching logic.  In: OOPSLA, ACM (2012) 555–574
  * [5] RoԷu, G., Զtefănescu, A.:  From Hoare logic to matching logic reachability.  In: FM. Volume 7436 of LNCS. (2012) 387–402
  * [6] RoԷu, G., Զtefănescu, A.:  Towards a unified theory of operational and axiomatic semantics.  In: ICALP. Volume 7392 of LNCS. (2012) 351–363
  * [7] Roşu, G., Ştefănescu, A., Ciobâcă, S., Moore, B.M.:  One-path reachability logic.  In: LICS, IEEE (2013) 358–367
  * [8] RoԷu, G., Ellison, C., Schulte, W.:  Matching logic: An alternative to Hoare/Floyd logic.  In: AMAST. Volume 6486 of LNCS. (2010) 142–162
  * [9] RoԷu, G., ԶerbănuԹă, T.F.:  An overview of the K semantic framework.  J. Logic and Algebraic Programming 79(6) (2010) 397–434
  * [10] Ştefănescu, A., Ciobâcă, S., Mereuţă, R., Moore, B.M., Şerbănuţă, T.F., Roşu, G.:  All-path reachability logic.  In: RTA. Volume 8560 of LNCS. (July 2014) 425–440
  * [11] Roşu, G.:  Matching logic.  Logical Methods in Computer Science 13(4) (December 2017) 1–61
  * [12] Roşu, G.:  Matching logic — extended abstract.  In: RTA. Volume 36 of Leibniz International Proceedings in Informatics (LIPIcs)., Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2015) 5–21
  * [13] Ellison, C., RoԷu, G.:  An executable formal semantics of C with applications.  In: POPL, ACM (2012) 533–544
  * [14] Hathhorn, C., Ellison, C., Rosu, G.:  Defining the undefinedness of C.  In: PLDI, ACM (2015) 336–345
  * [15] Felleisen, M., Findler, R.B., Flatt, M.:  Semantics Engineering with PLT Redex.  MIT (2009)
  * [16] Berry, G., Boudol, G.:  The chemical abstract machine.  Theoretical Computer Science 96(1) (1992) 217–248
  * [17] Matthews, J., Findler, R.B.:  An operational semantics for Scheme.  JFP 18(1) (2008) 47–86
  * [18] Filaretti, D., Maffeis, S.:  An executable formal semantics of PHP.  In: ECOOP. Volume 8586 of LNCS. (2014) 567–592
  * [19] de Moura, L.M., Bjørner, N.:  Z3: An efficient SMT solver.  In: TACAS. Volume 4963 of LNCS. (2008) 337–340
  * [20] Hoare, C.A.R.:  An axiomatic basis for computer programming.  Communications of the ACM 12(10) (1969) 576–580
  * [21] Owicki, S.S., Gries, D.:  Verifying properties of parallel programs: An axiomatic approach.  Communications of the ACM 19(5) (1976) 279–285
  * [22] Jones, C.B.:  Specification and design of (parallel) programs.  In Mason, R.E.A., ed.: Information Processing 1983: World Congress Proceedings, Elsevier (1984) 321–332
  * [23] O’Hearn, P.W.:  Resources, concurrency, and local reasoning.  Theoretical Computer Science 375(1-3) (2007) 271–307
  * [24] Reynolds, J.C.:  Separation logic: A logic for shared mutable data structures.  In: LICS, IEEE (2002) 55–74
  * [25] Feng, X.:  Local rely-guarantee reasoning.  In: POPL, ACM (2009) 315–327
  * [26] Vafeiadis, V., Parkinson, M.J.:  A marriage of rely/guarantee and separation logic.  In: CONCUR. Volume 4703 of LNCS. (2007) 256–271
  * [27] Reddy, U.S., Reynolds, J.C.:  Syntactic control of interference for separation logic.  In: POPL, ACM (2012) 323–336
  * [28] Hayman, J.:  Granularity and concurrent separation logic.  In: CONCUR. Volume 6901 of LNCS. (2011) 219–234
  * [29] Pnueli, A., Kesten, Y.:  A deductive proof system for $CTL^{\ast}$.  In: CONCUR. Volume 2421 of LNCS. (2002) 24–40
  * [30] Skeirik, S., Ştefănescu, A., Meseguer, J.:  A constructor-based reachability logic for rewrite theories.  In: LOPSTR. Volume 10855 of LNCS., Springer (2017) 201–217
  * [31] Bae, K., Escobar, S., Meseguer, J.:  Abstract logical model checking of infinite-state systems using narrowing.  In: RTA. (2013) 81–96
  * [32] Rocha, C., Meseguer, J.:  Proving safety properties of rewrite theories.  In: CALCO. Volume 6859 of LNCS. (2011) 314–328
  * [33] Rocha, C., Meseguer, J., Muñoz, C.A.:  Rewriting modulo SMT and open system analysis.  In: WRLA. Volume 8663 of LNCS., Springer (2014) 247–262
  * [34] Harel, D., Kozen, D., Tiuryn, J.:  Dynamic logic.  In: Handbook of Philosophical Logic. (1984) 497–604
  * [35] Beckert, B., Hähnle, R., Schmitt, P.H.:  Verification of Object-oriented Software: The KeY Approach.  Springer-Verlag (2007)
  * [36] Madeira, A., Neves, R., Martins, M.A., Barbosa, L.S.:  A dynamic logic for every season.  In: SBMF. Volume 8941 of LNCS., Springer (2014) 130–145
  * [37] Moore, B., Peña, L., Roşu, G.:  Program verification by coinduction.  In: 27th European Symposium on Programming (ESOP). (April 2018)