Publications (14)
Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems
Srajan Goyal, Alberto Griggio, Jacob Kimblad +1
With increasing complexity of Automated Driving Systems (ADS), ensuring their safety and reliability has become a critical challenge. The Verification and Validation (V&V) of these…
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…
Software Model Checking via Large-Block Encoding
Dirk Beyer, Alessandro Cimatti, Alberto Griggio +2
The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-f…
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 xSAP Safety Analysis Platform
Benjamin Bittner, Marco Bozzano, Roberto Cavada +6
This paper describes the xSAP safety analysis platform. xSAP provides several model-based safety analysis features for finite- and infinite-state synchronous transition systems. In…
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…
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
The problem of computing Craig interpolants in SAT and SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for int…
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositiona…
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…
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…
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…
IC3 Modulo Theories via Implicit Predicate Abstraction
Alessandro Cimatti, Alberto Griggio, Sergio Mover +1
We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theorie…
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
The problem of computing Craig Interpolants has recently received a lot of interest. In this paper, we address the problem of efficient generation of interpolants for some importan…