Abstract 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 …

We present SMT-RAT, a C++ toolbox offering theory solver modules for the development of
SMT solvers for nonlinear real arithmetic (NRA). NRA is an important but hard-to-solve …

We consider bisimulation and weak bisimulation relations in the context of the labeled
Markov chains of Hansson and Jonsson, the concurrent labeled Markov chains of Philippou …

We consider satisfiability modulo theory-solving for linear real arithmetic. Inspired by related
work for the Fourier–Motzkin method, we combine virtual substitution with learning …

We generalize the framework of virtual substitution for real quantifier elimination to arbitrary
but bounded degrees. We make explicit the representation of test points in elimination sets …

Modern satisfiability solvers are able to determine satisfiability of a given propositional logic
formula very efficiently. Satisfiability modulo theories (SMT) is an approach to use solvers to …

Modern conflict-driven clause-learning (CDCL) Boolean satisfiability (SAT) solvers routinely
solve formulas from industrial domains with millions of variables and clauses, despite the …

Verification and testing for cyber-physical system may involve constraints that have both
Boolean and nonlinear numerical expressions. Such constraints are undecidable, so …

Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations
and inequalities over the domain of the real numbers. Coming with a strong expressiveness …

We consider satisfiability modulo theory-solving for linear real arithmetic. Inspired by related
work for the Fourier-Motzkin method, we combine virtual substitution with learning strategies …