Lambda
Lambda is a model checker for the safety of parameterized transition systems. The state variables of a system are functions from uninterpreted sorts into Bool, Int, Real or an enumeration, and formulae describing the system have quantifiers that range over the uninterpreted sorts only. Lambda tries to show that a safety property holds in the system, for all cardinalities of the sorts, or to find a counterexample.
The input language is an extension of VMT-LIB, described on the Input language page.
Results
Lambda reports one of three verdicts. For safe, it produces an inductive invariant, which can be exported as SMT-LIB
obligations to be checked by an external solver such as Z3 or cvc5, or as a Veil module to be checked in Lean.
For unsafe, it produces a trace over finite universes. The verdict is unknown if an SMT check is inconclusive.
Algorithms
The algorithm is selected with --algo; all of them share the same representation, grounding and lemma management.
bounded-induction(default): generalizes invariants of ground instances, found with IC3, into quantified lemmas, and checks them with Z3 (optionally with Houdini filtering) or with a quantifier-instantiation procedure on MathSAT.parameter-abstraction: same loop as above, but the check for all sizes is done on a quantifier-free abstraction that tracks finitely many indices explicitly, using ic3ia. It applies to a specific syntactic fragment.updria: universal property-directed reachability with implicit predicate abstraction, refined with interpolants from ground instances. It returns invariants that are uniform in the cardinalities.bmc: bounded model checking with Z3, optionally on fixed cardinalities. It can find counterexamples but cannot prove safety.
Lambda 1.0 is available on the Download page, together with the benchmark collection.
More
- Download and installation instructions
- Usage: options, input formats and certificates
- Benchmarks: the corpus distributed with Lambda
- Publications