Institute for Computer Languages
Compilers and Languages Group
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.
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.
The tutorial will be of 2 days and will take place between 27-28 September, during the SYNASC 2011 conference.
The tutorial will comprise of four sessions, as follows:
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.
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.
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.
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.