HyComp swMATH ID: 20163 Software Authors: A. Cimatti, A. Griggio, S. Mover, S. Tonetta Description: HyComp: An SMT-based model checker for hybrid systems. 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. This work was carried out within the D-MILS project, which is partially funded under the European Commission’s Seventh Framework Programme (FP7). Homepage: http://link.springer.com/chapter/10.1007/978-3-662-46681-0_4 Related Software: nuXmv; CTIGAR; z3; NuSMV; MathSAT5; Kronos; Uppaal; Flow*; SpaceEx; ODEPACK; HyTech; KeYmaera; Spacer; iSAT; dReach; HYST; PySMT; CalCS; dReal; Yices Cited in: 5 Publications all top 5 Cited by 17 Authors 2 Cimatti, Alessandro 1 Bittner, Benjamin 1 Bozzano, Marco 1 Dague, Philippe 1 Gallois, Jean-Pierre 1 Gario, Marco 1 Griggio, Alberto 1 Irfan, Ahmed 1 Ishizawa, Takuya 1 Roveri, Marco 1 Sebastiani, Roberto 1 Suenaga, Kohei 1 Tonetta, Stefano 1 Travé-Massuyès, Louise 1 Vozarova, Viktoria 1 Ye, Lina 1 Zaatiti, Hadi Cited in 2 Serials 1 Artificial Intelligence 1 Journal of Logical and Algebraic Methods in Programming Cited in 3 Fields 4 Computer science (68-XX) 2 Systems theory; control (93-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year