A formal semantics for GOTO in the CProver ecosystem

Abstract

This thesis develops a formal and extensible verification framework for the CProver family of tools. Tools such as CBMC, 2LS, and ESBMC share a common intermediate representation, the GOTO IR, as well as core verification steps (symbolic execution, loop unwinding, decision procedure). However, their independent implementations have lacked formal semantics and reusable infrastructure. This fragmentation impedes rigorous reasoning about tool behavior, complicates the adoption of new verification methods, and restricts interoperability. We introduce the GOTO language, a formal abstraction that puts CProver's existing GOTO IR on solid semantic foundations. Verification proceeds by symbolically executing GOTO programs to generate loop-free symbolic traces, which are encoded into logical formulae for automated decision procedures. We formalize the operational semantics of GOTO and trace evaluation, and provide a machine-checked Isabelle/HOL development to ensure soundness. To enable modular verification, we design a transformation infrastructure analogous to compiler passes. This includes slicing, common-subexpression elimination, memory modeling via intrinsic symbols, and control-flow simplification. Multiple backends -- bounded model checking, abstract interpretation, and others -- can be applied over the same GOTO programs. We implement the framework in ESBMC and assess its effectiveness on extensive benchmark suites (including SV-COMP categories). Our evaluation demonstrates significant performance and precision improvements arising from GOTO-based optimizations. We further enhance tool interoperability by translating GOTO binaries from alternative verifiers (such as Kani for Rust) into our framework, supporting hybrid workflows that leverage front-end strengths of CBMC, Kani, or other tools with ESBMC's backend. By unifying theory and practice, this work establishes a principled foundation for the design, implementation, and verification of the CProver ecosystem.

Date of Award	15 Dec 2025
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Lucas Cordeiro (Main Supervisor), Edoardo Manino (Co Supervisor) & Giles Reger (Co Supervisor)