We present VMT-LIB, a language for the representation of verification problems of invariant and linear-time temporal properties on infinite-state symbolic transition systems. VMT-LIB is developed with the goal of facilitating the interoperability and exchange of benchmark problems among different verification tools. The VMT-LIB language an extension of the standard SMT-LIB language for SMT solvers, from which it inherits the clean semantics and the many available resources. In this paper we describe the syntax and semantics of VMT-LIB, and present a set of open-source tools to work with the language.
The VMT-LIB Language and Tools
Alessandro Cimatti;Alberto Griggio;Stefano Tonetta
2022-01-01
Abstract
We present VMT-LIB, a language for the representation of verification problems of invariant and linear-time temporal properties on infinite-state symbolic transition systems. VMT-LIB is developed with the goal of facilitating the interoperability and exchange of benchmark problems among different verification tools. The VMT-LIB language an extension of the standard SMT-LIB language for SMT solvers, from which it inherits the clean semantics and the many available resources. In this paper we describe the syntax and semantics of VMT-LIB, and present a set of open-source tools to work with the language.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.
