---
OA_place: repository
OA_type: green
_id: '22798'
abstract:
- lang: eng
  text: "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.\r\n\r\nThe 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.\r\n \r\nThe 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."
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  last_name: Chatterjee
- first_name: Amir
  full_name: '  Kafshdar Goharshady, Amir'
  last_name: '  Kafshdar Goharshady'
- first_name: Ehsan
  full_name: Kafshdar Goharshady, Ehsan
  last_name: Kafshdar Goharshady
- first_name: Mehrdad
  full_name: Karrabi, Mehrdad
  last_name: Karrabi
- first_name: Ðorđe
  full_name: Žikelić, Ðorđe
  last_name: Žikelić
citation:
  ama: 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>
  apa: 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>
  chicago: 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>.
  ieee: 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.
  ista: 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>.
  mla: 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>.
  short: K. Chatterjee, A.   Kafshdar Goharshady, E. Kafshdar Goharshady, M. Karrabi,
    Ð. Žikelić, (2024).
date_created: 2026-09-03T11:50:15Z
date_published: 2024-06-24T00:00:00Z
date_updated: 2026-09-03T11:51:23Z
day: '24'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.5281/zenodo.12518216
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5281/zenodo.12518216
month: '06'
oa: 1
oa_version: None
publisher: Repository
related_material:
  record:
  - id: '18155'
    relation: used_in_publication
    status: public
status: public
title: Data for Sound and Complete Witnesses for Template-based Verification of LTL
  Properties on Polynomial Programs
type: research_data_reference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2024'
...
