Reachability Modulo Theory Library
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina · EPiC series in computing · 2018
Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.