Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Linear Temporal Logic Modulo Theories over Finite Traces
Authors: Luca Geatti, Alessandro Gianola, Nicola Gigante
IJCAI 2022 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks. |
| Researcher Affiliation | Academia | Luca Geatti , Alessandro Gianola , Nicola Gigante Free University of Bozen-Bolzano, Italy EMAIL |
| Pseudocode | Yes | Algorithm 1 BLACK s main procedure for LTLf MT |
| Open Source Code | Yes | The source code and all the tests and benchmarks are available in BLACK s Git Hub repository, merged into version 0.7 of the tool. |
| Open Datasets | No | The paper mentions 'crafted benchmarks' and 'scalable patterns' but does not provide specific access information (links, DOIs, formal citations) to a publicly available or open dataset. |
| Dataset Splits | No | The paper does not explicitly specify training, validation, or test dataset split percentages or sample counts. |
| Hardware Specification | No | The paper states, 'The tests were run on commodity hardware,' which is not a specific hardware description required for reproducibility. |
| Software Dependencies | No | The paper mentions 'setting BLACK to use the Z3 backend [de Moura and Bjørner, 2008],' but it does not specify a version number for the Z3 solver or any other software dependency. |
| Experiment Setup | Yes | The tests were run on commodity hardware, setting BLACK to use the Z3 backend [de Moura and Bjørner, 2008]. The table shows... a qualitative plot of running times from N = 1 up to the maximum value of N which runs under the 5 minutes timeout. |