-
Notifications
You must be signed in to change notification settings - Fork 176
Audit Correctness of CBMC backend #310
Copy link
Copy link
Open
Labels
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[F] SoundnessKani failed to detect an issueKani failed to detect an issue
Milestone
Description
Activity
Metadata
Metadata
Assignees
Labels
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[F] SoundnessKani failed to detect an issueKani failed to detect an issue
RMC uses CBMC as a backend. If CBMC has soundness bugs, RMC will as well.
Likelihood:
CBMC is a large, complex codebase which has had significant bugs in the past, and will likely continue to do so.
Mitigation:
Path to soundness:
Audit CBMC codebase, trusted model checker.
Documentation: