-
Notifications
You must be signed in to change notification settings - Fork 156
Create a reference evaluator and back-to-back testing tool for the GOTO language
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.
List view
0 of 10 selected 0 issues of 10 selected
Abstract Syntax Specification Document for GOTO models
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2071 In model-checking/kani;Typing Rules and Semantics Specification Document for GOTO models
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2072 In model-checking/kani;Abstract Syntax Specification Document for GOTO traces
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2073 In model-checking/kani;Develop GOTO model AST for the evaluator
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2075 In model-checking/kani;Develop type-checking and invariant checking for GOTO models
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2076 In model-checking/kani;Develop reference trace evaluator for GOTO models
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2077 In model-checking/kani;Develop GOTO trace loader/deserialiser
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2079 In model-checking/kani;KR1: publish the GOTO syntax and semantics reference document on the github model-checking or
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2081 In model-checking/kani;KR2: publish the GOTO reference evaluator on the github model-checking org
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2082 In model-checking/kani;KR3: publish the GOTO back-to-back checking tool on the github model-checking org
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2083 In model-checking/kani;