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 web interface of Z3, 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

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.