Automatic Verification of Partial Correctness of Golog Programs
Authors: Naiqi Li, Yongmei Liu
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | 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 linaiqi@mail2.sysu.edu.cn, ymliu@mail.sysu.edu.cn |
| 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). |