Skip to content

Constraint based Invariant Synthesis

Jump to bottom
Matthias Heizmann edited this page Mar 4, 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.

12. Invariant Templates

  • Task 12.1: Write down a list of all parameters that define the invariant templates.
  • Task 12.2: Propose a data structure that defines the invariant templates. This data structure should be independent of the input program and should be used to build the invariant template. Alternatively, you can write a (highly parameterized) algorithm for building the invariant template. Note that this is a difficult task where you have to find a trade-off. If you use a formula-like tree-based data structure, it is easy to build the template from the data structure but difficult to construct the data structure. If you just use a list of integers it is easy to construct the data structure but you might not be able to build all interesting templates.

98. Parameters that Define the Templates.

We have one template per program point.

  • Number of disjuncts. (We assume, the template is given as DNF)
  • Number of conjuncts. (We assume that each conjunct is an (in)equality)
  • Relation symbol of (in)equality. Either =, <=, or <.
  • Variables that occur in (in)equality
  • Possible values for coefficients.

99. Relevant Classes in Ultimate

Substitution, SubstitutionWithLocalSimplification

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