Automatically Verifying Expressive Epistemic Properties of Programs
Authors: Francesco Belardinelli, Ioana Boureanu, Vadim Malvone, Fortunat Rajaona
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments. This work lends itself to checking several canonical examples in epistemic verification and a quite few others. ... In Table 1, all the answers to the formulas α1, α2, α 2 and α3 checked are as expected. ... To see the performance, we report the time it took to get the satisfaction results, for n = 5 and n = 10 cryptographers. |
| Researcher Affiliation | Academia | Francesco Belardinelli1, Ioana Boureanu2, Vadim Malvone3, Fortunat Rajaona2 1Imperial College London 2Surrey Centre for Cyber Security, University of Surrey 3T el ecom Paris francesco.belardinelli@imperial.ac.uk, {i.boureanu, s.rajaona}@surrey.ac.uk, vadim.malvone@telecom-paris.fr |
| Pseudocode | No | The paper provides formal definitions (e.g., Definition 7 for the translation τ) that describe the logic and translation recursively, but it does not include explicitly labeled 'Pseudocode' or 'Algorithm' blocks for an executable procedure. |
| Open Source Code | Yes | Our code mechanising the translation and examples encoded/tested in/with it is available at http://people.itcarlson.com/ioana/epistemic-program-verifier/src. |
| Open Datasets | No | The paper uses the 'dining cryptographers example' as a benchmark, which is a problem setup described mathematically within the paper and in referenced works (Chaum 1988; Gorogiannis, Raimondi, and Boureanu 2017), rather than an external, publicly available dataset that would be downloaded or cited with specific access information. |
| Dataset Splits | No | The paper evaluates logical formulas on a problem instance (dining cryptographers) but does not describe the use of dataset splits for training, validation, or testing. |
| Hardware Specification | No | The paper reports performance times for its experiments but does not specify the hardware (e.g., CPU, GPU models, or memory) used to obtain these results. |
| Software Dependencies | No | The paper states, 'To check the satisfiability/validity of the first-order formula resulting from the translation, we use the Haskell library SBV. ... SBV allows to use several SMT solvers, with Z3 as its default solver.' However, it does not provide specific version numbers for SBV, Z3, or Haskell. |
| Experiment Setup | No | The paper describes the logical problem setup, including variable definitions and formulas (e.g., for the Dining Cryptographers example: 'The domain of variables is B = {T, F}. The program variables are p = {x} {pi, ci | 0 i < n}'), and the logical formulas evaluated. However, it does not provide concrete experimental setup details such as hyperparameters, optimization settings, or other system-level training configurations typically found in experimental sections. |