We introduce a framework for the symbolic verificationudof epistemic properties of programs expressedudin a class of general-purpose programmingudlanguages. To this end, we reduce the verificationudproblem to that of satisfiability of first-order formulaeudin appropriate theories. We prove the correctnessudof our reduction and we validate our proposaludby applying it to two examples: the diningudcryptographers problem and the ThreeBallot votingudprotocol. We put forward an implementationudusing existing solvers, and report experimental resultsudshowing that the approach can perform betterudthan state-of-the-art symbolic model checkers forudtemporal-epistemic logic.
展开▼
