University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Novel Symbolic Approach to Verifying Epistemic Properties of Programs

Gorogiannis, N, Raimondi, F and Boureanu, Ioana (2017) A Novel Symbolic Approach to Verifying Epistemic Properties of Programs In: Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017), 19 - 25 August 2017, Melbourne, Australia.

ijcai17-kHoare.pdf - Accepted version Manuscript

Download (308kB) | Preview


We introduce a framework for the symbolic verification of epistemic properties of programs expressed in a class of general-purpose programming languages. To this end, we reduce the verification problem to that of satisfiability of first-order formulae in appropriate theories. We prove the correctness of our reduction and we validate our proposal by applying it to two examples: the dining cryptographers problem and the ThreeBallot voting protocol. We put forward an implementation using existing solvers, and report experimental results showing that the approach can perform better than state-of-the-art symbolic model checkers for temporal-epistemic logic.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Gorogiannis, N
Raimondi, F
Date : 25 August 2017
DOI : 10.24963/ijcai.2017/30
Copyright Disclaimer : Copyright © 2017 International Joint Conferences on Artificial Intelligence. All rights reserved.
Uncontrolled Keywords : Agent-based and Multi-agent Systems: Formal verification, validation and synthesis Multidisciplinary Topics and Applications: Validation and Verification
Related URLs :
Depositing User : Melanie Hughes
Date Deposited : 21 Jun 2017 13:12
Last Modified : 16 Jan 2019 18:53

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800