HyComp is a model checker for hybrid systems based on Satisfiability Modulo Theories (SMT). HyComp takes as input networks of hybrid automata specified using the HyDI symbolic language. HyComp relies on the encoding of the network into an infinite-state transition system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction, IC3). The tool features specialized encodings of the automata network and can discretize various kinds of dynamics. HyComp can verify invariant and LTL properties, and scenario specifications; it can also perform synthesis of parameters ensuring the satisfaction of a given (invariant) property. All these features are provided either through specialized algorithms, as in the case of scenario or LTL verification, or applying off-the-shelf algorithms based on SMT. We describe the tool in terms of functionalities, architecture, and implementation, and we present the results of an experimental evaluation.

HYCOMP - an SMT-based model checker for hybrid systems / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - 9035:(2015), pp. 52-67. (Intervento presentato al convegno 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a London, UK nel April 11-18, 2015) [10.1007/978-3-662-46681-0_4].

HYCOMP - an SMT-based model checker for hybrid systems

Cimatti A.;Griggio A.;Mover S.;Tonetta S.
2015-01-01

Abstract

HyComp is a model checker for hybrid systems based on Satisfiability Modulo Theories (SMT). HyComp takes as input networks of hybrid automata specified using the HyDI symbolic language. HyComp relies on the encoding of the network into an infinite-state transition system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction, IC3). The tool features specialized encodings of the automata network and can discretize various kinds of dynamics. HyComp can verify invariant and LTL properties, and scenario specifications; it can also perform synthesis of parameters ensuring the satisfaction of a given (invariant) property. All these features are provided either through specialized algorithms, as in the case of scenario or LTL verification, or applying off-the-shelf algorithms based on SMT. We describe the tool in terms of functionalities, architecture, and implementation, and we present the results of an experimental evaluation.
2015
Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings
Cham, Switzerland
Springer
978-3-662-46680-3
Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.
HYCOMP - an SMT-based model checker for hybrid systems / Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S.. - 9035:(2015), pp. 52-67. (Intervento presentato al convegno 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a London, UK nel April 11-18, 2015) [10.1007/978-3-662-46681-0_4].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/343005
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 47
  • ???jsp.display-item.citation.isi??? ND
  • OpenAlex ND
social impact