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..
Automatic Verification of Partial Correctness of Golog Programs
Authors: Naiqi Li, Yongmei Liu
IJCAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments show that our method can not only handle sequential and nested loops uniformly in a reasonable among of time, but also be used to discover succinct and comprehensible loop invariants and state constraints. |
| Researcher Affiliation | Academia | Naiqi Li Yongmei Liu Department of Computer Science, Sun Yat-sen University, Guangzhou 510006, China EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: veri(P, δ, Q, M) and Algorithm 2: infer(φ(s), δl, asso) |
| Open Source Code | No | The paper does not provide an unambiguous statement about releasing source code or a direct link to a repository for the described methodology. |
| Open Datasets | Yes | Our system successfully verified 22 programs in 9 domains. Among them the logistics domain is from the AIPS 00 planning competition, and the other 8 domains are adapted from those used in [Hu, 2012]. |
| Dataset Splits | No | The paper mentions using '9 domains' and '22 programs' for verification but does not specify any dataset splits like train/validation/test percentages or sample counts. |
| Hardware Specification | Yes | All experiments were conducted on a personal laptop equipped with 2.60 GHz CPU and 4.00GB RAM under Linux. |
| Software Dependencies | No | The paper mentions 'SWI-Prolog', 'E Prover [Schulz, 2013]', and 'Mini Sat [E en and S orensson, 2003]' but does not provide specific version numbers for these software dependencies. |
| Experiment Setup | Yes | In practice we preset a constant K, and let prog[M, δ ] = SK n=0 prog[M, δn]. while counter < K1 do (Algorithm 1) and while counter < K2 do (Algorithm 2). |