Skip to content

Constraint based Invariant Synthesis

Jump to bottom
Matthias Heizmann edited this page Nov 5, 2019 · 22 revisions

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.

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.

3. Control-flow Graphs

In this project we will use control-flow graphs to represent programs. A (rather formal) introduction can be found in the Slides of the lecture on Program Verification in Section 10 (control-flow graphs) which is currently on slide 264.

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

Clone this wiki locally