The GOTO intermediate verification language used inside CBMC has no standalone syntax and semantics specification. This resulted in a lot of time spent reverse engineering CBMC and backtracking on design choices made when implementing new features, or in new features behaving in hard to predict and possibly unsound ways. In order to let us innovate faster with better soundness guarantees for our users, we will:

• define a reference syntax and semantics specification for the GOTO language
• create an concrete evaluator for that reference semantics that can validate a trace against a model
• create back-to-back testing tool that checks that a verification engine’s interpretation of a GOTO program complies with the reference semantics, by checking the compliance of a set of structure-covering traces produced by the verification tool.

Making GOTO a standalone language and providing independent means for checking trace validity removes the exclusive dependency on CBMC, and will let us innovate faster with better soundness guarantees for our users.

The reference evaluator can (will) later be used as an abstraction refinement oracle in a CEGAR loop for GOTO programs, as a starting point for a new fuzzing engine for GOTO programs, as starting point for a concolic or a symbolic execution engine for GOTO, etc.