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..
Concurrency Debugging with MaxSMT
Authors: Miguel Terra-Neves, Nuno Machado, Ines Lynce, Vasco Manquinho1608-1616
AAAI 2019 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that using Max SMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs. |
| Researcher Affiliation | Collaboration | 1INESC-ID / Instituto Superior T ecnico, Universidade de Lisboa, Portugal 2Teradata Spain and HASLab INESC TEC / Universidade do Minho, Portugal |
| Pseudocode | Yes | Algorithm 1: Progressive algorithm for computing an alternate schedule. |
| Open Source Code | Yes | The Max SMT models and algorithms were integrated in the publicly available versions of SYMBIOSIS3 and CORTEX4 tools. 3http://github.com/nunomachado/symbiosis 4http://github.com/nunomachado/cortex-tool |
| Open Datasets | Yes | We consider two sets of test cases. The first includes several C/C++ and Java applications with strictly schedule-dependent bugs, such as shared buffer implementation or an adapted parallel file scanner (Elmas et al. 2013). The second set includes programs with path-schedule dependent bugs from the IBM Con Test benchmark suite, as well as the Ex MCR benchmark. |
| Dataset Splits | No | The paper mentions using "test cases" and "benchmarks" for evaluation but does not specify any training/validation/test dataset splits or cross-validation setup. |
| Hardware Specification | No | The paper does not provide specific details about the hardware used for the experiments, such as GPU/CPU models, memory, or specific cluster configurations. |
| Software Dependencies | Yes | In our experiments, Z3 (Bjørner and Phan 2014) (version 4.6.0) was used as the Max SMT solver. |
| Experiment Setup | Yes | For the inc (incomplete) sub-column, a conflict threshold of 200000 was used. A time limit of 3 hours was imposed for each execution on a particular test case. We consider two types of Max SMT models: one where all criteria are equally significant (i.e., φs = φdf s φbs s φcs s ) and one lexicographic model that optimizes φdf s first, followed by φbs s and then φcs s . |