Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf Wimmer, Dominik Stoffel, Wolfgang Kunz · 2004
We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of di#erent verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.