Artifact for Formal Methods 2024 paper "Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs"

Artifact for conference paper "Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs", accepted at 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024.

See README for details.

The task of verifying an LTL formula on a program can be reduced to verifying a Büchi specification on the product transition system. This tool takes a non-deterministic transition system together with a Büchi specification as input and based on user preferences tries to either (i) prove the existence of a run in the program that satisfies the Büchi condition or (ii) demonstrate that every run of the program satisfies the Büchi condition.

The tool is written in Java and works well with openjdk 11 on Ubuntu 22.04. Running all the experiments can take weeks to finish. We have provided a script for running the strongest configuration of our tool which solves most of the benchmarks and takes less than 48 hours. Detailed guidance is given in the readme file.

External link: https://zenodo.org/records/12518217