550 citations · 8k across the 290 of their papers we have counts for
11 papers · 1 filter
Verification of Configurable SRA Systems
Alessandro Cimatti, Alberto Griggio, Christian Lidström +2
Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous s…
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
Interlocking logics are at the core of critical systems controlling the traffic within stations. In this paper, we consider a generic interlocking logic, which can be instantiated…
Invariant Checking for SMT-based Systems with Quantifiers
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio +1
This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State…
The VMT-LIB Language and Tools
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
We present VMT-LIB, a language for the representation of verification problems of linear-time temporal properties on infinite-state symbolic transition systems. VMT-LIB is an exten…
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…