Skip to content

State Space Travel

Pre-release
Pre-release
Compare
Choose a tag to compare
@michbarsinai michbarsinai released this 01 Mar 09:38
· 182 commits to master since this release

DFSBProgramVerifier can now continue to traverse the program state space AFTER it has found a violation. This allows detecting multiple violations, pruning, and performing other explorations of a b-programs' state space.

Also, various improvements, especially regarding hashing functions of BProgramSyncSnapshots, and the objects that compose them.