thesis Krishnendu Chatterjee author Amir Kafshdar Goharshady author Ehsan Kafshdar Goharshady author Mehrdad Karrabi author Ðorđe Žikelić author KrCh department This repository contains the artifact of the paper titled "Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs" accepted at FM 2024. 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. Repository2024 10.5281/zenodo.12518216 https://research-explorer.ista.ac.at/record/18155 Chatterjee, Krishnendu, et al. <i>Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs</i>. Repository, 2024, doi:<a href="https://doi.org/10.5281/zenodo.12518216">10.5281/zenodo.12518216</a>. Chatterjee, K.,   Kafshdar Goharshady, A., Kafshdar Goharshady, E., Karrabi, M., &#38; Žikelić, Ð. (2024). Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. Repository. <a href="https://doi.org/10.5281/zenodo.12518216">https://doi.org/10.5281/zenodo.12518216</a> Chatterjee, Krishnendu, Amir   Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, and Ðorđe Žikelić. “Data for Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial Programs.” Repository, 2024. <a href="https://doi.org/10.5281/zenodo.12518216">https://doi.org/10.5281/zenodo.12518216</a>. Chatterjee K,   Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. 2024. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs, Repository, <a href="https://doi.org/10.5281/zenodo.12518216">10.5281/zenodo.12518216</a>. Chatterjee K,   Kafshdar Goharshady A, Kafshdar Goharshady E, Karrabi M, Žikelić Ð. Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs. 2024. doi:<a href="https://doi.org/10.5281/zenodo.12518216">10.5281/zenodo.12518216</a> K. Chatterjee, A.   Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, and Ð. Žikelić, “Data for Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs.” Repository, 2024. K. Chatterjee, A.   Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi, Ð. Žikelić, (2024). 227982026-09-03T11:50:15Z2026-09-03T11:51:23Z