Hybrid automata-based CEGAR for rectangular hybrid systems
In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we ...
Optimization techniques for craig interpolant compaction in unbounded model checking
This paper addresses the problem of reducing the size of Craig interpolants generated within inner steps of SAT-based Unbounded Model Checking. Craig interpolants are obtained from refutation proofs of unsatisfiable SAT runs, in terms of and/or circuits ...
Practical policy iterations
Policy iterations is a technique based on game theory that relies on a sequence of numerical optimization queries to compute the fixpoint of a set of equations. It has been proposed to support the static analysis of programs as an alternative to ...