Simon Robillard

Loop Analysis by Quantification over Iterations

2018 · EPiC series in computing

We present a framework to analyze and verify programs containing loops by using a first-order language of so-called extended expressions. This language can express both functional and temporal properties of loops. We prove soundness and …

A Strategy Language for Controlled Proof Search

2026 · Electronic Proceedings in Theoretical Computer Science

This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search.We give the semantics of strategies as functions over proof states, and of the operators that …