@inproceedings{taly2008synthesizing,
author = {Taly, Ankur and Gulwani, Sumit and Tiwari, Ashish},
title = {Synthesizing Switching Logic Using Constraint Solving},
booktitle = {VMCAI '09 Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation},
year = {2008},
month = {December},
abstract = {A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a sound technique for synthesizing a switching logic for changing modes so as to preserve the safety property. By construction, the synthesized hybrid system is well-formed and is guaranteed safe. Our approach is based on synthesizing a controlled invariant that is sufficient to prove safety. The generation of the controlled invariant is cast as a constraint solving problem, which is solved using SMT solvers. The generated controlled invariant is then used to arrive at the maximally liberal switching logic.},
publisher = {Springer-Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/synthesizing-switching-logic-using-constraint-solving/},
pages = {305},
edition = {VMCAI '09 Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation},
}