University of Manchester, UK
Title: Finding loop invariants using a theorem prover
Abstract: To make software verification easier, one needs to automate finding loop invariants. Loop invariant discovery is a very hardand creative problem. We show how one can find complex invariants for loops over arrays using a combination of two ideas:
(1) Finding invariants over integer variables using computer algebra methods
(2) Finding array loop invariants using symbol elimination performed by a theorem prover
University of Patras, Greece
Title: Coloring Random Graphs
as the degree increases, at specific values, this window undergoes abrupt changes.
Technical University of Darmstadt, Germany
Title and abstract: Embedding Formal Methods into Systems Engineering
University of Tsukuba, Japan
Title: A Compiler for Origami Construction and Verification
Abstract: The talk is about the computer assisted construction of simple geometrical objects . I mainly discuss the construction of geometrical objects by means of origami, but the methodology will be applicable to other means of constructions.
Our observation to begin with is that the prescription of construction of geometrical objects is in essence programming. Hence we are in need of a kind of programming language and a computation model that it is based on. We do have a rudimentary, in the sense of computer science, language and a logical framework that date back to the end of 1980s or even to 300 BC. The former is Huzita’s origami basic operations sometimes referred to as Huzita’s axioms and the latter is Geometrical Elements of Euclid.
Given such a language and a prescription of the construction written in that language, we are interested in executing the prescription. The execution consists of the construction of a model inside a computer, the visualization of the model in a way similar to what we see and manipulate using some material and construction tools, and the verification of the correctness of the construction with regards to the specification. In the case of origami, the material is a sheet of paper and the tools are our hands.
The assistance that we have developed for this purpose is very similar in its role to compilers of programming languages. We compile the prescription, i.e. program, to executable codes that are then interpreted by a computer. The result is displayed on the screen of the computer. Our language is based on a fragment of the first-order predicate logic with the domain of interpretation in R^3. The program is compiled first into existentially quantified formulas and then into a set of polynomials. The set of polynomials is solved using the Groebner basis method and/or the cylindrical algebraic composition for the existential variables. The model that embodies the solution is the result of the execution of the program. Moreover, the set of polynomials are used for proving the correctness of the construction.
As in the usual compilers, we perform optimizations to produce more efficient codes. The necessity of the optimization is more for the verification than for the construction. We use several geometrical laws as well as algebraic laws for the polynomial simplifications.
The compiler has been implemented and improved for some years and is a core of our Eos (e-origami system). The talk is combination of the explanation of the outline of the compiler as well as the demo of Eos.
University of Bath, UK
Title: The Sparsity Challenge