SMT-Based Verification of Hybrid Systems

Authors

  • Alessandro Cimatti Fondazione Bruno Kessler
  • Sergio Mover Fondazione Bruno Kessler
  • Stefano Tonetta Fondazione Bruno Kessler

DOI:

https://doi.org/10.1609/aaai.v26i1.8442

Keywords:

SMT, SMT-based verification, network of hybrid automata, message sequence charts, bounded model checking, k-induction

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.

Downloads

Published

2021-09-20

How to Cite

Cimatti, A., Mover, S., & Tonetta, S. (2021). SMT-Based Verification of Hybrid Systems. Proceedings of the AAAI Conference on Artificial Intelligence, 26(1), 2100-2105. https://doi.org/10.1609/aaai.v26i1.8442

Issue

Vol. 26 No. 1 (2012): Twenty-Sixth AAAI Conference on Artificial Intelligence

Section

Spotlight