Document Actions

Invited speakers

Andrei Voronkov

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

Lefteris Kirousis

University of Patras, Greece

Title: Coloring Random Graphs

Abstract: We will survey several recent results concerning the chromatic number of random graphs. The setting is as follows: We consider a probability space with graphs of a given average degree and n vertices. In the first case, (the Erdos-Renyi graphs), the probability space is uniform and comprises all graphs with the given average degree and n vertices. In the second case (regular graphs), the probability space is again uniform but the space comprises only graphs where all n vertices have the same degree (necessarily equal to the one given as average).

In both cases the chromatic number exhibits interesting threshold behavior: for a given average degree (given constant degree, for the regular case, respectively), the chromatic number of (asymptotically with n) almost all graphs lies within a common, small window of 1–3 integers. However
as the degree increases, at specific values, this window undergoes abrupt changes.

It is worth pointing out that the work in this area was partially motivated by theoretical, but mathematically non-rigorous results in Statistical Physics. Time permitting, this “physics connection” will also be outlined.

Helmut Veith

Technical University of Darmstadt, Germany

Title and abstract: Embedding Formal Methods into Systems Engineering

Tetsuo Ida

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.

James Davenport

University of Bath, UK

Title: The Sparsity Challenge

abstract: TBA

Sections

Personal tools

Document Actions

Invited speakers