Milestone [1]: AST -> CFG -> FOL (no loops) | |
זמן: Time: Time: Time: | 20/04/2021 16:30 |
זמן סיום: End Time: End Time: End Time: | 20/04/2021 18:30 |
The students will demonstrate an implementation that transforms an AST to a CFG, and produces an FOL formula using the proof rule shown in class. |
Milestone [2]: Loops + Arrays + SMT | |
זמן: Time: Time: Time: | 18/05/2021 |
זמן סיום: End Time: End Time: End Time: | 18/05/2021 |
The student will present verification benchmarks involving loops and arrays, and an implementation that can verify the assertions in them. We will use Z3, and SMT solver; for now, loop invariants are provided as part of the specification. |