Program Analysis Is Harder Than Verification: A Computability Perspective

Abstract

We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.

1 Introduction

It is common to assume that program analysis is harder than program verification (e.g. [1, 17, 22]). The intuition is that this happens because in program analysis we need to synthesize a correct program invariant while in program verification we have just to check whether a given program invariant is correct. The distinction between checking a proof and computing a witness for that proof can be traced back to Leibniz [18] in his ars iudicandi and ars inveniendi, respectively representing the analytic and synthetic method. In Leibniz’s ars combinatoria, the ars inveniendi is defined as the art of discovering “correct” questions while ars iudicandi is defined as the art of discovering “correct” answers. These foundational aspects of mathematical reasoning have a peculiar meaning when dealing with questions and answers concerning the behaviour of computer programs as objects of our investigation.

Our main goal is to define a general and precise model for reasoning on the computability aspects of the notions of (sound or complete) static analyser and verifier for generic programs (viz. Turing machines). Both static analysers and verifiers assume a given domain A of abstract program assertions, that may range from synctatic program properties (e.g., program sizes or LOCs) to complexity properties (e.g., number of execution steps in some abstract machine) and all the semantic properties of the program behaviour (e.g., value range of program variables or shape of program memories). A program analyser is defined to be any total computable (i.e., total recursive) function that for any program P returns an assertion $a_P$ in A, which is sound when the concrete meaning of the assertion $a_P$ includes P. Instead, a program verifier is a (total) decision procedure which is capable of checking whether a given program P satisfies a given assertion a ranging in A, answering “true” or “don’t know”, which is sound when a positive check of a for P means that the concrete meaning of the assertion a includes P. Completeness, which coupled with soundness is here called precision, for a program analyser holds when, for any program P, it returns the strongest assertion in A for P, while a program verifier is called precise if it is able to prove any true assertion in A for a program P. This general and minimal model allows us to extend to static program analysis and verification some standard results and methods of computability theory. We provide an instance of the well-known Rice’s Theorem [29] for generic analysers and verifiers, by proving that sound and precise analysers (resp. verifiers) exist only for trivial domains of assertions. This allows us to generalise known results about undecidability of program analysis, such as the undecidability of the meet over all paths (MOP) solution for monotone dataflow analysis frameworks [15], making them independent from the structure of the domain of assertions. Then, we define a model for comparing the relative “verification power” of program analysers and verifiers. In this model, a verifier ${{\mathrm{\mathcal {V}}}}$ on a domain A of assertions is more precise than an analyser ${{\mathrm{\mathcal {A}}}}$ on the same domain A when any assertion a in A which can be proved by ${{\mathrm{\mathcal {A}}}}$ for a program P—this means that the output of the analyser ${{\mathrm{\mathcal {A}}}}(P)$ is stronger than the assertion a—can be also proved by ${{\mathrm{\mathcal {V}}}}$. Conversely, ${{\mathrm{\mathcal {A}}}}$ is more precise than ${{\mathrm{\mathcal {V}}}}$ when any assertion a proved by ${{\mathrm{\mathcal {V}}}}$ can be also proved by ${{\mathrm{\mathcal {A}}}}$. We prove that while it is always possible to constructively transform a program analyser into an equivalent verifier (i.e., with the same verification power), the converse does not hold in general. In fact, we first show that for finite domains of assertions, any “reasonable” verifier can be constructively transformed into an equivalent analyser, where reasonable means that the verifier ${{\mathrm{\mathcal {V}}}}$ is: (i) nontrivial: for any program, ${{\mathrm{\mathcal {V}}}}$ is capable to prove some assertion, possibly a trivially true assertion; (ii) monotone: if ${{\mathrm{\mathcal {V}}}}$ proves an assertion a and a is stronger than $a'$ then ${{\mathrm{\mathcal {V}}}}$ is also capable of proving $a'$; (iii) logically meet-closed: if ${{\mathrm{\mathcal {V}}}}$ proves both $a_1$ and $a_2$ and the logical conjunction $a_1\wedge a_2$ is a representable assertion then ${{\mathrm{\mathcal {V}}}}$ is also capable of proving it. Next, we prove the following impossibility result: for any infinite abstract domain of assertions A, no constructive reduction from reasonable verifiers on A to equivalent analysers on A is possible. This provides, to the best of our knowledge, the first formalization of the common folklore that program analysis is harder than program verification.

2 Background

We follow the standard terminology and notation for sets and computable functions in recursion theory (e.g., [12, 26, 30]). If X and Y are sets then $X\rightarrow Y$ and ${XY}$ denote, respectively, the set of all total and partial functions from X to Y. If $f:XY$ then $f(x){\downarrow \,}$ and $f(x){\uparrow \,}$ mean that f is defined/undefined on $x\in X$. Hence ${{\mathrm{dom}}}(f) = \{x\in X~|~f(x){\downarrow \,}\}$. If $S\subseteq Y$ then $f(x)\in S$ denotes the implification $f(x){\downarrow \,}\Rightarrow f(x)\in S$. If $f,g:XY$ then $f=g$ means that ${{\mathrm{dom}}}(f)={{\mathrm{dom}}}(g)$ and for any $x\in {{\mathrm{dom}}}(f)={{\mathrm{dom}}}(g)$, $f(x)=g(x)$. The set of all partial (total) recursive functions on natural numbers is denoted by (). Recall that $A\subseteq \mathbb {N}$ is a recursively enumerable (r.e., or semidecidable) set if $A={{\mathrm{dom}}}(f)$ for some , while $A\subseteq \mathbb {N}$ is a recursive (or decidable) set if both A and its complement $\bar{A}=\mathbb {N}\smallsetminus A$ are recursively enumerable, and this happens when there exists such that $f = \lambda n.\, n\in A~ \mathbf ? ~ 1~ \mathbf : ~ 0$.

Let ${{\mathrm{Prog}}}$ denote some deterministic programming language which is Turing complete. More precisely, this means that for any partial recursive function there exists a program $P\in {{\mathrm{Prog}}}$ such that ${\llbracket P \rrbracket }\cong f$, where ${\llbracket P \rrbracket }:DD$ is a denotational input/output semantics of P on a domain D of input/output values for ${{\mathrm{Prog}}}$, where: undefinedness encodes nontermination and $\cong$ means equality up to some recursive encoding ${{\mathrm{enc}}}:D {\mathop {\rightarrow }\limits ^{\scriptscriptstyle \mathrm {r}}}\mathbb {N}$ and decoding ${{\mathrm{dec}}}:\mathbb {N}{\mathop {\rightarrow }\limits ^{\scriptscriptstyle \mathrm {r}}}D$ functions, i.e., $f={{\mathrm{enc}}}\circ {\llbracket P \rrbracket }\circ {{\mathrm{dec}}}$. We also assume a small-step transition relation $\Rightarrow \, \subseteq ({{\mathrm{Prog}}}\times D) \times ( ({{\mathrm{Prog}}}\times D)\cup D)$ for ${{\mathrm{Prog}}}$ defining an operational semantics which is functionally equivalent to the denotational semantics: $\langle P,i \rangle \Rightarrow ^* o$ iff ${\llbracket P \rrbracket }i=o$. By an abuse of notation, we will identify the input/output semantics of a program P with the partial recursive function computed by P, i.e., we will consider programs $P\in {{\mathrm{Prog}}}$ whose input/output semantics is a partial recursive function , so that, by Turing completeness, .

3 Abstract Domains

Static program analysis and verification are always defined with respect to a given (denumerable) domain of program assertions, that we call here abstract domain [7], where the meaning of assertions is formalized by a function which induces a logical implication relation between assertions.

Definition 3.1

(Abstract Domain). An abstract domain is a tuple $\langle A,\gamma ,\le _\gamma \rangle$ such that:

• (1) A is any denumerable set;

• (2) $\gamma : A \rightarrow \wp ({{\mathrm{Prog}}})$ is any function;

• (3) $\le _\gamma \,\,\triangleq \, \{(a_1,a_2)\in A\times A~|~ \gamma (a_1) \subseteq \gamma (a_2)\}$ is a decidable relation.

An abstract element $a\in A$ such that $\gamma (a)={{\mathrm{Prog}}}$ is called an abstract top, while a is called an abstract bottom when $\gamma (a)=\varnothing$.    $\square$

The elements of A are called assertions or abstract values, $\gamma$ is called concretization function (this may also be a nonrecursive function, which is typical of abstract domains representing semantic program properties), and $\le _\gamma$ is called the implication or approximation relation of A. Thus, in this general model, a program assertion $a\in A$ plays the role of some abstract representation of any program property $\gamma (a)\in \wp ({{\mathrm{Prog}}})$, while the comparison relation $a_1\le _\gamma a_2$ holds when $a_1$ is a stronger (or more precise) property than $a_2$. Let us also observe that, as a limit case, Definition 3.1 allows an abstract domain to be empty, that is, the tuple $\langle \varnothing ,\varnothing ,\varnothing \rangle$ satisfies the definition of abstract domain, where $\varnothing$ denotes both the empty set, the empty function (i.e., the unique subset of $\varnothing \times \varnothing$) and the empty relation.

Example 3.2

Let us give some simple examples of abstract domains.

• (1) Consider $A=\mathbb {N}$ with $\gamma (n)\triangleq \{P\in {{\mathrm{Prog}}}~|~ {{\mathrm{size}}}(P)\le n\}$, where ${{{\mathrm{size}}}:{{\mathrm{Prog}}}\rightarrow \mathbb {N}}$ is some computable program size function. Here, $\le _\gamma$ is clearly decidable and coincides with the partial order $\le _\mathbb {N}$ on numbers.

• (2) Consider $A=\mathbb {N}$ with $\gamma (n) \triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i. \exists o,k. (\langle P,i \rangle \Rightarrow ^k o) \, \& \, k\le n \}$, i.e., n represents all the programs which, given any input, terminate in at most n steps. Here again, $n\le _\gamma m$ iff $n\le _\mathbb {N}m$, so that $\le _\gamma$ is decidable.

• (3) Consider $A=\mathbb {N}$ with $\gamma (n)\triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i\in [0,n].\exists o.\, \langle P,i \rangle \Rightarrow ^* o\}$, that is, n represents all the programs which terminate for any input $i\le n$. Once again, $n\le _\gamma m$ iff $n\le _\mathbb {N}m$.

• (4) Consider $A=\mathbb {N}$ with $\gamma (n)\triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i\in \mathbb {N}.\, {\llbracket P \rrbracket }(i)=o \Rightarrow o\le n\}$, that is, n represents those programs which, in case of termination, give an output o bounded by n. Again, $n\le _\gamma m$ iff $n\le _\mathbb {N}m$.

• (5) Consider with $\gamma (g)\triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i.\, \big (g(i){\downarrow \,}\Rightarrow (\exists o,k. \langle P,i \rangle \Rightarrow ^k o,\, k\le g(i))\big ) \wedge \big ( (\exists o,k. \langle P,i \rangle \Rightarrow ^k o) \Rightarrow g(i){\downarrow \,},\, k\le g(i)\big )\}$, that is, g represents those programs whose time complexity is bounded by the function g. Here, $g \le _\gamma g'$ iff $\forall i.\, g(i){\downarrow \,}\Rightarrow (g'(i){\downarrow \,}\,\wedge \, g(i) \le g'(i))$.    $\square$

Definition 3.1 does not require injectivity of the concretization function $\gamma$, thus multiple assertions could have the same meaning. Two abstract values $a_1,a_2\in A$ are called equivalent when $\gamma (a_1)=\gamma (a_2)$. Let us observe that since $\le _\gamma$ is required to be decidable, the equivalence $\gamma (a_1) = \gamma (a_2)$ is decidable as well. For example, for the well-known numerical abstract domain of convex polyhedra [11] represented through linear constraints between program variables, we may well have multiple representations $P_1$ and $P_2$ for the same polyhedron, e.g., $P_1=\{x=z,z\le y\}$ and $P_2=\{x=z,x\le y\}$ both represent the same polyhedron. Thus, in general, an abstract domain A is not required to be partially ordered by $\le _\gamma$. On the other hand, the relation $\le _\gamma$ is clearly a preorder on A. The only basic requirement is that for any pair of abstract values $a_1,a_2\in A$, one can decide if $a_1$ is a more precise program assertion than $a_2$, i.e., if $\gamma (a_1) \subseteq \gamma (a_2)$ holds. In this sense we do not require that a partial order $\le$ is defined a priori on A and that $\gamma$ is monotone w.r.t. $\le$, since for our purposes it is enough to consider the preorder $\le _\gamma$ induced by $\gamma$. If instead A is endowed with a partial order $\le _A$ and A is defined in abstract interpretation [7, 8] through a Galois insertion based on the concretization map $\gamma$, then it turns out that $\gamma (a_1) \subseteq \gamma (a_2) \Leftrightarrow a_1 \le _A a_2$ holds, so that the decidability of the relation $\le _\gamma \, = \{(a_1,a_2)\in A\times A~|~ \gamma (a_1) \subseteq \gamma (a_2)\}$ boils down to the decidability of the partial order relation $\le _A$. As an example, it is well known that the abstract domain of polyhedra does not admit a Galois insertion [11], nevertheless its induced preorder relation $\le _\gamma$ is decidable: for example, for polyhedra represented by linear constraints, there exist algorithms for deciding if $\gamma (P_1) \subseteq \gamma (P_2)$ for any pair of convex polyhedra representations $P_1$ and $P_2$ (see e.g. [23, Sect. 5.3]).

3.1 Abstract Domains in Abstract Interpretation

An abstract domain in standard abstract interpretation [7,8,9] is usually defined by a poset $\langle A,\le _A \rangle$ containing a top element $\top \in A$ and a concretization map $\gamma _A:A\rightarrow \wp ({{\mathrm{Dom}}})$, where ${{\mathrm{Dom}}}$ denotes some concrete semantic domain (e.g., program stores or program traces), such that: (a) A is machine representable, namely the abstract elements of A are encoded by some data structures (e.g., tuples, vectors, lists, matrices, etc.), and some algorithms are available for deciding if $a_1\le _A a_2$ holds; (b) $a_1 \le _A a_2 \Leftrightarrow \gamma _A(a_1) \subseteq \gamma _A(a_2)$ holds (this equivalence always holds for Galois insertions); (c) $\gamma _A(\top )={{\mathrm{Dom}}}$. Let us point out that Definition 3.1 is very general since the concretization of an abstract value can be any program property, possibly a purely syntactic property or some space or time complexity property, as in the simple cases of Example 3.2 (1)-(2)-(5).

Let $\gamma _A:A\rightarrow \wp ({{\mathrm{Dom}}})$ and assume that ${{\mathrm{Dom}}}$ is defined by program stores, namely ${{\mathrm{Dom}}}\triangleq {{\mathrm{Var}}}\rightarrow {{\mathrm{Val}}}$, where ${{\mathrm{Var}}}$ is a finite set of program variables and ${{\mathrm{Val}}}$ is a corresponding denumerable set of values. Since ${{\mathrm{Var}}}\rightarrow {{\mathrm{Val}}}$ has a finite domain and a denumerable range, we can assume a recursive encoding of finite tuples of values into natural numbers $\mathbb {N}$, i.e. ${{\mathrm{Var}}}\rightarrow {{\mathrm{Val}}}\cong \mathbb {N}$, and define $\gamma _A:A\rightarrow \wp (\mathbb {N})$. This is equivalent assuming that programs have one single variable, say x, which may assume tuples of values in ${{\mathrm{Val}}}$. A set of numbers $\gamma _A(a)\in \wp (\mathbb {N})$ is meant to represent a property of the values stored in the program variable x at the end of the program execution, that is, if the program terminates its execution then the variable x stores a value in $\gamma _A(a)$. Hence, as usual, the property $\varnothing \in \wp (\mathbb {N})$ means that the program does not correctly terminate its execution either by true nontermination or by some run-time error, namely, that the exit program point is not reachable. For simplicity, we do not consider intermediate program points and assertions in our semantics.

For an abstract domain $\langle A,\gamma _A,\le _A \rangle$ in standard abstract interpretation, the corresponding concretization function $\gamma : A\rightarrow \wp ({{\mathrm{Prog}}})$ of Definition 3.1 is defined as:

$$ \gamma (a) \triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i\in \mathbb {N}.\, {\llbracket P \rrbracket }(i) \in \gamma _{A} (a)\} $$

where we recall that ${\llbracket P \rrbracket }(i) \in \gamma _{A} (a)$ means ${\llbracket P \rrbracket }(i)=o \Rightarrow o \in \gamma _{A} (a)$. Hence, if A contains top $\top _A$ and bottom $\bot _A$ such that $\gamma _A(\top _A)=\mathbb {N}$ and $\gamma _A(\bot _A)=\varnothing$ then $\gamma (\top _A) = {{\mathrm{Prog}}}$ and $\gamma (\bot _A)= \{P\in {{\mathrm{Prog}}}~|~P \text {~never terminates}\}$. Moreover, since $\gamma _A$ is monotonic, we have that $\gamma$ is monotonic as well. The fact that all the elements in A are machine representable boils down to the requirement that A is a recursive set, while the binary preorder relation $\le _{\gamma }$ is decidable because $a_1 \le _A a_2 \Leftrightarrow \gamma (a_1) \subseteq \gamma (a_2)$ holds and $\le _A$ is decidable. This therefore defines an abstract domain according to Definition 3.1.

In this simple view of the abstract domain A, there is no input property for the variable x, meaning that at the beginning x may store any value. It is easy to generalize the above definition by requiring an input abstract property in A for x, so that the abstract domain is a Cartesian product $A\times A$ together with a concretization $\gamma ^{i\!/\!o}: A\times A \rightarrow \wp ({{\mathrm{Prog}}})$ defined as follows:

$$ \gamma ^{i\!/\!o}(\langle a_i,a_o \rangle ) \triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i\in \mathbb {N}.\,i \in \gamma _{A}(a_i) \Rightarrow {\llbracket P \rrbracket }(i) \in \gamma _{A} (a_o)\}. $$

This is a generalization since, for any $a\in A$, we have that $\gamma (a)=\gamma ^{i\!/\!o}(\langle \top _A,a \rangle )$.

Example 3.3

(Interval Abstract Domain). Let ${{\mathrm{Int}}}$ be the standard interval domain [7] restricted to natural numbers in $\mathbb {N}$, endowed with the standard subset ordering:

$$ {{\mathrm{Int}}}\triangleq \{[a,b] ~|~ a,b\in \mathbb {N},\, a\le b\} \cup \{\bot _{{{\mathrm{Int}}}}\} \cup \{[a,+\infty )~|~a\in \mathbb {N}\} $$

with concretization $\gamma _{{{\mathrm{Int}}}} : {{\mathrm{Int}}}\rightarrow \wp (\mathbb {N})$, where $\gamma _{{{\mathrm{Int}}}}(\bot _{{{\mathrm{Int}}}})=\varnothing$, $\gamma _{{{\mathrm{Int}}}}([a,b])=[a,b]$ and $\gamma _{{{\mathrm{Int}}}}([0,+\infty ))=\mathbb {N}$, so that $[0,+\infty )$ is also denoted by $\top _{{{\mathrm{Int}}}}$. Thus, here, for the concretization function $\gamma : {{\mathrm{Int}}}\rightarrow \wp ({{\mathrm{Prog}}})$ we have that: $\gamma (\top _{{{\mathrm{Int}}}}) = {{\mathrm{Prog}}}$, $\gamma (\bot _{{{\mathrm{Int}}}})= \{P\in {{\mathrm{Prog}}}~|~\forall i.\,{\llbracket P \rrbracket }(i){\uparrow \,}\}$, $\gamma ([a,+\infty )) =\{P\in {{\mathrm{Prog}}}~|~ \forall i\in \mathbb {N}.\, {\llbracket P \rrbracket }(i){\downarrow \,}\Rightarrow {\llbracket P \rrbracket }(i)\ge a\}$. We also have the input/output concretization $\gamma ^{i\!/\!o}: {{\mathrm{Int}}}\times {{\mathrm{Int}}}\rightarrow \wp ({{\mathrm{Prog}}})$, where

$$ \gamma ^{i\!/\!o}(\langle I,J \rangle ) \triangleq \{P\in {{\mathrm{Prog}}}~|~ \forall i\in \mathbb {N}.\, i \in \gamma _{{{\mathrm{Int}}}}(I) \Rightarrow {\llbracket P \rrbracket }(i) \in \gamma _{{{\mathrm{Int}}}} (J)\}. $$

   $\square$

4 Program Analysers and Verifiers

In our model, the notions of program analyser and verifier are as general as possible.

Definition 4.1

(Program Analyser). Given an abstract domain $\langle A,\gamma , \le _\gamma \rangle$, a program analyser on A is any total recursive function ${{\mathrm{\mathcal {A}}}}:{{\mathrm{Prog}}}\rightarrow A$.

The set of analysers on a given abstract domain A will be denoted by ${{\mathrm{\mathbb {A}}}}_A$.

An analyser ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ is sound if for any $P\in {{\mathrm{Prog}}}$ and $a\in A$,

$$ {{\mathrm{\mathcal {A}}}}(P) \le _\gamma a \,\Rightarrow \, P \in \gamma (a) $$

while ${{\mathrm{\mathcal {A}}}}$ is precise if it is also complete, i.e., if the reverse implication also holds:

$$ P \in \gamma (a) \,\Rightarrow \, {{\mathrm{\mathcal {A}}}}(P) \le _\gamma a. $$

   $\square$

Notice that this definition of soundness is equivalent to the standard notion of sound static analysis, namely, for any program P, ${{\mathrm{\mathcal {A}}}}(P)$ always outputs a program assertion which is satisfied by P, i.e., $P \in \gamma ({{\mathrm{\mathcal {A}}}}(P))$. Let us also note that on the empty abstract domain $\varnothing$, no analyser can be defined simply because there exists no function in ${{\mathrm{Prog}}}\rightarrow \varnothing$. Instead, for a singleton abstract domain $A_\bullet \triangleq \{\bullet \}$, if ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_{A_\bullet }$ is sound then $\gamma (\bullet )={{\mathrm{Prog}}}$, so that $\bullet$ is necessarily an abstract top. Also, if the abstract domain A contains a top abstract value $\top _A\in A$ then, as expected, $\lambda P.\top _A$ is a trivially sound analyser on A. Finally, we observe that if ${{\mathrm{\mathcal {A}}}}_1$ and ${{\mathrm{\mathcal {A}}}}_2$ are both precise on the same abstract domain then we have ${{\mathrm{\mathcal {A}}}}_1=_\gamma {{\mathrm{\mathcal {A}}}}_2$, meaning that ${{\mathrm{\mathcal {A}}}}_1$ and ${{\mathrm{\mathcal {A}}}}_2$ coincide up to equivalent abstract values, i.e., $\gamma \circ {{\mathrm{\mathcal {A}}}}_1 = \gamma \circ {{\mathrm{\mathcal {A}}}}_2$. In fact, for any $P\in {{\mathrm{Prog}}}$, we have that $P\in \gamma ({{\mathrm{\mathcal {A}}}}_2(P))$ implies $\gamma ({{\mathrm{\mathcal {A}}}}_1(P))\subseteq \gamma ({{\mathrm{\mathcal {A}}}}_2(P))$ and $P\in \gamma ({{\mathrm{\mathcal {A}}}}_1(P))$ implies $\gamma ({{\mathrm{\mathcal {A}}}}_2(P)) \subseteq \gamma ({{\mathrm{\mathcal {A}}}}_1(P))$, so that ${{\mathrm{\mathcal {A}}}}_1=_\gamma {{\mathrm{\mathcal {A}}}}_2$.

Example 4.2

Software metrics static analysers [35] deal with nonsemantic program properties, such as the domain in Example 3.2 (1). Bounded model checking [4, 34] handles program properties such as those encoded by the domains of Example 3.2 (2)-(3). Complexity bound analysers such as [32, 36] cope with domains of properties such as those in Example 3.2 (4)-(5). Numerical abstract domains used in program analysis (see [23]) include the interval abstraction described in Example 3.3.    $\square$

Definition 4.3

(Program Verifier). Given an abstract domain $\langle A,\gamma ,\le _\gamma \rangle$, a program verifier on A is any total recursive function ${{\mathrm{\mathcal {V}}}}:{{\mathrm{Prog}}}\times A \rightarrow \{\mathbf {t},\mathbf ? \}$.

The set of verifiers on a given abstract domain A will be denoted by ${{\mathrm{\mathbb {V}}}}_A$.

A verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is sound if for any $P\in {{\mathrm{Prog}}}$ and $a\in A$,

$$ {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\,\Rightarrow \, P \in \gamma (a) $$

while ${{\mathrm{\mathcal {V}}}}$ is precise if it is also complete, i.e., if the reverse implication also holds:

$$ P \in \gamma (a) \,\Rightarrow \, {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}. $$

A verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is nontrivial if for any program there exists at least one assertion which ${{\mathrm{\mathcal {V}}}}$ is able to prove, i.e., for any $P\in {{\mathrm{Prog}}}$ there exists some $a\in A$ such that ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$. Also, a verifier is defined to be trivial when it is not nontrivial.

A verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is monotone when the verification algorithm is monotone w.r.t. $\le _\gamma$, i.e., $({{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\;\wedge \; a\le _\gamma a') \;\Rightarrow \; {{\mathrm{\mathcal {V}}}}(P,a')=\mathbf {t}$.    $\square$

Remark 4.4

Let us observe some straight consequences of Definition 4.3.

(1)  Notice that for all nonempty abstract domains A, $\lambda (P,a).\,\mathbf ?$ is a legal and vacuously sound verifier. Also, if $A=\varnothing$ is the empty abstract domain then the empty verifier ${{\mathrm{\mathcal {V}}}}: {{\mathrm{Prog}}}\times \varnothing \rightarrow \{\mathbf {t},\mathbf ? \}$ (namely, the function with empty graph) is trivially precise.

(2)  Let us observe that if ${{\mathrm{\mathcal {V}}}}$ is nontrivial and monotone then ${{\mathrm{\mathcal {V}}}}$ is able to prove any abstract top: in fact, if $\top \in A$ and $\gamma (\top )={{\mathrm{Prog}}}$ then, for any $P\in {{\mathrm{Prog}}}$, since there exists some $a\in A$ such that ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$ and $a\le _\gamma \top$, then, by monotonicity, ${{\mathrm{\mathcal {V}}}}(P,\top )=\mathbf {t}$.

(3)  Note that if a verifier ${{\mathrm{\mathcal {V}}}}$ is precise then ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf ? \Leftrightarrow P\not \in \gamma (a)$, so that in this case an output ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf ?$ always means that P does not satisfy the property a.

(4)  Finally, if ${{\mathrm{\mathcal {V}}}}_1$ and ${{\mathrm{\mathcal {V}}}}_2$ are precise on the same abstract domain then ${{\mathrm{\mathcal {V}}}}_1(P,a) =\mathbf {t}\Leftrightarrow P\in \gamma (a) \Leftrightarrow {{\mathrm{\mathcal {V}}}}_2(P,a)=\mathbf {t}$, so that ${{\mathrm{\mathcal {V}}}}_1={{\mathrm{\mathcal {V}}}}_2$.    $\square$

Example 4.5

Program verifiers abund in literature, e.g., [3, 21, 27]. For example, [13] aims at complexity verification on domains like that in Example 3.2 (5) while reachability verifiers like [33] can check numerical properties of program variables such as those of Example 3.3.    $\square$

5 Rice’s Theorem for Static Program Analysis and Verification

Classical Rice’s Theorem in computability theory [26, 29, 30] states that an extensional property $\varPi \subseteq \mathbb {N}$ of an effective numbering of partial recursive functions is a recursive set if and only if $\varPi =\varnothing$ or $\varPi =\mathbb {N}$, i.e., $\varPi$ is trivial. Let us recall that $\varPi \subseteq \mathbb {N}$ is extensional when $\varphi _n=\varphi _m$ implies $n\in \varPi ~\Leftrightarrow ~ m\in \varPi$. When dealing with program properties rather than indices of partial recursive functions, i.e., when $\varPi \subseteq {{\mathrm{Prog}}}$, Rice’s Theorem states that any nontrivial semantic program property is undecidable (see [28] for a statement of Rice’s Theorem tailored for program properties). It is worth recalling that Rice’s Theorem has been extended by Asperti [2] through an interesting generalization to so-called “complexity cliques”, namely nonextensional program properties which may take into account the space or time complexity of programs: for example, the abstract domain of Example 3.2 (5) is not extensional but when logically “intersected” with an extensional domain (i.e., it is a product domain $A_1\times A_2$ where the concretization function is the set intersection $\lambda \langle a_1,a_2 \rangle .\gamma _1(a_1)\cap \gamma _2(a_2)$) falls into this generalized version of Rice’s Theorem.

In the following, we provide an instantiation of Rice’s Theorem to sound static program analysis and verification by introducing a notion of extensionality for abstract domains. Abstract domains commonly used in abstract interpretation turn out to be extensional, when they are used for approximating the input/output behaviour of programs. For example, if a sound abstract interpretation of a program P in the interval abstract domain computes as abstract output a program assertion such as $x\in [1,5]$ and $y\in [2,+\infty )$ then this assertion is a sound abstract output for any other program Q having the same input/output behaviour of P.

Definition 5.1

(Extensional Abstract Domain). An abstract domain $\langle A,\gamma ,\le _\gamma \rangle$ is extensional when for any $a\in A$, $\gamma (a)\subseteq {{\mathrm{Prog}}}$ is an extensional program property, namely, if ${\llbracket P \rrbracket }={\llbracket Q \rrbracket }$ then $P\in \gamma (a) \Leftrightarrow Q\in \gamma (a)$.    $\square$

As usual, the intuition is that an extensional program property depends exclusively on the input/output program semantics ${\llbracket \cdot \rrbracket }$. As a simple example, the domains of Example 3.2 (3)-(4) are extensional while the domains of Example 3.2 (1)-(2)-(5) are not.

Definition 5.2

(Trivial Abstract Domain). An abstract domain $\langle A,\gamma ,\le _\gamma \rangle$ is trivial when A contains abstract bottom or top elements only, i.e., for any $a\in A$, $\gamma (a) \in \{ \varnothing , {{\mathrm{Prog}}}\}$.    $\square$

Definition 5.2 allows 4 possible types for a trivial abstract domain A: (1) $A=\varnothing$; (2) A is nonempty and consists of bottom elements only, i.e., $A\ne \varnothing$ and for all $a\in A$, $\gamma (a)=\varnothing$; (3) A is nonempty and consists of top elements only, i.e., $A\ne \varnothing$ and for all $a\in A$, $\gamma (a)={{\mathrm{Prog}}}$; (4) A satisfies (2) and (3), i.e., A contains both bottom and top elements.

Theorem 5.3

(Rice’s Theorem for Program Analysis). Let $\langle A,\gamma ,\le _\gamma \rangle$ be an extensional abstract domain and let ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ be a sound analyser. Then, ${{\mathrm{\mathcal {A}}}}$ is precise iff A is trivial.

Proof

Since we assume the existence of a sound analyser ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ on the extensional abstract domain A, observe that necessarily $A\ne \varnothing$.

Assume that A is trivial. We have to show that for any $a\in A$ and $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a \Leftrightarrow P\in \gamma (a)$. Assume that $P\in \gamma (a)$ for some $a\in A$. Then, we have that $\gamma (a)\ne \varnothing$, so that, since A is trivial, it must necessarily be that $\gamma (a)={{\mathrm{Prog}}}$. By soundness of ${{\mathrm{\mathcal {A}}}}$, $P\in \gamma ({{\mathrm{\mathcal {A}}}}(P))$, so that, since A is trivial, $\gamma ({{\mathrm{\mathcal {A}}}}(P))= {{\mathrm{Prog}}}$. Hence, we have that $\gamma ({{\mathrm{\mathcal {A}}}}(P))=\gamma (a)$, thus implying ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a$. On the other hand, if ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a$ then $\gamma ({{\mathrm{\mathcal {A}}}}(P))\subseteq \gamma (a)$, so that, since, by soundness of ${{\mathrm{\mathcal {A}}}}$, $P\in \gamma ({{\mathrm{\mathcal {A}}}}(P))$, we also have that $P\in \gamma (a)$.

Conversely, assume now that ${{\mathrm{\mathcal {A}}}}$ is precise, namely, $P\in \gamma (a)$ iff ${{\mathrm{\mathcal {A}}}}(P) \le _\gamma a$. Thus, since ${{\mathrm{\mathcal {A}}}}$ is a total recursive function and $\le _\gamma$ is decidable, we have that, for any $a\in A$, $P\in ^? \gamma (a)$ is decidable. Since $\gamma (a)$ is an extensional program property, by Rice’s Theorem, $\gamma (a)$ must necessarily be trivial, i.e., $\gamma (a) \in \{ \varnothing , {{\mathrm{Prog}}}\}$. This means that the abstract domain A is trivial.    $\square$

Rice’s Theorem for program analysis can be applied to several abstract domains. Due to lack of space, we just mention that the well-known undecidability of computing the meet over all paths (MOP) solution for a monotone dataflow analysis problem, proved by Kam and Ullman [15, Sect. 6] by resorting to undecidability of Post’s Correspondence Problem, can be derived as a simple consequence of Theorem 5.3.

Along the same lines of Theorem 5.3, Rice’s Theorem can be instantiated to program verification as follows.

Theorem 5.4

(Rice’s Theorem for Program Verification). Let $\langle A,\gamma ,\le _\gamma \rangle$ be an extensional abstract domain and let ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ be a sound, nontrivial and monotone verifier. Then, ${{\mathrm{\mathcal {V}}}}$ is precise iff A is trivial.

Proof

Let A be an extensional abstract domain and ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ be sound and nontrivial. If $A=\varnothing$ then A is trivial while the only possible verifier ${{\mathrm{\mathcal {V}}}}:{{\mathrm{Prog}}}\times \varnothing \rightarrow \{\mathbf {t},\mathbf ? \}$ is the empty verifier, which is vacuously precise but it is not nontrivial. Thus, $A\ne \varnothing$ holds.

Assume that ${{\mathrm{\mathcal {V}}}}$ is precise, that is, $P\in \gamma (a)$ iff ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$. Hence, since ${{\mathrm{\mathcal {V}}}}$ is a total recursive function, ${{\mathrm{\mathcal {V}}}}(P,a)=^?\mathbf {t}$ is decidable, so that $P\in ^?\gamma (a)$ is decidable as well. As in the proof of Theorem 5.3, since $\gamma (a)$ is an extensional program property, by Rice’s Theorem, $\gamma (a)\in \{ \varnothing , {{\mathrm{Prog}}}\}$. Thus, the abstract domain A is trivial.

Conversely, let $A\ne \varnothing$ be a trivial abstract domain. We have to prove that for any $a\in A$ and $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\Leftrightarrow P\in \gamma (a)$. Consider any $a\in A$. Since A is trivial, $\gamma (a)\in \{\varnothing ,{{\mathrm{Prog}}}\}$. If $\gamma (a)=\varnothing$ then, by soundness of ${{\mathrm{\mathcal {V}}}}$, for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf ?$, so that ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\Leftrightarrow P\in \gamma (a)$ holds. If, instead, $\gamma (a)={{\mathrm{Prog}}}$, i.e. a is an abstract top, then, since ${{\mathrm{\mathcal {V}}}}$ is assumed to be nontrivial and monotone, by Remark 4.4 (2), ${{\mathrm{\mathcal {V}}}}$ is able to prove the abstract top a for any program, namely, for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$, so that ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\Leftrightarrow P\in \gamma (a)$ holds.    $\square$

Let us remark a noteworthy difference of Theorem 5.4 w.r.t. Rice’s theorem for static analysis. Let us consider a trivial abstract domain $A\triangleq \{\top \}$ with $\gamma (\top )={{\mathrm{Prog}}}$. Here, the trivially sound analyser $\lambda P.\top$ is also precise, in accordance with Theorem 5.3. Instead, the trivially sound verifier ${{\mathrm{\mathcal {V}}}}_\mathbf{? } \triangleq \lambda (P,a).\mathbf ?$ is not precise, because $P\in \gamma (\top ) \Leftrightarrow {{\mathrm{\mathcal {V}}}}_\mathbf{? }(P,\top ) = \mathbf {t}$ does not hold. The point here is that ${{\mathrm{\mathcal {V}}}}_\mathbf{? }$ lacks the property of being nontrivial, and therefore Theorem 5.4 cannot be applied. On the other hand, ${{\mathrm{\mathcal {V}}}}_{\mathbf {t}}\triangleq \lambda (P,a).\mathbf {t}$ is nontrivial and precise, because, in this case, $P\in \gamma (\top ) \Leftrightarrow {{\mathrm{\mathcal {V}}}}_{\mathbf {t}}(P,\top ) = \mathbf {t}$ holds. Similarly, if we consider the trivial abstract domain $A'\triangleq \{\top ,\top '\}$, with $\gamma (\top ) = {{\mathrm{Prog}}}= \gamma (\top ')$, then the verifier

$${{\mathrm{\mathcal {V}}}}' (P,a)\triangleq {\left\{ \begin{array}{ll} \mathbf {t}&{} \text {if } a=\top \\ \mathbf ? &{}\text {if } a=\top ' \end{array}\right. } $$

is sound and nontrivial, but still ${{\mathrm{\mathcal {V}}}}'$ is not precise, because $P\in \gamma (\top ') \Leftrightarrow {{\mathrm{\mathcal {V}}}}'(P,\top ') = \mathbf {t}$ does not hold. The point here is that ${{\mathrm{\mathcal {V}}}}'$ is not monotone, because ${{\mathrm{\mathcal {V}}}}'(P,\top )=\mathbf {t}$ and $\top \le _\gamma \top '$ but ${{\mathrm{\mathcal {V}}}}'(P,\top ')\ne \mathbf {t}$, so that Theorem 5.4 cannot be applied.

6 Comparing Analysers and Verifiers

Let us now focus on a model for comparing the relative precision of program analysers and verifiers w.r.t. a common abstract domain $\langle A,\gamma ,\le _\gamma \rangle$.

Definition 6.1

(Comparison Relations). Let ${{\mathrm{\mathcal {V}}}},{{\mathrm{\mathcal {V}}}}' \in {{\mathrm{\mathbb {V}}}}_{\!A},$ ${{\mathrm{\mathcal {A}}}},{{\mathrm{\mathcal {A}}}}' \in {{\mathrm{\mathbb {A}}}}_A,$ and $\mathcal {X},\mathcal {Y}\in {{\mathrm{\mathbb {V}}}}_{\!A} \cup {{\mathrm{\mathbb {A}}}}_A$.

(1):

${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$ iff $\,\forall P\in {{\mathrm{Prog}}}.\forall a \in A.\; {{\mathrm{\mathcal {V}}}}'(P,a)=\mathbf {t}\,\Rightarrow \, {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$

(2):

${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$ iff $\,\forall P\in {{\mathrm{Prog}}}.\; {{\mathrm{\mathcal {A}}}}(P) \le _\gamma {{\mathrm{\mathcal {A}}}}'(P)$

(3):

${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$ iff $\,\forall P\in {{\mathrm{Prog}}}. \forall a \in A.\; {{\mathrm{\mathcal {A}}}}(P) \le _\gamma a \,\Rightarrow \, {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$

(4):

${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}$ iff $\,\forall P\in {{\mathrm{Prog}}}. \forall a \in A.\; {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\,\Rightarrow \, {{\mathrm{\mathcal {A}}}}(P) \le _\gamma a$

(5):

$\mathcal {X} \cong \mathcal {Y}$ when $\mathcal {X} \sqsubseteq \mathcal {Y}$ and $\mathcal {Y} \sqsubseteq \mathcal {X}$    $\square$

Let us comment on the previous definitions, which intuitively take into account the relative “verification powers” of verifiers and analysers. The relation ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$ holds when every assertion proved by ${{\mathrm{\mathcal {V}}}}'$ can be also proved by ${{\mathrm{\mathcal {V}}}}$, while ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$ means that the output assertion provided by ${{\mathrm{\mathcal {A}}}}$ is more precise than that produced by ${{\mathrm{\mathcal {A}}}}'$. Also, a verifier ${{\mathrm{\mathcal {V}}}}$ is more precise than an analyser ${{\mathrm{\mathcal {A}}}}$ when the verification power of ${{\mathrm{\mathcal {V}}}}$ is not less than the verification power of ${{\mathrm{\mathcal {A}}}}$, namely, any assertion a which can be proved by ${{\mathrm{\mathcal {A}}}}$ for a program P, i.e. ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a$ holds, can be also proved by ${{\mathrm{\mathcal {V}}}}$. Likewise, ${{\mathrm{\mathcal {A}}}}$ is more precise than ${{\mathrm{\mathcal {V}}}}$ when any assertion a proved by ${{\mathrm{\mathcal {V}}}}$ can be also proved by ${{\mathrm{\mathcal {A}}}}$, i.e., ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$ implies ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a$.

Let us observe that $\langle {{\mathrm{\mathbb {V}}}}_{\!A},\sqsubseteq \rangle$ turns out to be a poset, while $\langle {{\mathrm{\mathbb {A}}}}_A,\sqsubseteq \rangle$ is just a preordered set (cf. the lattice of abstract interpretations in [8]). We have that $\langle {{\mathrm{\mathbb {V}}}}_{\!A},\sqsubseteq \rangle$ has a greatest element ${{\mathrm{\mathcal {V}}}}_\mathbf{? }\triangleq \lambda (P,a).\mathbf ?$, which, in particular, is always sound although it is trivial. On the other hand, if A includes a top element $\top$ then ${{\mathrm{\mathcal {A}}}}_\top \triangleq \lambda P.\top$ is a sound analyser which is a maximal element in $\langle {{\mathrm{\mathbb {A}}}}_A,\sqsubseteq \rangle$. Also, ${{\mathrm{\mathcal {V}}}}\cong {{\mathrm{\mathcal {V}}}}'$ means that ${{\mathrm{\mathcal {V}}}}= {{\mathrm{\mathcal {V}}}}'$ as total functions, while ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {A}}}}'$ means that $\gamma \circ {{\mathrm{\mathcal {A}}}}= \gamma \circ {{\mathrm{\mathcal {A}}}}'$. Moreover, the comparison relation $\sqsubseteq$ is transitive even when considering analysers and verifiers together: if ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$ and ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$ then ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$, and if ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}$ and ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$ then ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$. Also, the relation $\sqsubseteq$ shifts soundness from verifiers to analysers, and from analysers to verifiers as follows (due to lack of space the proof is omitted).

Lemma 6.2

Let ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ and ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$. If ${{\mathrm{\mathcal {V}}}}$ is sound and ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$ then ${{\mathrm{\mathcal {A}}}}$ is sound; if ${{\mathrm{\mathcal {A}}}}$ is sound and ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}$ then ${{\mathrm{\mathcal {V}}}}$ is sound.

As expected, any sound analyser can be used to refine a given sound verifier (cf. [19, 20, 24, 25]) and this can be formalized and proved in our framework as follows.

Lemma 6.3

Given ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ and ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ which are both sound, let

$$\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})(P,a) \triangleq {\left\{ \begin{array}{ll} \mathbf {t}&{} \text { if } {{\mathrm{\mathcal {A}}}}(P)\le _\gamma a\\ {{\mathrm{\mathcal {V}}}}(P,a) &{} \text { if } {{\mathrm{\mathcal {A}}}}(P)\not \le _\gamma a \end{array}\right. } $$

Then, $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is sound, $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})\sqsubseteq {{\mathrm{\mathcal {V}}}}$ and $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})= {{\mathrm{\mathcal {V}}}}\,\Leftrightarrow \, {{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$.

Proof

$\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is sound because both ${{\mathrm{\mathcal {A}}}}$ and ${{\mathrm{\mathcal {V}}}}$ are sound. If ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$ then $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})(P,a)=\mathbf {t}$, i.e., $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})\sqsubseteq {{\mathrm{\mathcal {V}}}}$. Moreover, $\tau _{{{\mathrm{\mathcal {A}}}}}({{\mathrm{\mathcal {V}}}})= {{\mathrm{\mathcal {V}}}}$ iff ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a \Rightarrow {{\mathrm{\mathcal {V}}}}(P,a) =\mathbf {t}$ iff ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$.    $\square$

6.1 Optimal and Best Analysers and Verifiers

It makes sense to define optimality by restricting to sound analysers and verifiers only. Optimality is defined as minimality w.r.t. the precision relation $\sqsubseteq$, while being the best analyser/verifier means to be the most precise.

Definition 6.4

(Optimal and Best Analysers and Verifiers). A sound analyser ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ is optimal if for any sound ${{\mathrm{\mathcal {A}}}}'\in {{\mathrm{\mathbb {A}}}}_A$, ${{\mathrm{\mathcal {A}}}}'\sqsubseteq {{\mathrm{\mathcal {A}}}}\Rightarrow {{\mathrm{\mathcal {A}}}}' \cong {{\mathrm{\mathcal {A}}}}$, while ${{\mathrm{\mathcal {A}}}}$ is a best analyser if for any sound ${{\mathrm{\mathcal {A}}}}'\in {{\mathrm{\mathbb {A}}}}_A$, ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$.

A sound verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is optimal if for any ${{\mathrm{\mathcal {V}}}}'\in {{\mathrm{\mathbb {V}}}}_{\!A}$, ${{\mathrm{\mathcal {V}}}}'\sqsubseteq {{\mathrm{\mathcal {V}}}}\Rightarrow {{\mathrm{\mathcal {V}}}}'\cong {{\mathrm{\mathcal {V}}}}$, while ${{\mathrm{\mathcal {V}}}}$ is the best verifier if for any ${{\mathrm{\mathcal {V}}}}'\in {{\mathrm{\mathbb {V}}}}_{\!A}$, ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$.    $\square$

Let us first observe that if a best analyser or verifier exists then this is unique, while for analysers if ${{\mathrm{\mathcal {A}}}}_1$ and ${{\mathrm{\mathcal {A}}}}_2$ are two best analysers on A then ${{\mathrm{\mathcal {A}}}}_1\cong {{\mathrm{\mathcal {A}}}}_2$ holds. Of course, the possibility of defining an optimal/best analyser or verifier depends on the abstract domain A. For example, for a variable sign domain such as $\{\mathbb {Z}_{\le 0}, \mathbb {Z}_{\ge 0}, \mathbb {Z}\}$ just optimal analysers and verifiers could be defined, because for approximating the set $\{0\}$ two optimal sound abstract values are available rather than a best sound abstract value. Here, the expected but interesting property to remark is that the notion of precise (i.e., sound and complete) analyser turns out to coincide with the notion of being the best analyser.

Lemma 6.5

Let ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ be sound. Then, ${{\mathrm{\mathcal {A}}}}$ is precise iff ${{\mathrm{\mathcal {A}}}}$ is a best analyser.

Proof

$(\Rightarrow )$ Consider any sound ${{\mathrm{\mathcal {A}}}}'\in {{\mathrm{\mathbb {A}}}}_A$. Assume, by contradiction, that ${{\mathrm{\mathcal {A}}}}\not \sqsubseteq {{\mathrm{\mathcal {A}}}}'$, namely, there exists some $P\in {{\mathrm{Prog}}}$ such that $\gamma ({{\mathrm{\mathcal {A}}}}(P)) \not \subseteq \gamma ({{\mathrm{\mathcal {A}}}}'(P))$. By soundness of ${{\mathrm{\mathcal {A}}}}'$, ${\llbracket P \rrbracket }\in \gamma ({{\mathrm{\mathcal {A}}}}'(P))$, so that, by precision of ${{\mathrm{\mathcal {A}}}}$, $\gamma ({{\mathrm{\mathcal {A}}}}(P))\subseteq \gamma ({{\mathrm{\mathcal {A}}}}'(P))$, which is a contradiction. Thus, ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$ holds. This means that ${{\mathrm{\mathcal {A}}}}$ is a best analyser on A.

$(\Leftarrow )$ We have to prove that for any $P\in {{\mathrm{Prog}}}$ and $a\in A$, ${\llbracket P \rrbracket }\in \gamma (a) \Rightarrow \gamma ({{\mathrm{\mathcal {A}}}}(P)) \subseteq \gamma (a)$. Assume, by contradiction, that there exist $Q\in {{\mathrm{Prog}}}$ and $b\in A$ such that ${\llbracket Q \rrbracket }\in \gamma (b)$ and $\gamma ({{\mathrm{\mathcal {A}}}}(Q))\not \subseteq \gamma (b)$. Then, we define ${{\mathrm{\mathcal {A}}}}':{{\mathrm{Prog}}}\rightarrow A$ as follows:

$$ {{\mathrm{\mathcal {A}}}}'(P) \triangleq {\left\{ \begin{array}{ll} {{\mathrm{\mathcal {A}}}}(P) &{} \text {if } P\not \equiv Q\\ b &{} \text {if } P\equiv Q \end{array}\right. } $$

It turns out that ${{\mathrm{\mathcal {A}}}}'$ is a total recursive function because $P\equiv Q$ is decidable. Moreover, ${{\mathrm{\mathcal {A}}}}'$ is sound: assume that $\gamma ({{\mathrm{\mathcal {A}}}}'(P))\subseteq \gamma (a)$; if $P\not \equiv Q$ then ${{\mathrm{\mathcal {A}}}}'(P)={{\mathrm{\mathcal {A}}}}(P)$ so that $\gamma ({{\mathrm{\mathcal {A}}}}(P))\subseteq \gamma (a)$, and, by soundness of ${{\mathrm{\mathcal {A}}}}$, ${\llbracket P \rrbracket }\in \gamma (a)$; if $P\equiv Q$ then ${{\mathrm{\mathcal {A}}}}'(Q)=b$ so that $\gamma (b)=\gamma ({{\mathrm{\mathcal {A}}}}'(Q))=\gamma ({{\mathrm{\mathcal {A}}}}'(P))\subseteq \gamma (a)$, hence, ${\llbracket Q \rrbracket }\in \gamma (b)$ implies ${\llbracket Q \rrbracket }\in \gamma (a)$. Since ${{\mathrm{\mathcal {A}}}}$ is a best analyser on A, we have that ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$, so that $\gamma ({{\mathrm{\mathcal {A}}}}(Q))\subseteq \gamma ({{\mathrm{\mathcal {A}}}}'(Q))=\gamma (b)$, which is a contradiction.    $\square$

We therefore derive the following consequence of Rice’s Theorem 5.3 for static analysis: the best analyser on an extensional abstract domain A exists if and only if A is trivial. This fact formalizes in our model the common intuition that, given any abstract domain, the best static analyser (where best means for any input program) cannot be defined due to Rice’s Theorem. An analogous result can be given for verifiers.

Lemma 6.6

Let ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ be sound. Then ${{\mathrm{\mathcal {V}}}}$ is precise iff ${{\mathrm{\mathcal {V}}}}$ is the best verifier on A.

Proof

Assume that ${{\mathrm{\mathcal {V}}}}$ is precise and ${{\mathrm{\mathcal {V}}}}'\in {{\mathrm{\mathbb {V}}}}_{\!A}$ be sound. If ${{\mathrm{\mathcal {V}}}}'(P,a)=\mathbf {t}$ then, by soundness of ${{\mathrm{\mathcal {V}}}}'$, ${\llbracket P \rrbracket }\in \gamma (a)$, and in turn, by completeness of ${{\mathrm{\mathcal {V}}}}$, ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$, thus proving that ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$. On the other hand, assume that ${{\mathrm{\mathcal {V}}}}$ is the best verifier on A. Assume, by contradiction, that ${{\mathrm{\mathcal {V}}}}$ is not complete, namely that there exist some $Q\in {{\mathrm{Prog}}}$ and $b\in A$ such that ${\llbracket Q \rrbracket }\in \gamma (b)$ and ${{\mathrm{\mathcal {V}}}}(Q,b)=\mathbf ?$. We then define ${{\mathrm{\mathcal {V}}}}':{{\mathrm{Prog}}}\times A \rightarrow \{\mathbf {t},\mathbf ? \}$ as follows:

$$ {{\mathrm{\mathcal {V}}}}'(P,a) \triangleq {\left\{ \begin{array}{ll} \mathbf {t}&{} \text {if } P\equiv Q \;\wedge \; a=b\\ {{\mathrm{\mathcal {V}}}}(P,a) &{} \text {otherwise } \end{array}\right. } $$

Then, ${{\mathrm{\mathcal {V}}}}'$ is a total recursive function because $P\equiv Q$ and $a=b$ are decidable. Also, ${{\mathrm{\mathcal {V}}}}'$ is sound because ${\llbracket Q \rrbracket }\in \gamma (b)$ and ${{\mathrm{\mathcal {V}}}}$ is sound. Since ${{\mathrm{\mathcal {V}}}}$ is the best verifier, we have that ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$, so that ${{\mathrm{\mathcal {V}}}}'(Q,b)=\mathbf {t}$ implies ${{\mathrm{\mathcal {V}}}}(Q,b)=\mathbf {t}$, which is a contradiction.    $\square$

Thus, similarly to static analysis, as a consequence of Rice’s Theorem 5.4 for verification, the best nontrivial and monotone verifier on an extensional abstract domain A exists if and only if A is trivial, which is a common belief in program verification. Let us also remark that best abstract program semantics, rather than program analysers, do exist for nontrivial domains (see e.g. [6]). Clearly, this is not in contradiction with Theorem 5.3 since these abstract program semantics are not total recursive functions, i.e., they are not program analysers.

7 Reducing Verification to Analysis and Back

As usual in computability and complexity, our comparison between verification and analysis is made through a many-one reduction, namely by reducing a verification problem into an analysis problem and vice versa. The minimal requirement is that these reduction functions are total recursive. Moreover, we require that the reduction function does not depend upon a fixed abstract domain. This allows us to be problem agnostic and to prove a reduction for all possible verifiers and analysers. Program verification and analysis are therefore equivalent problems whenever we can reduce one to the other. In the following, we prove that while it is always possible to transform a program analyser into an equivalent program verifier, the converse does not hold in general, but it can always be done for finite abstract domains.

7.1 Reducing Verification to Analysis

Theorem 7.1

Let $\langle A,\gamma ,\le _\gamma \rangle$ be any given abstract domain. There exists a transform $\sigma : {{\mathrm{\mathbb {A}}}}_A \rightarrow {{\mathrm{\mathbb {V}}}}_{\!A}$ such that:

(1):

$\sigma$ is a total recursive function such that for all ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$, $\sigma ({{\mathrm{\mathcal {A}}}}) \cong {{\mathrm{\mathcal {A}}}}$;

(2):

if ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ is sound then $\sigma ({{\mathrm{\mathcal {A}}}})$ is sound;

(3):

$\sigma$ is monotonic;

(4):

$\sigma ({{\mathrm{\mathcal {A}}}}) \cong \sigma ({{\mathrm{\mathcal {A}}}}') \Rightarrow {{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {A}}}}'$.

Proof

Given ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$, we define $\sigma ({{\mathrm{\mathcal {A}}}}): {{\mathrm{Prog}}}\times A \rightarrow \{\mathbf {t},\mathbf ? \}$ as follows:

$$ \sigma ({{\mathrm{\mathcal {A}}}})(P,a) \triangleq {\left\{ \begin{array}{ll} \mathbf {t}&{} \text {if } {{\mathrm{\mathcal {A}}}}(P) \le _{\gamma } a\\ \mathbf ? &{} \text {if } {{\mathrm{\mathcal {A}}}}(P) \not \le _{\gamma } a \end{array}\right. } $$

(1) Since ${{\mathrm{\mathcal {A}}}}$ is a total recursive function and $\le _{\gamma }$ is decidable, we have that $\sigma ({{\mathrm{\mathcal {A}}}})$ is a total recursive function, namely $\sigma ({{\mathrm{\mathcal {A}}}})\in {{\mathrm{\mathbb {V}}}}_{\!A}$, and $\sigma$ is a total recursive function as well. Since, by definition, $\sigma ({{\mathrm{\mathcal {A}}}})(P,a) = \mathbf {t}\Leftrightarrow {{\mathrm{\mathcal {A}}}}(P) \le _{\gamma } a$, we have that $\sigma ({{\mathrm{\mathcal {A}}}}) \cong {{\mathrm{\mathcal {A}}}}$. (2) By Lemma 6.2, if ${{\mathrm{\mathcal {A}}}}$ is sound then the equivalent verifier $\sigma ({{\mathrm{\mathcal {A}}}})$ is sound as well. (3) It turns out that $\sigma$ is monotonic: if ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}'$ then $\sigma ({{\mathrm{\mathcal {A}}}}')(P,a)=\mathbf {t}$ $\Leftrightarrow$ ${{\mathrm{\mathcal {A}}}}'(P)\le _{\gamma } a$ $\Rightarrow$ ${{\mathrm{\mathcal {A}}}}(P)\le _{\gamma } {{\mathrm{\mathcal {A}}}}'(P)\le _{\gamma } a$ $\Leftrightarrow$ $\sigma ({{\mathrm{\mathcal {A}}}})(P,a)=\mathbf {t}$, so that $\sigma ({{\mathrm{\mathcal {A}}}}) \sqsubseteq \sigma ({{\mathrm{\mathcal {A}}}}')$ holds. (4) Assume that $\sigma ({{\mathrm{\mathcal {A}}}}) \cong \sigma ({{\mathrm{\mathcal {A}}}}')$, hence, for any $P\in {{\mathrm{Prog}}}$, $\sigma ({{\mathrm{\mathcal {A}}}})(P,{{\mathrm{\mathcal {A}}}}(P)) = \sigma ({{\mathrm{\mathcal {A}}}}')(P,{{\mathrm{\mathcal {A}}}}(P))$, namely, ${{\mathrm{\mathcal {A}}}}(P)\le _{\gamma } {{\mathrm{\mathcal {A}}}}(P) \,\Leftrightarrow \, {{\mathrm{\mathcal {A}}}}'(P) \le _{\gamma } {{\mathrm{\mathcal {A}}}}(P)$, so that ${{\mathrm{\mathcal {A}}}}'(P) \le _{\gamma } {{\mathrm{\mathcal {A}}}}(P)$ holds. On the other hand, ${{\mathrm{\mathcal {A}}}}(P) \le _{\gamma } {{\mathrm{\mathcal {A}}}}'(P)$ can be dually obtained, therefore $\gamma ({{\mathrm{\mathcal {A}}}}(P))=\gamma ({{\mathrm{\mathcal {A}}}}'(P))$ holds, namely ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {A}}}}'$.    $\square$

Intuitively, Theorem 7.1 shows that program verification on a given abstract domain A can always and unconditionally be reduced to program analysis on A. This means that a solution to the program analysis problem on A, i.e. the definition of an analyser ${{\mathrm{\mathcal {A}}}}$, can constructively be transformed into a solution to the program verification problem on the same domain A, i.e. the design of a verifier $\sigma ({{\mathrm{\mathcal {A}}}})$ which is equivalent to ${{\mathrm{\mathcal {A}}}}$. The proof of Theorem 7.1 provides this constructive transform $\sigma$, which is defined as expected: an analyser ${{\mathrm{\mathcal {A}}}}$ on any (possibly infinite) abstract domain A can be used as a verifier for any assertion $a\in A$ simply by checking whether ${{\mathrm{\mathcal {A}}}}(P)\le _\gamma a$ holds or not.

7.2 Reducing Analysis to Verification

It turns out that the converse of Theorem 7.1 does not hold, namely a program analysis problem in general cannot be reduced to a verification problem. Instead, this reduction can be always done for finite abstract domains. Given a verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$, for any program $P\in {{\mathrm{Prog}}}$, let us define ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) \triangleq \{a\in A~|~ {{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\}$, namely, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$ is the set of assertions proved by ${{\mathrm{\mathcal {V}}}}$ for P. Also, given an assertion $a\in A$, we define $\uparrow \!\!\!\,a \triangleq \{a'\in A~|~ a\le _\gamma a'\}$ as the set of assertions weaker than a. The following result provides a useful characterization of the equivalence between verifiers and analysers.

Lemma 7.2

Let $\langle A,\gamma ,\le _\gamma \rangle$ be an abstract domain, ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ and ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$. Then, ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {V}}}}$ if and only if for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) =\, \uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(P)$.

Proof

By Definition 6.1, it turns out that ${{\mathrm{\mathcal {A}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}$ iff for any P, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) \subseteq \;\uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(P)$, while we have that ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$ iff for any P, $\uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(P) \subseteq {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$. Thus, ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {V}}}}$ if and only if for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) =\; \uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(P)$.    $\square$

A consequence of Lemma 7.2 is that, given ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$, ${{\mathrm{\mathcal {V}}}}$ can be transformed into an equivalent analyser $\tau ({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {A}}}}_A$ if and only if for any program P, an assertion $a_P\in A$ exists such that ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) =\; \uparrow \!\!\!\,a_P$. In this case, one can then define $\tau ({{\mathrm{\mathcal {V}}}})(P) \triangleq a_P$.

Lemma 7.3

Let $\langle A,\gamma ,\le _\gamma \rangle$ be an abstract domain and ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$. If ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ is such that ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {V}}}}$ then: (1) $A\ne \varnothing$; (2) ${{\mathrm{\mathcal {V}}}}$ is not trivial; (3) ${{\mathrm{\mathcal {V}}}}$ is monotone.

Proof

(1) We observed just after Definition 4.1 that no analyser can be defined on the empty abstract domain. (2) If ${{\mathrm{\mathcal {V}}}}$ is trivial then there exists a program $Q\in {{\mathrm{Prog}}}$ such that for any $a\in A$, ${{\mathrm{\mathcal {V}}}}(Q,a)=\mathbf ?$, so that if ${{\mathrm{\mathcal {V}}}}\cong {{\mathrm{\mathcal {A}}}}$ for some ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$ then, from ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {A}}}}$ we would derive ${{\mathrm{\mathcal {V}}}}(Q,{{\mathrm{\mathcal {A}}}}(Q))=\mathbf {t}$, which is a contradiction. (3) Assume that ${{\mathrm{\mathcal {V}}}}$ is not monotone. Then, there exist $Q\in {{\mathrm{Prog}}}$ and $a,a'\in A$ such that $a\in {{\mathrm{\mathcal {V}}}}_\mathbf {t}(Q)$, $a\le _\gamma a'$ but $a'\not \in {{\mathrm{\mathcal {V}}}}_\mathbf {t}(Q)$. If ${{\mathrm{\mathcal {V}}}}\cong \mathcal {A}$, for some ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$, then, by Lemma 7.2, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(Q)=\,\uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(Q)$, so that we would have that $a\in \,\uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(Q)$ but $a'\not \in \, \uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(Q)$, which is a contradiction.    $\square$

We also observe that even for a nontrivial and monotone verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ on a finite abstract domain A, it is not guaranteed that an equivalent analyser exists. In fact, if an equivalent analyser ${{\mathrm{\mathcal {A}}}}$ exists then, by Lemma 7.2, for any program P, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$ must contain the least element, namely for any program P it must be the case that there exists a strongest assertion proved by ${{\mathrm{\mathcal {V}}}}$ for P.

Example 7.4

Consider a sign domain such as $S\triangleq \{\mathbb {Z}_{\le 0}, \mathbb {Z}_{\ge 0}, \mathbb {Z}\}$ where $\mathbb {Z}_{\le 0} \le _\gamma \mathbb {Z}$ and $\mathbb {Z}_{\ge 0} \le _\gamma \mathbb {Z}$. For a program such as $Q \equiv x:=0$, a sound verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_S$ could be able to prove all the assertions in S, namely ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(Q)=S$. However, there exists no assertion $a_Q\in S$ such that ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(Q) =\; \uparrow \!\!\!\,a_Q$. Hence, by Lemma 7.2, there exists no analyser in ${{\mathrm{\mathbb {A}}}}_S$ which is equivalent to ${{\mathrm{\mathcal {V}}}}$. Also, if $S' \triangleq \{\mathbb {Z}_{=0}, \mathbb {Z}_{\le 0}, \mathbb {Z}_{\ge 0}, \mathbb {Z}\}$, so that $S'$ is a meet-semilattice, and ${{\mathrm{\mathcal {V}}}}'\in {{\mathrm{\mathbb {V}}}}_{S'}$ is a sound verifier such that ${{\mathrm{\mathcal {V}}}}'_\mathbf {t}(Q)=S'\smallsetminus \{\mathbb {Z}_{=0} \}$, still, by Lemma 7.2, there exists no analyser in ${{\mathrm{\mathbb {A}}}}_{S'}$ which is equivalent to ${{\mathrm{\mathcal {V}}}}'$.    $\square$

Definition 7.5

A verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}$ is finitely meet-closed when for any $P\in {{\mathrm{Prog}}}$ and $a, a_1,a_2\in A$, if ${{\mathrm{\mathcal {V}}}}(P,a_1)=\mathbf {t}={{\mathrm{\mathcal {V}}}}(P,a_2)$ and $\gamma (a)=\gamma (a_1)\cap \gamma (a_2)$ then ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$. The following notation will be used: for any domain A,

$$ {{\mathrm{\mathbb {V}}}}_{\!A}^+ \triangleq \{{{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A} ~|~ {{\mathrm{\mathcal {V}}}}\text { is nontrivial, monotone and finitely meet-closed}\}. $$

   $\square$

Thus, finitely meet-closed verifiers can prove logical conjunctions of provable assertions.

Theorem 7.6

(Reduction for Finite Domains). Let $\langle A,\gamma ,\le _\gamma \rangle$ be a nonempty finite abstract domain. There exists a transform $\tau : {{\mathrm{\mathbb {V}}}}^+_A \rightarrow {{\mathrm{\mathbb {A}}}}_A$ such that:

(1):

$\tau$ is a total recursive function such that for all ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$, $\tau ({{\mathrm{\mathcal {V}}}}) \cong {{\mathrm{\mathcal {V}}}}$;

(2):

if ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$ is sound then $\tau ({{\mathrm{\mathcal {V}}}})$ is sound;

(3):

$\tau$ is monotonic;

(4):

$\tau ({{\mathrm{\mathcal {V}}}}) \cong \tau ({{\mathrm{\mathcal {V}}}}') \Rightarrow {{\mathrm{\mathcal {V}}}}\cong {{\mathrm{\mathcal {V}}}}'$.

Proof

(1) Let $A=\{a_1,...,a_n\}$ be any enumeration of A, with $n\ge 1$. Given ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}^+$, we define $\tau ({{\mathrm{\mathcal {V}}}}): {{\mathrm{Prog}}}\rightarrow A$ as follows:

$$ \tau ({{\mathrm{\mathcal {V}}}})(P) \triangleq {\left\{ \begin{array}{ll} r:= \text {undef};\\ \mathbf{forall }\,\, i\in 1..n \,\,\mathbf{do }\\ \qquad \mathbf{if }\,\, \big (a_i \in {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) \,\wedge \, (r= \text {undef} \;\vee \; a_i\le _\gamma r)\big ) \,\,\mathbf{then }\,\, r:=a_i ;\\ \mathbf{output }\,\, r \end{array}\right. } $$

Then, it turns out that $\tau$ is a total recursive function. Since ${{\mathrm{\mathcal {V}}}}$ is a total recursive function, A is finite and $\le _\gamma$ is decidable, we have that $\tau ({{\mathrm{\mathcal {V}}}})$ is a total recursive function, so that $\tau ({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {A}}}}_A$. Since ${{\mathrm{\mathcal {V}}}}$ is not trivial, for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)\ne \varnothing$. Also, since A is finite and ${{\mathrm{\mathcal {V}}}}$ is finitely meet-closed there exists some $a_k\in {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$ such that ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)\subseteq \; \uparrow \!\!\!\,a_k$, so that $\tau ({{\mathrm{\mathcal {V}}}})(P)$ outputs some value in A. Moreover, since ${{\mathrm{\mathcal {V}}}}$ is monotone, $\uparrow \!\!\!\,a_k\subseteq {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$, so that $\uparrow \!\!\!\,a_k = {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$. Thus, the above procedure defining $\tau ({{\mathrm{\mathcal {V}}}})(P)$ finds and outputs $a_k$. Hence, for any $P\in {{\mathrm{Prog}}}$ and $a\in A$, ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}\Leftrightarrow a\in {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) \Leftrightarrow a\in \,\uparrow \!\!\!\,a_k \Leftrightarrow a_k \le _\gamma a \Leftrightarrow \tau ({{\mathrm{\mathcal {V}}}})(P) \le _\gamma a$, that is, $\tau ({{\mathrm{\mathcal {V}}}}) \cong {{\mathrm{\mathcal {V}}}}$ holds.

(2) By Lemma 6.2, if ${{\mathrm{\mathcal {V}}}}$ is sound then the equivalent analyser $\tau ({{\mathrm{\mathcal {V}}}})$ is sound as well.

(3) It turns out that $\tau$ is monotonic: if ${{\mathrm{\mathcal {V}}}}\sqsubseteq {{\mathrm{\mathcal {V}}}}'$ then, by definition, ${{\mathrm{\mathcal {V}}}}'_\mathbf {t}(P) \subseteq {{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)$, so that, since ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) = \,\uparrow \!\!\!\,\tau ({{\mathrm{\mathcal {V}}}})(P)$ and ${{\mathrm{\mathcal {V}}}}'_\mathbf {t}(P) = \,\uparrow \!\!\!\,\tau ({{\mathrm{\mathcal {V}}}}')(P)$, we obtain $\tau ({{\mathrm{\mathcal {V}}}})(P)\le _\gamma \tau ({{\mathrm{\mathcal {V}}}}')(P)$, namely $\tau ({{\mathrm{\mathcal {V}}}}) \sqsubseteq \tau ({{\mathrm{\mathcal {V}}}}')$ holds.

(4) Assume that $\tau ({{\mathrm{\mathcal {V}}}}) \cong \tau ({{\mathrm{\mathcal {V}}}}')$. Hence, for any $P\in {{\mathrm{Prog}}}$, $\gamma (\tau ({{\mathrm{\mathcal {V}}}})(P)) = \gamma (\tau ({{\mathrm{\mathcal {V}}}}')(P))$, so that, since ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) = \;\uparrow \!\!\!\,\tau ({{\mathrm{\mathcal {V}}}})(P)$ and ${{\mathrm{\mathcal {V}}}}'_\mathbf {t}(P) = \;\uparrow \!\!\!\,\tau ({{\mathrm{\mathcal {V}}}}')(P)$, we obtain ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)={{\mathrm{\mathcal {V}}}}'_\mathbf {t}(P)$, namely ${{\mathrm{\mathcal {V}}}}= {{\mathrm{\mathcal {V}}}}'$.    $\square$

An example of this reduction of verification to static analysis for finite domains is dataflow analysis as model checking shown in [31] (excluding Kildall’s constant propagation domain [16]). Let us now focus on infinite domains of assertions.

Lemma 7.7

There exists a denumerable infinite abstract domain $\langle A,\gamma ,\le _\gamma \rangle$ and a verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$ such that for any analyser ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_A$, ${{\mathrm{\mathcal {A}}}}\not \cong {{\mathrm{\mathcal {V}}}}$.

Proof

Let us consider the infinite domain ${{\mathrm{T}}}\triangleq \mathbb {N}\cup \{\top \}$ together with the following concretization function: $\gamma (\top ) \triangleq {{\mathrm{Prog}}}$ and, for any $n\in \mathbb {N}$,

$$ \gamma (n) \triangleq \{P\in {{\mathrm{Prog}}}~|~ P \text { on input } 0 \text { converges in } n \text { or fewer steps}\} $$

where the number of steps is determined by a small-step operational semantics $\Rightarrow$, as recalled in Sect. 2. Thus, we have that if $n,m\in \mathbb {N}$ then $n \le _\gamma m$ iff $n\le _\mathbb {N}m$, while $n\le _\gamma \top$. We define a function ${{\mathrm{\mathcal {V}}}}:{{\mathrm{Prog}}}\times {{\mathrm{T}}}\rightarrow \{\mathbf {t},\mathbf ? \}$ as follows:

$$ {{\mathrm{\mathcal {V}}}}(P,a) \triangleq {\left\{ \begin{array}{ll} \mathbf {t}&{} \text {if }a=\top \\ \mathbf {t}&{} \text {if } a=n \text { and } P \text { on input } 0 \text { converges in } n \text { or fewer steps}\\ \mathbf ? &{} \text {if } a=n \text { and } P \text { on input } 0 \text { does not converge in } n \text { or fewer steps}\\ \end{array}\right. } $$

Clearly, for any number $n\in \mathbb {N}$, the predicate “P on input 0 converges in n or fewer steps” is decidable, where the input 0 could be replaced by any other (finite set of) input value(s). Hence, ${{\mathrm{\mathcal {V}}}}$ turns out to be a total recursive function, that is, a verifier on the abstract domain ${{\mathrm{T}}}$. In particular, let us remark that ${{\mathrm{\mathcal {V}}}}$ is a sound verifier. Moreover, ${{\mathrm{\mathcal {V}}}}$ is nontrivial, since, for any $P\in {{\mathrm{Prog}}}$, ${{\mathrm{\mathcal {V}}}}(P,\top )=\mathbf {t}$, and monotone because if ${{\mathrm{\mathcal {V}}}}(P,n)=\mathbf {t}$ and $n\le _\gamma a$ then either $a=\top$ and ${{\mathrm{\mathcal {V}}}}(P,\top )=\mathbf {t}$ or $a=m$, so that $n\le _\mathbb {N}m$ and therefore ${{\mathrm{\mathcal {V}}}}(P,m)=\mathbf {t}$. Clearly, ${{\mathrm{\mathcal {V}}}}$ is also finitely meet-closed, because if ${{\mathrm{\mathcal {V}}}}(P,a_1)=\mathbf {t}={{\mathrm{\mathcal {V}}}}(P,a_2)$ and $\gamma (a)=\gamma (a_1)\cap \gamma (a_2)$ then either $a=a_1$ or $a=a_2$, so that ${{\mathrm{\mathcal {V}}}}(P,a)=\mathbf {t}$. Summing up, it turns out that ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_{{{\mathrm{T}}}}$. Assume now, by contradiction, that there exists an analyser ${{\mathrm{\mathcal {A}}}}\in {{\mathrm{\mathbb {A}}}}_{{{\mathrm{T}}}}$ such that ${{\mathrm{\mathcal {A}}}}\cong {{\mathrm{\mathcal {V}}}}$. By Lemma 7.2, for any $P\in {{\mathrm{Prog}}}$, we have that ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P) = \;\uparrow \!\!\!\,{{\mathrm{\mathcal {A}}}}(P)$. Hence, if P on input 0 diverges then ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)=\{\top \}$ so that ${{\mathrm{\mathcal {A}}}}(P)=\top$, while if P on input 0 converges in exactly n steps then ${{\mathrm{\mathcal {V}}}}_\mathbf {t}(P)=\{m\in \mathbb {N}~|~ m\ge n\}\cup \{\top \}$, so ${{\mathrm{\mathcal {A}}}}(P)=n$, namely ${{\mathrm{\mathcal {A}}}}$ goes as follows:

$$ {{\mathrm{\mathcal {A}}}}(P)= {\left\{ \begin{array}{ll} \top &{} \text {if } P \text { on input } 0 \text { diverges}\\ n &{} \text {if } P \text { on input } 0 \text { converges in exactly } n \text { steps} \end{array}\right. } $$

Since ${{\mathrm{\mathcal {A}}}}$ is a total recursive function, we would have defined an algorithm ${{\mathrm{\mathcal {A}}}}$ for deciding if a program $P\in {{\mathrm{Prog}}}$ on input 0 terminates or not. Since ${{\mathrm{Prog}}}$ is assumed to be Turing complete with respect to the operational semantics $\Rightarrow$, this leads to a contradiction.    $\square$

As a straight consequence of Lemma 7.7, the following theorem proves that for any infinite abstract domain A, no reduction from verifiers in ${{\mathrm{\mathbb {V}}}}^+_A$ to equivalent analysers in ${{\mathrm{\mathbb {A}}}}_A$ is possible.

Theorem 7.8

(Impossibility of the Reduction for Infinite Domains). For any denumerable infinite abstract domain $\langle A,\gamma ,\le _\gamma \rangle$, there exists no function $\tau : {{\mathrm{\mathbb {V}}}}^+_A \rightarrow {{\mathrm{\mathbb {A}}}}_A$ such that $\tau$ is a total recursive function and for all ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$, $\tau ({{\mathrm{\mathcal {V}}}}) \cong {{\mathrm{\mathcal {V}}}}$.

Proof

Assume, by contradiction, that $\tau : {{\mathrm{\mathbb {V}}}}^+_A \rightarrow {{\mathrm{\mathbb {A}}}}_A$ is a total recursive function such that for all ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$, $\tau ({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {A}}}}_A$ and $\tau ({{\mathrm{\mathcal {V}}}}) \cong {{\mathrm{\mathcal {V}}}}$. Then, for the infinite domain A and verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}^+_A$ provided by Lemma 7.7, we would be able to construct an analyser $\tau ({{\mathrm{\mathcal {V}}}})\in {{\mathrm{\mathbb {A}}}}_A$ such that $\tau ({{\mathrm{\mathcal {V}}}})\cong {{\mathrm{\mathcal {V}}}}$, which would be in contradiction with Lemma 7.7.    $\square$

Intuitively, this result states that given any infinite abstract domain A, no general algorithm exists for constructively designing out of a reasonable (i.e., nontrivial, monotone and finitely meet-closed) verifier ${{\mathrm{\mathcal {V}}}}$ on A an equivalent analyser on the same domain A. This can be read as a precise statement proving the folklore belief that “program analysis is harder than verification”, at least for infinite domains of program assertions. It is important to remark that the verifier ${{\mathrm{\mathcal {V}}}}\in {{\mathrm{\mathbb {V}}}}_{\!A}^+$ on the infinite domain A defined by the proof of Lemma 7.7 is sound. Thus, even if we restrict the reduction transform $\tau :{{\mathrm{\mathbb {V}}}}^{+,\text {sound}}_A \rightarrow {{\mathrm{\mathbb {A}}}}^{\text {sound}}_A$ of Theorem 7.8 to be applied to sound verifiers—so that by Lemma 6.2 the range would be the sound analysers in ${{\mathrm{\mathbb {A}}}}_A$—the same proof of Lemma 7.7 could still be used for proving that such transform $\tau$ cannot exist.

A further consequence of Theorem 7.8 is the fact proved in [10] that abstract interpretation-based program analysis with infinite domains and widening/narrowing operators is strictly more powerful than with finite domains.

8 Conclusion and Future Work

We put forward a general model for studying static program analysers and verifiers from a computability perspective. This allowed us to state and prove, with simple arguments borrowed from standard computability theory, that for infinite abstract domains of program assertions, program analysis is a harder problem than program verification. This is, to the best of our knowledge, the first formalization and proof of this popular belief, which also includes the relationship between type inference and type checking. We think that this foundational model can be extended to study further properties of program analysers and verifiers. In particular, this opens interesting perspectives in reasoning about program analysis and verification in a more abstract way towards a theory of computation that may include approximate methods, such as program analysers and verifiers, as objects of investigation, as suggested in [5, 14]. For instance, the precision of program analysis and program verification, as well as their computational complexity, are intensional program properties. Intensionally different but extensionally equivalent programs may exhibit completely different behaviours when analysed or verified. In this perspective, new intensional versions of Rice’s Theorem can be stated for program analysis, similarly to what is known for Blum’s complexity in [2]. Also, new models for reasoning about the space and time complexities of program analysis and verification algorithms can be studied, especially for defining a notion of complexity class of program analysers and verifiers.