COST IC0901 WG1 and WG2 Meeting and Third Workshop on Formal and Automated Theorem Proving

Invited lecture Programme Participants Location Organisation Registration Photos

COST Action IC0901 Working Group 1 and Working Group 2 Meeting
and
Third Workshop on Formal and Automated Theorem Proving and Applications
January 29-30, 2010, Belgrade, Serbia

The workshop will mainly address the topics in formal and automated theorem proving, especially concerning SAT/SMT solvers and their applications.

The web page of the COST Action IC0901 is here.

The web page of the Second Workshop on Formal Theorem Proving and Applications is here.

The web page of the First Workshop on Formal Theorem Proving and Applications is here.

Invited Lecture

Ralph-Johan Back (Abo Akademi University, Turku, Finland)

Title: Invariant based programming

Abstract:

Invariant based programming is an approach to constructing programs where the basic program situations (pre- and postconditions and intermediate (loop) invariants) are identified and formalized before we connect these situations with executable transitions. The program is built in a stepwise manner, each step adding (or deleting or changing) either a situation or a transition between situations. We continuously check that each step preserves the correctness of the program built this far. Invariant based programming is now taught in introductory programming courses in our university, and seems to provide a simple and intuitive method for introducing formal methods and correctness concerns early on in the programming education. Invariant based programming is carried out within a visual formalism that we call invariant diagrams. All the information needed for checking program correctness is directly displayed in the diagram. This means that correctness can be checked directly by analysing the diagram, without the need for learning complicated programming logic proof rules.

The talk will describe the basic idea of invariant based programming and exemplify the approach with a simple example. We will identify the proof obligations that together establish the correctness of the constructed program, and explain the central role that automatic verification of these proof conditions (using SMT solvers) plays. We describe the basic workflow of invariant based programming, and our experiences from teaching this approach to both experienced programmers and to first year CS students.

Workshop programme

Book of Abstracts and Discussions with Workshop programme

January 29, 2010.
09:30---10:00	Registration
10:00---10:15	Opening Remarks
Invited Lecture
10:15---11:00	Ralph-Johan Back (Åbo Akademi University, Turku, Finland):
	Invariant Based Programming
Goals of the COST Action IC0901
11:00---11:30	Viktor Kunčak (EPFL, Lausanne, Switzerland):
	Towards a Rich Model Toolkit
11:30---12:00	Coffee break
Session SAT Solving; Session Chair: Peter Schneider-Kamp
12:00---12:30	Oliver Kullmann (Swansea University, United Kingdom):
	The OKlibrary, an Open-source Research Platform for SAT Solving (and Beyond)
12:30---13:00	Mladen Nikolić (University of Belgrade, Serbia):
	A Methodology for Comparison and Ranking of SAT Solvers
13:00---14:30	Lunch break
Session SMT Solving; Session Chair: Paul Jackson
14:30---15:00	Ružica Piskač (EPFL, Lausanne, Switzerland):
	Combining Theories with Shared Set Operations
15:00---15:30	Philipp Ruemmer (Oxford University Computing Laboratory, United Kingdom):
	The SMT-LIB 2 Standard: Overview and Proposed New Theories
15:30---16:00	Predrag Janičić and Filip Marić (University of Belgrade, Serbia):
	Uniform Reduction to SAT and SMT
16:00---16:30	Coffee break
16:30---17:00	Paul Jackson (University of Edinburgh, United Kingdom):
	Proving SPARK VCs with SMT solvers. Implications for the Rich Model Language
Session COST IC0901; Session Chair: Viktor Kunčak
17:00---18:00	Rich Model Language: Panel Discussion
19:15---20:00	Visit to the Retrospective Exhibition of Paja Jovanović
20:00---22:30	Dinner

January 30, 2010.
Session Formal and Automated Theorem Proving; Session Chair: Filip Marić
09:30---10:00	Sascha Boehme (TU Munich , Germany):
	Efficient Proof Reconstruction for the SMT Solver Z3
10:00---10:30	Florian Haftmann (TU Munich, Germany):
	Integrating Isabelle/HOL And Functional Programming -- Current Trends
10:30---11:00	Marc Bezem (University of Bergen, Norway):
	Automating Coherent Logic
11:00---11:30	Moa Johansson (University of Verona, Italy):
	Conjecture Synthesis for Inductive Theory Formation
11:30---12:00	Coffee break
Session Applications of Theorem Proving; Session Chair: Barbara Jobstmann
12:00---12:30	Johannes Eriksson (Åbo Akademi University, Turku, Finland):
	Automatic Checking of Invariant Diagrams
12:30---13:00	Filip Marić (University of Belgrade, Serbia):
	Automated Timetabling using a SAT Encoding
13:00---13:30	Walther Neuper (Graz University of Technology, Austria):
	Program Languages with CTP Features?
13:30---15:00	Lunch break
15:00---16:00	Mini excursion: Knez Mihajlova Street and Kalemegdan
Session Logical Foundations; Session Chair: Silvia Ghilezan
16:00---16:30	Stefan Ratschan (Academy of Sciences, Prague, Czech Republic):
	Deciding Non-linear Numerical Constraints: an Overview
16:30---17:00	Philippe Suter (EPFL, Lausanne, Switzerland):
	Decision Procedures for Algebraic Data Types with Abstractions [ppsx]
17:00---17:30	Coffee break
17:30---18:00	Hugo Herbelin (INRIA - PPS, Paris, France):
	Intuitionistically Proving Markov's Principle Thanks to Delimited Control
18:00---18:30	Jelena Ivetic (University of Novi Sad, Serbia):
	Intuitionistic Sequent-style Calculus with Explicit Structural Rules
19:45---22:30	Dinner

Participants

Ralph-Johan Back, Abo Akademi University, Turku, Finland
Milan Bankovic, University of Belgrade, Serbia
Marc Bezem, University of Bergen, Norway [COST Action MC Member]
Sascha Boehme, TU Munich, Germany [COST Action WG Member]
Johannes Eriksson, Abo Akademi University, Turku, Finland
Silvia Ghilezan, University of Novi Sad, Serbia [COST Action MC Member]
Florian Haftmann, TU Munich, Germany [COST Action WG Member]
Hugo Herbelin, INRIA- PPS, Paris, France
Jelena Ivetic, University of Novi Sad, Serbia
Paul Jackson, University of Edinburgh, UK [COST Action MC Member, WG1 Deputy Chair]
Svetlana Jaksic, University of Novi Sad, Serbia
Predrag Janicic, University of Belgrade, Serbia [COST Action MC Member]
Barbara Jobstmann, CNRS/Verimag, Gieres, France [COST Action MC Member]
Moa Johansson, University of Verona, Italy [COST Action WG Member]
Oliver Kullmann, Swansea University, UK
Viktor Kuncak, EPFL, Lausanne, Switzerland [COST Action Chair]
Petar Maksimovic, Mathematical Institute, Belgrade, Serbia
Filip Maric, University of Belgrade, Serbia
Bojan Marinkovic, Mathematical Institute, Belgrade, Serbia
Walther Neuper, Graz University of Technology, Austria
Mladen Nikolic, University of Belgrade, Serbia
Jovanka Pantovic, University of Novi Sad, Serbia
Vesna Pavlovic, University of Belgrade, Serbia
Danijela Petrovic, University of Belgrade, Serbia
Ruzica Piskac, EPFL, Lausanne, Switzerland
Miroslav Popovic, University of Novi Sad, Serbia
Stefan Ratschan, Academy of Sciences of the Czech Republic, Prague, Czech Republic [COST Action MC Member]
Alexis Saurin, INRIA - PPS, Paris, France
Peter Schneider-Kamp, University of Southern Denmark, Odense, Denmark [COST Action MC Member Substitute]
Mirko Stojadinovic, University of Belgrade, Serbia
Sana Stojanovic, University of Belgrade, Serbia
Philippe Suter, EPFL, Lausanne, Switzerland
Philipp Ruemmer, University of Oxford, UK [COST Action MC Member Substitute]
Milena Vujosevic-Janicic, University of Belgrade, Serbia
Dragisa Zunic, University of Novi Sad, Serbia

Workshop Location

The workhsop will be located at:
Faculty of Mathematics, University of Belgrade,
Studentski Trg 16,
11000 Belgrade.
All lectures will be held at room 718, on the fourth floor.

Online maps of Belgrade: