The VMT-LIB Language and Tools
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
TL;DR
VMT-LIB is a new language extending SMT-LIB to represent verification problems involving linear-time temporal properties on infinite-state systems, aiming to improve interoperability among verification tools.
Contribution
It introduces VMT-LIB, a standardized language and set of tools for encoding and exchanging verification benchmarks for infinite-state systems.
Findings
VMT-LIB enables interoperability among different verification tools.
Open-source tools facilitate working with the VMT-LIB language.
The language supports representing linear-time temporal properties on infinite-state systems.
Abstract
We present VMT-LIB, a language for the representation of verification problems of linear-time temporal properties on infinite-state symbolic transition systems. VMT-LIB is an extension of the standard SMT-LIB language for SMT solvers, developed with the goal of facilitating the interoperability and exchange of benchmark problems among different verification tools. Besides describing its syntax and semantics, we also present a set of open-source tools to work with the language.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Embedded Systems Design Techniques · Logic, programming, and type systems