#### Alladi Ramakrishnan Hall

#### Symbolic Verification of Epistemic Properties in Programs

#### Ioana Boureanu

##### University of Surrey, UK

*In this talk, we will look at one approach to make the model checking of certain privacy-encoding properties in simple programs more efficient. Concretely, we target knowledge-intrinsic properties over the states of a program, such as “a program-observer knows that variable x is equal to y + 5”. To formalise these, we introduce a “program-epistemic” logic, in which we can express statements like: if command/program C starts at a state satisfying φ, then in all states where the execution of C finishes, agent A is epistemically unaware of π. In the latter, π is a formula which can contain several knowledge/epistemic operators scoping quantifier-free first-order formulae. We show that, in some cases and for simple programs, model checking this logic can be reduced to SMT-solving. Lastly, we report our experimental results which show that this technique significantly outperforms epistemic model checking.*

Based on joint work with Nikos Gorogiannis and Franco Raimondi, presented at IJCAI2017.

Done