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: International Joint Conference on Artificial Intelligence (IJCAI 2017), 19 - 25 August 2017, Melbourne, Australia.

[img]
Preview
Text
ijcai17-kHoare.pdf - Accepted version Manuscript

Download (308kB) | Preview

Abstract

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 :
NameEmailORCID
Gorogiannis, NUNSPECIFIEDUNSPECIFIED
Raimondi, FUNSPECIFIEDUNSPECIFIED
Boureanu, Ioanai.boureanu@surrey.ac.ukUNSPECIFIED
Date : 25 August 2017
Copyright Disclaimer : Copyright 2017 IJCAI
Related URLs :
Depositing User : Melanie Hughes
Date Deposited : 21 Jun 2017 13:12
Last Modified : 04 Aug 2017 08:17
URI: http://epubs.surrey.ac.uk/id/eprint/841450

Actions (login required)

View Item View Item

Downloads

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