TL;DR
Zot is an extendible bounded model checker supporting multiple temporal logic encodings via plug-ins, facilitating experimentation and customization for different logic languages and applications.
Contribution
The paper introduces Zot, a flexible bounded model checker with a multi-layered logic support and plug-in architecture for encoding temporal logic as SAT problems.
Findings
Supports various logic languages through plug-ins
Encourages experimentation with simple, modifiable encodings
Offers an extendible and customizable model checking framework
Abstract
Zot is an agile and easily extendible bounded model checker, which can be downloaded at http://home.dei.polimi.it/pradella/. The tool supports different logic languages through a multi-layered approach: its core uses PLTL, and on top of it a decidable predicative fragment of TRIO is defined. An interesting feature of Zot is its ability to support different encodings of temporal logic as SAT problems by means of plug-ins. This approach encourages experimentation, as plug-ins are expected to be quite simple, compact (usually around 500 lines of code), easily modifiable, and extendible.
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 · Logic, programming, and type systems · Model-Driven Software Engineering Techniques