Skip to content

Constraint based Invariant Synthesis

Jump to bottom
Matthias Heizmann edited this page Feb 23, 2020 · 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.

Exercises

  • Ex 3.1 Draw a control-flow graph for a (very) small program.

...

11. Control-flow graphs in Ultimate

In Ultimate the effect of a transition is determined by TransFormula object.

  • Ex 11.1 Read documentation of TransFormula.
  • Ex 11.2 Find a presentation for the algorithm that is compatible to TransFormulas.
  • Ex 11.3 Pick a small CFG and write down (on paper) for each transition a logical formula that denotes the "effect" of this transition. Use two different formalisms: 1. a formula over primed and unprimed variables and 2. Ultimate's TransFormula.
  • Ex 11.4 Run Ultimate on some small program. Set a breakpoint in line 76 of the InvariantSynthesisObserver and use the debug mode of Eclipse to see the CFG and all of its TransFormulas.

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