SMT-Based Verification of Hybrid Systems

Alessandro Cimatti; Sergio Mover; Stefano Tonetta

SMT-Based Verification of Hybrid Systems

Alessandro Cimatti
, Sergio Mover
, Stefano Tonetta

Fondazione Bruno Kessler

Research output: Contribution to conference › Paper › peer-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 language	English
Pages	2100-2105
Number of pages	6
Publication status	Published - 1 Jan 2012
Externally published	Yes
Event	26th AAAI Conference on Artificial Intelligence, AAAI 2012 - Toronto, Canada Duration: 22 Jul 2012 → 26 Jul 2012

Conference

Conference	26th AAAI Conference on Artificial Intelligence, AAAI 2012
Country/Territory	Canada
City	Toronto
Period	22/07/12 → 26/07/12

Cite this

@conference{5d2b718e743342fd9f6ca6563f400154,

title = "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.",

author = "Alessandro Cimatti and Sergio Mover and Stefano Tonetta",

note = "Publisher Copyright: Copyright {\textcopyright} 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.; 26th AAAI Conference on Artificial Intelligence, AAAI 2012 ; Conference date: 22-07-2012 Through 26-07-2012",

year = "2012",

month = jan,

day = "1",

language = "English",

pages = "2100--2105",

}

TY - CONF

T1 - SMT-Based Verification of Hybrid Systems

AU - Cimatti, Alessandro

AU - Mover, Sergio

AU - Tonetta, Stefano

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

M3 - Paper

AN - SCOPUS:84885204105

SP - 2100

EP - 2105

T2 - 26th AAAI Conference on Artificial Intelligence, AAAI 2012

Y2 - 22 July 2012 through 26 July 2012

ER -

SMT-Based Verification of Hybrid Systems

Abstract

Conference

Fingerprint

Cite this