Constraint based Invariant Synthesis

Project Goal

Implement in Ultimate a library for a constraint-based synthesis of invariants.

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.

Literature

Motivation for the synthesis of invariants Slides of the lecture on Program Verification (Section 19: Constraint-Based Invariant Synthesis, currently at slide 433)

More details, examples, does not only introduce synthesis of safety invariants, but also synthesis of ranking functions, recurrence sets and interpolants. 2010CAV - Rybalchenko - Constraint Solving for Program Verification Theory and Practice by Example

Original paper on the topic. 2003CAV - Colón,Sankaranarayanan,Sipma - Linear Invariant Generation Using Non-linear Constraint Solving