18 citations · 31 across the 3 of their papers we have counts for
3 papers
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Makai Mann, Ahmed Irfan, Alberto Griggio +2
We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems th…
Satisfiability Modulo Transcendental Functions via Incremental Linearization
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan +2
In this paper we present an abstraction-refinement approach to Satisfiability Modulo the theory of transcendental functions, such as exponentiation and trigonometric functions. The…
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan +2
Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand…