SMU Research Data Repository (RDR)
Browse

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

Download (22.4 MB)
software
posted on 2024-09-30, 08:26 authored by Krishnendu Chatterjee, Amir Goharshady, Ehsan Goharshady, Mehrdad Karrabi, Djordje ZIKELICDjordje ZIKELIC

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

History

Confidential or personally identifiable information

  • I confirm that the uploaded data has no confidential or personally identifiable information.

Usage metrics

    School of Computing and Information Systems

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC