Léo Stefanesco

Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions

Bitvectors are foundational for automated reasoning about programs, and fixed-width bitvector solvers (QF_BV) are fast and ubiquitous. However, the theory of parametric bitvectors (PBV), where widths are symbolic, is much less well understood. The theory of multi-width PBV, where...

Constructive characterisations of the must -preorder for asynchrony

De Nicola and Hennessy's must -preorder is a liveness preserving refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q . Owing to the universal quantification over clients, this definition does not yield a practical proof...