Constraint based Invariant Synthesis

Introduction to the Topic

1. SMT-LIB

SMT-LIB is a standard that defines how to work with SMT formulas on a computer.

Ex 1.1: Download and run an SMT solver, e.g., Z3 https://github.com/Z3Prover/z3

In principle you could also use the Webinterface of the Z3 SMT solver, but I presume it is more convenient to have something that runs on your machine.

Ex 1.2 Write a bunch of SMT scripts that contain the check-sat command. Writing SMT scripts is not easy. Start with the scripts from the Z3 web interface and modify them. Use some formulas from you logics lecture. Use the get-model or the get-value command to get a satisfying assignment. Note that you will not get a response if your formulas become difficult. Formulas with quantifiers are typically difficult.

2. Boogie

Boogie is a language that is like programming languages suitable for writing down algorithms in a machine readable from. However, Boogie is typically not used by programmers to write code. It is typically used to model computer programs written in other programming languages.

• Boogie specification This is Boogie 2
• Microsoft's tool for Boogie verificationBoogie @ rise4fun
• A Boogie interpreter Boogaloo
• Verification of safety properties in Ultimate
• Termination analysis in Ultimate (link currently not working, problem with umlauts)
• Synthesis of ranking functions and nontermination arguments in Ultimate

Exercises

• Ex 2.1 Write some (small) Boogie program that is correct.
• Ex 2.2 Write some (small) Boogie program that not correct.
• Ex 2.3 Write some (small) Boogie program where Ultimate is unable to decide correctness.
• Ex 2.4 Write some (small) Boogie program that is nonterminating.
• Ex 2.5 Write some (small) Boogie program that is terminating.