Statements. The first few statements in $P_{M}$ correspond to initialization:
$x_{\text{curr}}$ is initialized to $x_{q_{0}}$ and both $y_{1}$ and $y_{2}$
get initialized to $z$. Further we demand that all constants are different
from each other: for every $q\neq q^{\prime}$ we demand that $x_{q}$ and
$x_{q^{\prime}}$ are unequal, and that $z$ is different from any $x_{q}$.

INIT: $\displaystyle\textbf{assume}\,(x_{q}\neq x_{q^{\prime}})$
$\displaystyle\quad\quad\texttt{(** for every }q\neq q^{\prime}\texttt{**)}$
$\displaystyle\textbf{assume}\,(x_{q}\neq z)$
$\displaystyle\quad\quad\texttt{(** for every }q\texttt{**)}$
$\displaystyle\textbf{assume}\,(x_{\text{curr}}:=x_{s})$
$\displaystyle\textbf{assume}\,(y_{1}:=z)$
$\displaystyle\textbf{assume}\,(y_{2}:=z)$

The initialization block is followed by a while loop with the condition
$(x_{\text{curr}}\neq x_{\mathsf{HALT}})$. The body of the loop contains, one
block (labelled $\texttt{BLOCK}_{q}$) for every for every
$q\to(instr,C_{i},q^{\prime})\in\delta$. The statements inside
$\texttt{BLOCK}_{q}$ depend upon what $instr$ is:

  1. (1)

Case $instr$ is $\mathsf{INC}$ or $\mathsf{DEC}$:
In this case the code block is

$\displaystyle\texttt{BLOCK}_{q}:$
$\displaystyle\textbf{if}\,(x_{\text{curr}}=x_{q})\\{$ $\displaystyle\quad
w_{1}:=f(y_{i})$ $\displaystyle\quad w_{2}:=g(y_{i})$ $\displaystyle\quad
w_{3}:=g(w_{1})$ $\displaystyle\quad w_{4}:=f(w_{2})$
$\displaystyle\quad\textbf{assume}\,(w_{3}=y_{i})$
$\displaystyle\quad\textbf{assume}\,(w_{4}=y_{i})$ $\displaystyle\quad\langle
stmt\rangle$ $\displaystyle\quad x_{\text{curr}}:=x_{q^{\prime}}$
$\displaystyle\\}$

where $\langle stmt\rangle$ is $y_{i}:=f(y_{i})$ if $instr$ is $\mathsf{INC}$
and $y_{i}:=g(y_{i})$ if $instr$ is $\mathsf{DEC}$.

  2. (2)

Case $instr$ is $\mathsf{CHECK}$:
In this case the code block is

$\displaystyle\texttt{BLOCK}_{q}:$
$\displaystyle\textbf{if}\,(x_{\text{curr}}=x_{q})\\{$
$\displaystyle\quad\textbf{assume}\,(y_{i}=z)$ $\displaystyle\\}$

Finally the specification is
$\phi_{M}\mathrel{\ensurestackMath{\stackon[1pt]{=}{\scriptstyle\Delta}}}(x_{\text{curr}}\neq
x_{\mathsf{HALT}})$

The correctness of the reduction is captured by the following lemma

###### Lemma 1.

$M$ does not reach $\mathsf{HALT}$ iff $P_{M}\models\phi_{M}$.

###### Proof.

Before we begin the actual proof, we note that every complete execution of
$P_{M}$ ends in
$\text{``}\textbf{assume}(x_{\text{curr}}=x_{\mathsf{HALT}})\text{''}$.

Let us first prove the forward direction: If $M$ does not reach
$\mathsf{HALT}$, then $P_{M}\models\phi_{M}$. Let’s say $M$ does not reach
$\mathsf{HALT}$. In this case, we show that no complete execution of $P_{M}$
is feasible (and thus $P_{M}\models\phi_{M}$). Assume, on the contrary, that
there is a complete execution $\sigma$ which is also feasible. As we noted
before, $\sigma$ ends in
$\text{``}\textbf{assume}(x_{\text{curr}}=x_{\mathsf{HALT}})\text{''}$. We
first observe that $\sigma$ is feasible in $\mathcal{M}_{\mathbb{N}}$ where
the universe is the set of natural numbers, $z$ is interpreted as $0$ and $f$
and $g$ are respectively $\lambda i.i+1$ and $\lambda i.i-1$. Now, let
$\texttt{INIT},\texttt{BLOCK}_{q_{i_{1}}}\ldots\texttt{BLOCK}_{q_{i_{k}}}$ be
the sequence of blocks taken in $\sigma$. Since $\sigma$ is feasible, it must
be that in the last block $\texttt{BLOCK}_{q_{i_{k}}}$, $x_{\text{curr}}$ must
be assigned to $x_{\mathsf{HALT}}$. Now, consider the corresponding run
$\rho=s\to q_{i_{1}}\cdots q_{i_{k}}\to\mathsf{HALT}$. It easily follows that
$\rho$ is a valid run of $M$, contradicting our initial assumption that $M$
does not reach $\mathsf{HALT}$.

Let us now prove the other direction (in a contrapositive manner): If $M$
reaches $\mathsf{HALT}$, then $P_{M}\not\models\phi_{M}$. Consider the run
$\rho$ of $M$ that reaches $\mathsf{HALT}$. Then, $\rho=q_{i_{0}}\to
q_{i_{1}}\cdots q_{i_{k}}\to\mathsf{HALT}$, where $q_{i_{0}}=s$. We now
construct a _feasible_ complete execution $\sigma$ of $P_{M}$, which, as we
noted before, ends in
$\text{``}\textbf{assume}(x_{\text{curr}}=x_{\mathsf{HALT}})\text{''}$ (and
thus $P_{M}\not\models\phi_{M}$). The execution $\sigma$ will essentially
mimic the run $\rho$ of $M$, and is the sequence of statements generated by
the sequence of blocks
$\texttt{INIT},\texttt{BLOCK}_{q_{i_{1}}}\ldots\texttt{BLOCK}_{q_{i_{k}}}$.
Since $\rho$ is a run of $M$, it follows that $\sigma$ is feasible in the FO
model $\mathcal{M}_{\mathbb{N}}$, where the universe is the set of natural
numbers, the constant $z$ is interpreted as $0$, $f$ is interpreted to be the
function $\lambda i.i+1$ and $g$ is the function $\lambda i.i-1$. ∎

###  B.1. Undecidability when programs executions have early-assumes but are
not memoizing

We now give the main modifications of the above proof to adapt it to a proof
of Theorem 2.

We will continue to have an input variable that stands for the counter value
$0$, and $f$ and $g$ defined over it with $f^{i}(0)$ denoting the counter
value $i$. Again, we would like to assert that for each of the terms
$f^{i}(0)$, $g(f(f^{i}(0)))=f^{i}(0)$. The assumes that we executed in the
previous proof are not, however, early assumes.

In order to ensure the above property of the model, we introduce a “fake”
counter variable $c^{*}$. The program always ensures, in every round of
simulating the 2-CM one step, that $c^{*}$ always advances (i.e., we update
$c^{*}$ to $f(c^{*})$), and we assure that $c^{*}=g(f(c^{*}))$ using an
assume. We remove the assumes that we did using the true counters $c_{1}$ and
$c_{2}$ to ensure $g$ is the inverse of $f$.

Note that the counter $c^{*}$ always stays ahead of the other counters, and
hence the assumes it makes are early.

The second complication to deal with are the assumptions that $c_{1}$ and
$c_{2}$ make when they check for equality with $0$. These again are not early
assumes in the construction. We modify the manipulation of the counter $c^{*}$
so that at every point it computes $r_{1}(c^{*})$, $r_{2}(c^{*})$,
$s_{1}(c^{*})$, and $s_{2}(c^{*})$. It also assumes the first two terms are
equal and the second two terms are disequal. Furthermore, for $0$ we have the
reverse; $r_{1}(0)\not=r_{2}(0)$ and $s_{1}(0)=s_{2}(0)$. These assumes are
again early as $c^{*}$ stays ahead of the true computation. Now, when we want
to simulate the check that $c_{1}$ is $0$, we instead check whether
$r_{1}(c_{1})\not=r_{2}(0)$, and to check if $c_{1}$ is not $0$, we check
$s_{1}(c_{1})\not=s_{2}(c_{1})$. Hence all assumes on the real simulation are
disequality assumes, and hence do not break the early assume requirement.

The rest of the construction and proof is simple.

###  B.2. Undecidability when programs executions are memoizing but do not
have early-assumes

We now give the main modifications of the main proof above to adapt it to a
proof of Theorem 3. In fact we will show programs with a _single_ non-early
assume already are undecidable to verify.

We again model the counters on terms as above. However, we start with two
variables $x$ and $y$, both representing $0$.

In every step, we simulate the counters $c_{1}$ and $c_{2}$ on terms
constructed from $x$, as before, but we make no assumes of equality.
Consequently, the initial model on terms involving $x$ would be a “free”
structure. Meanwhile, on $y$, we simulate a fake counter as before, that
continually increases, staying always ahead of the computation on $x$, and
ensuring that $g$ is the inverse of $f$ on terms involving $y$.

The initial model will keep the two submodels from $x$ and $y$ disjoint.

At the end of the computation (when we reach a final state of the 2-CM
machine), we do a single assume $x=y$. This will collapse two models, and
impose the structure the model on $y$ had on the free model on $x$. Hence the
counters and simulation become a correct simulation.

We again need to handle assumes that we need to make to check counters
equality with $0$. We do this as follows. We have functions $h_{1}$ and
$h_{2}$ that operate on the free model involving $x$, and in particular we
consider the terms of the form $h_{1}^{n}(x)$ and $h_{2}^{n}(x)$. These
essentially are meant to keep a copy of $0$, i.e., $x$. The fact that these
are equal to $x$ will be enforced later when the models of $x$ and $y$ merge.
Every time we want to check if a counter $c_{i}$ is equal to $x$, we check
instead whether $r(h_{i}(0))=r(c_{i})$, where $r$ is yet another function we
introduce. The idea is that $r$ will be identity on these terms, but again
that is assured later.

Meanwhile, in $y$, we ensure that $h_{1}(y)=y$ and $h_{1}(y)=y$ and $r$ is
identity. When we finally collapse the models with an assume that $x$ and $y$
are equal, it will impose the required structure on the model of $x$, and
hence the $0$-equality tests will become correct.

The above is the main idea of the construction; the rest of the construction
and proof is straightforward.

###### Acknowledgements.

We gratefully acknowledge National Science Foundation for supporting Umang
Mathur (grant NSF CSR 1422798), P. Madhusudan (grants 1138994 and SHF 1527395)
and Mahesh Viswanathan (grant NSF CPS 1329991).

## References

  * (1)
  * Alpern et al. (1988) B. Alpern, M. N. Wegman, and F. K. Zadeck. 1988.  Detecting Equality of Variables in Programs. In _Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’88)_. ACM, New York, NY, USA, 1–11.  https://doi.org/10.1145/73560.73561
  * Alur et al. (2005) Rajeev Alur, Michael Benedikt, Kousha Etessami, Patrice Godefroid, Thomas Reps, and Mihalis Yannakakis. 2005.  Analysis of Recursive State Machines.  _ACM Trans. Program. Lang. Syst._ 27, 4 (July 2005), 786–818.  https://doi.org/10.1145/1075382.1075387
  * Alur and Madhusudan (2004) Rajeev Alur and P. Madhusudan. 2004.  Visibly Pushdown Languages. In _Proceedings of the Thirty-sixth Annual ACM Symposium on Theory of Computing_ _(STOC ’04)_. ACM, New York, NY, USA, 202–211.  https://doi.org/10.1145/1007352.1007390
  * Alur and Madhusudan (2009) Rajeev Alur and P. Madhusudan. 2009.  Adding Nesting Structure to Words.  _J. ACM_ 56, 3, Article 16 (May 2009), 43 pages.  https://doi.org/10.1145/1516512.1516518
  * Bradley and Manna (2007) Aaron R. Bradley and Zohar Manna. 2007.  _The Calculus of Computation: Decision Procedures with Applications to Verification_.  Springer-Verlag, Berlin, Heidelberg.
  * Bryant et al. (2001) Randal E. Bryant, Steven German, and Miroslav N. Velev. 2001\.  Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic.  _ACM Trans. Comput. Logic_ 2, 1 (Jan. 2001), 93–134.  https://doi.org/10.1145/371282.371364
  * Burch and Dill (1994) Jerry R. Burch and David L. Dill. 1994.  Automatic Verification of Pipelined Microprocessor Control. In _Proceedings of the 6th International Conference on Computer Aided Verification_ _(CAV ’94)_. Springer-Verlag, London, UK, UK, 68–80.  http://dl.acm.org/citation.cfm?id=647763.735662
  * Chatterjee et al. (2016) Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. 2016\.  Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’16)_. ACM, New York, NY, USA, 733–747.  https://doi.org/10.1145/2837614.2837624
  * Chatterjee et al. (2015) Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. 2015\.  Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth. In _Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’15)_. ACM, New York, NY, USA, 97–109.  https://doi.org/10.1145/2676726.2676979
  * Courcelle and Engelfriet (2012) Professor Bruno Courcelle and Dr Joost Engelfriet. 2012.  _Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach_ (1st ed.).  Cambridge University Press, New York, NY, USA.
  * Dillig et al. (2011) Isil Dillig, Thomas Dillig, and Alex Aiken. 2011\.  Precise Reasoning for Programs Using Containers. In _Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’11)_. ACM, New York, NY, USA, 187–200.  https://doi.org/10.1145/1926385.1926407
  * Esparza et al. (2000) Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. 2000.  Efficient Algorithms for Model Checking Pushdown Systems. In _Proceedings of the 12th International Conference on Computer Aided Verification_ _(CAV ’00)_. Springer-Verlag, London, UK, UK, 232–247.  http://dl.acm.org/citation.cfm?id=647769.734087
  * Esparza and Knoop (1999) Javier Esparza and Jens Knoop. 1999.  An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis. In _Foundations of Software Science and Computation Structures_ , Wolfgang Thomas (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 14–30.
  * Farzan et al. (2014) Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2014\.  Proofs That Count. In _Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’14)_. ACM, New York, NY, USA, 151–164.  https://doi.org/10.1145/2535838.2535885
  * Farzan et al. (2015) Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2015\.  Proof Spaces for Unbounded Parallelism. In _Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’15)_. ACM, New York, NY, USA, 407–420.  https://doi.org/10.1145/2676726.2677012
  * Godefroid and Yannakakis (2013) Patrice Godefroid and Mihalis Yannakakis. 2013.  Analysis of Boolean Programs. In _Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems_ _(TACAS’13)_. Springer-Verlag, Berlin, Heidelberg, 214–229.  https://doi.org/10.1007/978-3-642-36742-7_16
  * Godoy and Tiwari (2009) Guillem Godoy and Ashish Tiwari. 2009.  Invariant Checking for Programs with Procedure Calls. In _Proceedings of the 16th International Symposium on Static Analysis_ _(SAS ’09)_. Springer-Verlag, Berlin, Heidelberg, 326–342.  https://doi.org/10.1007/978-3-642-03237-0_22
  * Granger (1991) Philippe Granger. 1991\.  Static Analysis of Linear Congruence Equalities Among Variables of a Program. In _Proceedings of the International Joint Conference on Theory and Practice of Software Development on Colloquium on Trees in Algebra and Programming (CAAP ’91): Vol 1_ _(TAPSOFT ’91)_. Springer-Verlag New York, Inc., New York, NY, USA, 169–192.  http://dl.acm.org/citation.cfm?id=111310.111320
  * Gulwani and Necula (2004a) Sumit Gulwani and George C. Necula. 2004a.  Global Value Numbering Using Random Interpretation. In _Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’04)_. ACM, New York, NY, USA, 342–352.  https://doi.org/10.1145/964001.964030
  * Gulwani and Necula (2004b) Sumit Gulwani and George C Necula. 2004b.  A polynomial-time algorithm for global value numbering. In _International Static Analysis Symposium_. Springer, 212–227.
  * Gulwani and Tiwari (2006) Sumit Gulwani and Ashish Tiwari. 2006.  Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions. In _Proceedings of the 15th European Conference on Programming Languages and Systems_ _(ESOP’06)_. Springer-Verlag, Berlin, Heidelberg, 279–293.  https://doi.org/10.1007/11693024_19
  * Heizmann et al. (2009) Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2009\.  Refinement of Trace Abstraction. In _Proceedings of the 16th International Symposium on Static Analysis_ _(SAS ’09)_. Springer-Verlag, Berlin, Heidelberg, 69–85.  https://doi.org/10.1007/978-3-642-03237-0_7
  * Heizmann et al. (2010) Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2010\.  Nested Interpolants. In _Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’10)_. ACM, New York, NY, USA, 471–482.  https://doi.org/10.1145/1706299.1706353
  * Heizmann et al. (2013) Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013\.  Software Model Checking for People Who Love Automata. In _Computer Aided Verification_ , Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 36–52.
  * Karp and Miller (1969) Richard M. Karp and Raymond E. Miller. 1969.  Parallel Program Schemata.  _J. Comput. Syst. Sci._ 3, 2 (May 1969), 147–195.  https://doi.org/10.1016/S0022-0000(69)80011-5
  * Karr (1976) Michael Karr. 1976\.  Affine Relationships Among Variables of a Program.  _Acta Inf._ 6, 2 (June 1976), 133–151.  https://doi.org/10.1007/BF00268497
  * Kosaraju (1982) S. Rao Kosaraju. 1982\.  Decidability of Reachability in Vector Addition Systems (Preliminary Version). In _Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing_ _(STOC ’82)_. ACM, New York, NY, USA, 267–281.  https://doi.org/10.1145/800070.802201
  * Löding et al. (2017) Christof Löding, P. Madhusudan, and Lucas Peña. 2017\.  Foundations for Natural Proofs and Quantifier Instantiation.  _Proc. ACM Program. Lang._ 2, POPL, Article 10 (Dec. 2017), 30 pages.  https://doi.org/10.1145/3158098
  * Lopes and Monteiro (2016) Nuno P. Lopes and José Monteiro. 2016.  Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic.  _International Journal on Software Tools for Technology Transfer_ 18, 4 (01 Aug 2016), 359–374.  https://doi.org/10.1007/s10009-015-0366-1
  * Madhusudan and Parlato (2011) P. Madhusudan and Gennaro Parlato. 2011.  The Tree Width of Auxiliary Storage. In _Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL ’11)_. ACM, New York, NY, USA, 283–294.  https://doi.org/10.1145/1926385.1926419
  * Mayr (1981) Ernst W. Mayr. 1981\.  An Algorithm for the General Petri Net Reachability Problem. In _Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing_ _(STOC ’81)_. ACM, New York, NY, USA, 238–246.  https://doi.org/10.1145/800076.802477
  * Müller-Olm and Seidl (2004) Markus Müller-Olm and Helmut Seidl. 2004.  A Note on Karr’s Algorithm. In _Automata, Languages and Programming_ , Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1016–1028.
  * Müller-Olm and Seidl (2005) Markus Müller-Olm and Helmut Seidl. 2005.  A Generic Framework for Interprocedural Analysis of Numerical Properties. In _Proceedings of the 12th International Conference on Static Analysis_ _(SAS’05)_. Springer-Verlag, Berlin, Heidelberg, 235–250.  https://doi.org/10.1007/11547662_17
  * Pek et al. (2014) Edgar Pek, Xiaokang Qiu, and P. Madhusudan. 2014.  Natural Proofs for Data Structure Manipulation in C Using Separation Logic. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ _(PLDI ’14)_. ACM, New York, NY, USA, 440–451.  https://doi.org/10.1145/2594291.2594325
  * Qiu et al. (2013) Xiaokang Qiu, Pranav Garg, Andrei Ştefănescu, and Parthasarathy Madhusudan. 2013.  Natural Proofs for Structure, Data, and Separation. In _Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation_ _(PLDI ’13)_. ACM, New York, NY, USA, 231–242.  https://doi.org/10.1145/2491956.2462169
  * Robertson and Seymour (1983) Neil Robertson and Paul D Seymour. 1983.  Graph minors. I. Excluding a forest.  _Journal of Combinatorial Theory, Series B_ 35, 1 (1983), 39–61.
  * Schwoon (2002) Stefan Schwoon. 2002\.  _Model-Checking Pushdown Systems_.  Ph.D. Thesis. Technische Universität München.  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schwoon-phd02.pdf
  * Seese (1991) D. Seese. 1991.  The structure of the models of decidable monadic theories of graphs.  _Annals of Pure and Applied Logic_ 53, 2 (1991), 169 – 195.  https://doi.org/10.1016/0168-0072(91)90054-P