SMT-Based Verification of Hybrid Systems
Abstract
Hybrid automata networks (HAN) are a powerful formalism to model complex embedded systems. In this paper, we survey the recent advances in the application of Satisfiability Modulo Theories (SMT) to the analysis of HAN. SMT can be seen as an extended form of Boolean satisfiability (SAT), where literals are interpreted with respect to a background theory (e.g. linear arithmetic). HAN can be symbolically represented by means of SMT formulae, and analyzed by generalizing to the case of SMT the traditional model checking algorithms based on SAT.
Cite
Text
Cimatti et al. "SMT-Based Verification of Hybrid Systems." AAAI Conference on Artificial Intelligence, 2012. doi:10.1609/AAAI.V26I1.8442Markdown
[Cimatti et al. "SMT-Based Verification of Hybrid Systems." AAAI Conference on Artificial Intelligence, 2012.](https://mlanthology.org/aaai/2012/cimatti2012aaai-smt/) doi:10.1609/AAAI.V26I1.8442BibTeX
@inproceedings{cimatti2012aaai-smt,
title = {{SMT-Based Verification of Hybrid Systems}},
author = {Cimatti, Alessandro and Mover, Sergio and Tonetta, Stefano},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2012},
pages = {2100-2105},
doi = {10.1609/AAAI.V26I1.8442},
url = {https://mlanthology.org/aaai/2012/cimatti2012aaai-smt/}
}