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..
SMT-Based Validation of Timed Failure Propagation Graphs
Authors: Marco Bozzano, Alessandro Cimatti, Marco Gario, Andrea Micheli
AAAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implemented a prototype tool using the techniques described in this paper. The tool is able to generate partial traces for a TFPG, test possibility and necessity of arbitrary conditions, check refinement, and perform diagnosis and diagnosability. Due to the lack of publicly available TFPGs, we evaluated the scalability of the approach on a benchmark of randomly generated TFPGs. We run two sets of experiments: refinement and diagnosability. |
| Researcher Affiliation | Academia | Marco Bozzano, Alessandro Cimatti, Marco Gario and Andrea Micheli Fondazione Bruno Kessler Italy EMAIL |
| Pseudocode | No | The paper uses mathematical formulas for encoding TFPGs (e.g., Bor, Tor, Band, Tand) but does not include any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Prototype tool and benchmarks are available at http://es.fbk.eu/people/gario/aaai15/ |
| Open Datasets | Yes | Due to the lack of publicly available TFPGs, we evaluated the scalability of the approach on a benchmark of randomly generated TFPGs. Prototype tool and benchmarks are available at http://es.fbk.eu/people/gario/aaai15/ |
| Dataset Splits | No | The paper describes using randomly generated TFPGs as benchmarks for evaluation, but it does not specify explicit training, validation, or test splits of a dataset in the context of model training/evaluation. |
| Hardware Specification | Yes | We run our experiments using Z3 (de Moura and Bjørner 2008) as SMT Solver on an Intel i7 2.93GHz, using a time-out of 300 seconds and memory-out of 2GB for all experiments. |
| Software Dependencies | No | The paper mentions 'Z3 as SMT Solver' but does not specify a version number for Z3 or any other software libraries or dependencies with their versions. |
| Experiment Setup | Yes | We run our experiments using Z3 (de Moura and Bjørner 2008) as SMT Solver on an Intel i7 2.93GHz, using a time-out of 300 seconds and memory-out of 2GB for all experiments. |