The tutorial will present several symbolic computation, invariant generation and theorem proving methods and tools. By the end of the tutorial, participants will have a better understanding in choosing the appropriate methodology for their specific application.

The tutorial is meant for graduate and undergraduate students, as well as for more experienced researchers in the field of formal methods and symbolic computation.

Organisation

This tutorial will be co-located with the SYNASC 2011 conference, Timisoara, Romania.

The tutorial will be organised as a series of four connected tutorial sessions. Each of the tutorial sessions will be of half a day. Tutorial sessions will overview foundations and challenges, describe available tool support for various theoretical frameworks, and comprise of an interleaving of tool presentations and labs. The lab sessions will give the attendees an opportunity to get some hands on experience with the presented tools.

Organisers

• Laura Kovács (Vienna University of Technology)
• Veronika Pillwein (Research Institute for Symbolic Computation, Linz)
• Andrei Voronkov (The University of Manchester)

Schedule

The tutorial will be of 2 days and will take place during the SYNASC 2011 conference. The exact date will soon be announced.

The tutorial will comprise of four sessions, as follows:

• Tutorial 1: Symbolic Computation (Groebner Bases, Cylindrical Decomposition, Symbolic Summation)
  • Particular focus on: Groebner basis, cylindrical decomposition, and symbolic summation
  • Speaker: Veronika Pillwein (Research Institute for Symbolic Computation, Linz)
  • Abstract: Groebner bases and Cylindrical Algebraic Decomposition are two fundamental tools in symbolic computation. Groebner bases can be used to analyse systems of polynomial equations, and Cylindrical Algebraic Decomposition can be used to analyse systems of polynomial inequalities. Analyse may mean finding a sample solution, computing the dimension of the solution space, proving that one system implies another.

    Both have a variety of applications. The emphasis of this tutorial is to give an overview on show case problems and to present show case solutions. One particular field of applications arises in the context of symbolic summation. Slightly extending the classical domain for which Groebner bases and Cylindrical Decomposition were introduced, we show how to deal with questions on how to compute closed form representations, derive recurrence relations or decide positivity of certain sums.

• Tutorial 2: Theorem Proving
  • Particular focus on: Resolution and superposition calculus, saturation algorithms, and redundancy elimination
  • Speaker: Andrei Voronkov (The University of Manchester)
  • Abstract: Reasoning with quantifiers and theories is generally regarded as the main obstacle in applications of reasoning to software verification.

    In this tutorial we address this challenge, and overview the power and limitations of automated first-order theorem proving. To this end, we will discuss the the resolution and superposition calculus, introduce the saturation principle, and present various algorithms implementing redundancy elimination, preprocessing and clause form transformation.

    Throughout this tutorial session we will use the first-order theorem prover Vampire. To this end, we will describe basic principles of using Vampire, and overview implementation issues of saturation, and the resolution and superposition calculus. We will also present various Vampire options for controlling the proof search.

• Tutorial 3: Program Assertion Synthesis using Symbolic Computation
  • Particular focus on: Program verification, inductive assertions, and polynomial invariants
  • Speaker: Laura Kovács (Vienna University of Technology)
  • Abstract: Verification of programs with loops and recursion requires auxiliary program assertions, such as loop invariants and formulas expressing ranking functions and loop iteration bounds.

    In this tutorial we discuss how such assertions can automatically be generated using symbolic computation algorithms and computational logic. To this end, we will first describe the notion of invariants, and present a program verification calculus based on Hoare logic. Next, we will translate the challenge of program assertion generation into a polynomial ideal problem. To this end, we will outline how the combination of symbolic summation, Groebner basis computation and cylindrical algebraic decomposition yields complex polynomial invariants and loop bounds over scalar loop variables. The method will be illustrated on concrete examples using the Aligator software tool.

• Tutorial 4: Invariant Generation using Theorem Proving
• Particular focus on: Quantified invariants, interpolants, and symbol elimination
• Speakers: Laura Kovács (Vienna University of Technology) and Andrei Voronkov (The University of Manchester)
• Abstract: Symbol elimination is a powerful technique to automatically generate quantified loop properties over unbounded data structures, such as array. It can also be regarded as an alternative approach to interpolation.

  In this tutorial we will present the symbol elimination technique and discuss its implementation in Vampire. To this end, we will overview new features of Vampire, including theory reasoning, consequence removal, colored proof generation, and interpolation. We will then present how symbol elimination can be used in applications of invariant generation and program analysis.