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

Résultats de recherche: Contribution à une conférence › Papier › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages	2100-2105
Nombre de pages	6
état	Publié - 1 janv. 2012
Modification externe	Oui
Evénement	26th AAAI Conference on Artificial Intelligence, AAAI 2012 - Toronto, Canada Durée: 22 juil. 2012 → 26 juil. 2012

Une conférence

Une conférence	26th AAAI Conference on Artificial Intelligence, AAAI 2012
Pays/Territoire	Canada
La ville	Toronto
période	22/07/12 → 26/07/12

Contient cette citation

@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

Résumé

Une conférence

Empreinte digitale

Contient cette citation