Fortunac/general loop invariant checker

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.

MIT License

102 stars 14 forks source link

Closed fortunac closed 3 years ago

fortunac commented 3 years ago

Simplifies the loop invariant checker to handle more general cases
- Rather than finding the loop guard and creating constraints from those, we find the weakest precondition for the loop itself.
- invariant /\ (invariant => ite(!loop_guard, precondition of the exit, wp(loop_body, invariant))
Adds more test cases:
- A loop with a nondeterministic number of iterations
- A do while loop
- A loop with a break
- A non-terminating loop

codyroux commented 3 years ago

This is neato burrito! Very nice stuff.