Skip to main navigation Skip to search Skip to main content

SMT-based verification of hybrid systems

  • FBK-irst

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationAAAI-12 / IAAI-12 - Proceedings of the 26th AAAI Conference on Artificial Intelligence and the 24th Innovative Applications of Artificial Intelligence Conference
Pages2100-2105
Number of pages6
Publication statusPublished - 7 Nov 2012
Externally publishedYes
Event26th AAAI Conference on Artificial Intelligence and the 24th Innovative Applications of Artificial Intelligence Conference, AAAI-12 / IAAI-12 - Toronto, ON, Canada
Duration: 22 Jul 201226 Jul 2012

Publication series

NameProceedings of the National Conference on Artificial Intelligence
Volume3

Conference

Conference26th AAAI Conference on Artificial Intelligence and the 24th Innovative Applications of Artificial Intelligence Conference, AAAI-12 / IAAI-12
Country/TerritoryCanada
CityToronto, ON
Period22/07/1226/07/12

Fingerprint

Dive into the research topics of 'SMT-based verification of hybrid systems'. Together they form a unique fingerprint.

Cite this