@InProceedings{Mari+Tronci2007,
author="Mari, Federico
and Tronci, Enrico",
editor="Bemporad, A.
and Bicchi, A.
and Buttazzo, G.C.",
title="CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems",
booktitle="Hybrid Systems: Computation and Control (HSCC 2007)",
series="Lecture Notes in Computer Science",
year="2007",
publisher="Springer",
volume="4416",
pages="399--412",
optkeywords="Model Checking; Abstraction; CEGAR; SAT; Hybrid Systems; DTHS",
abstract="Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=92), last updated on Thu, 22 Nov 2012 14:59:18 +0100",
doi="10.1007/978-3-540-71493-4_32",
opturl="https://doi.org/10.1007/978-3-540-71493-4_32",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Mari2007.pdf:PDF"
}