# SMT-based Model Checking for Recursive Programs

arXiv: https://arxiv.org/abs/1405.4028 · HTML: https://mlsanity.com/paper/1405.4028/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 May 2014.

## Built on by (most cited first, 16 of 16)

- [Toward Neural-Network-Guided Program Synthesis and Verification](https://mlsanity.com/paper/2103.09414/) (2021)
- [Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes](https://mlsanity.com/paper/2205.14943/) (2022)
- [Can LLM Aid in Solving Constraints with Inductive Definitions?](https://mlsanity.com/paper/2603.03668/) (2026)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)
- [SINGA-Easy: An Easy-to-Use Framework for MultiModal Analysis](https://mlsanity.com/paper/2108.02572/) (2021)
- [VisualTextRank: Unsupervised Graph-based Content Extraction for Automating Ad Text to Image Search](https://mlsanity.com/paper/2108.02725/) (2021)
- [Text is NOT Enough: Integrating Visual Impressions into Open-domain Dialogue Generation](https://mlsanity.com/paper/2109.05778/) (2021)
- [Discovering Personalized Semantics for Soft Attributes in Recommender Systems using Concept Activation Vectors](https://mlsanity.com/paper/2202.02830/) (2022)
- [Reinforced MOOCs Concept Recommendation in Heterogeneous Information Networks](https://mlsanity.com/paper/2203.11011/) (2022)
- [Explanation-Guided Fairness Testing through Genetic Algorithm](https://mlsanity.com/paper/2205.08335/) (2022)
- [Using Graph Neural Networks for Program Termination](https://mlsanity.com/paper/2207.14648/) (2022)
- [Tribe or Not? Critical Inspection of Group Differences Using TribalGram](https://mlsanity.com/paper/2303.09664/) (2023)
- [Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning](https://mlsanity.com/paper/2305.01206/) (2023)
- [Data-driven Verification of Procedural Programs with Integer Arrays](https://mlsanity.com/paper/2505.15958/) (2025)
- [Verification Modulo Tested Library Contracts](https://mlsanity.com/paper/2604.15533/) (2026)
- [Theory Under Construction: Orchestrating Language Models for Research Software Where the Specification Evolves](https://mlsanity.com/paper/2604.27209/) (2026)

## Abstract (arXiv)

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE "lazily". We use existing interpolation techniques to over-approximate QE and introduce "Model Based Projection" to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.