Invited lecture Programme Participants Location Organisation Registration Photos

COST Action IC0901 Working Group 1 and Working Group 2 Meeting
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


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.
10:00---10:15Opening Remarks
Invited Lecture
10:15---11:00Ralph-Johan Back (Åbo Akademi University, Turku, Finland):
 Invariant Based Programming slides
Goals of the COST Action IC0901
11:00---11:30 Viktor Kunčak (EPFL, Lausanne, Switzerland):
 Towards a Rich Model Toolkit slides
11:30---12:00 Coffee break
Session SAT Solving; Session Chair: Peter Schneider-Kamp
12:00---12:30Oliver Kullmann (Swansea University, United Kingdom):
 The OKlibrary, an Open-source Research Platform for SAT Solving (and Beyond) slides
12:30---13:00Mladen Nikolić (University of Belgrade, Serbia):
 A Methodology for Comparison and Ranking of SAT Solvers slides
13:00---14:30 Lunch break
Session SMT Solving; Session Chair: Paul Jackson
14:30---15:00Ružica Piskač (EPFL, Lausanne, Switzerland):
 Combining Theories with Shared Set Operations slides
15:00---15:30Philipp Ruemmer (Oxford University Computing Laboratory, United Kingdom):
 The SMT-LIB 2 Standard: Overview and Proposed New Theories slides
15:30---16:00Predrag Janičić and Filip Marić (University of Belgrade, Serbia):
 Uniform Reduction to SAT and SMT slides
16:00---16:30Coffee break
16:30---17:00Paul Jackson (University of Edinburgh, United Kingdom):
 Proving SPARK VCs with SMT solvers. Implications for the Rich Model Language slides
Session COST IC0901; Session Chair: Viktor Kunčak
17:00---18:00Rich Model Language: Panel Discussion
19:15---20:00Visit to the Retrospective Exhibition of Paja Jovanović
January 30, 2010.
Session Formal and Automated Theorem Proving; Session Chair: Filip Marić
09:30---10:00Sascha Boehme (TU Munich , Germany):
 Efficient Proof Reconstruction for the SMT Solver Z3 slides
10:00---10:30Florian Haftmann (TU Munich, Germany):
 Integrating Isabelle/HOL And Functional Programming -- Current Trends slides
10:30---11:00Marc Bezem (University of Bergen, Norway):
 Automating Coherent Logic slides
11:00---11:30Moa Johansson (University of Verona, Italy):
 Conjecture Synthesis for Inductive Theory Formation slides
11:30---12:00 Coffee break
Session Applications of Theorem Proving; Session Chair: Barbara Jobstmann
12:00---12:30Johannes Eriksson (Åbo Akademi University, Turku, Finland):
 Automatic Checking of Invariant Diagrams slides
12:30---13:00Filip Marić (University of Belgrade, Serbia):
 Automated Timetabling using a SAT Encoding slides
13:00---13:30Walther Neuper (Graz University of Technology, Austria):
 Program Languages with CTP Features? slides
13:30---15:00Lunch break
15:00---16:00Mini excursion: Knez Mihajlova Street and Kalemegdan
Session Logical Foundations; Session Chair: Silvia Ghilezan
16:00---16:30Stefan Ratschan (Academy of Sciences, Prague, Czech Republic):
 Deciding Non-linear Numerical Constraints: an Overview slides
16:30---17:00Philippe Suter (EPFL, Lausanne, Switzerland):
 Decision Procedures for Algebraic Data Types with Abstractions slides [ppsx]
17:00---17:30Coffee break
17:30---18:00Hugo Herbelin (INRIA - PPS, Paris, France):
 Intuitionistically Proving Markov's Principle Thanks to Delimited Control slides
18:00---18:30Jelena Ivetic (University of Novi Sad, Serbia):
 Intuitionistic Sequent-style Calculus with Explicit Structural Rules slides


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:

B92 Google maps

Little Belgrade City Guide for workshop participants

Information on Serbia


Hotel Palace
Toplicin venac 23
11000 Belgrade


The workshop is organized by
Automated Reasoning GrOup
Faculty of Mathematics
University of Belgrade


If you are interested in participating the workshop please contact Predrag Janicic.


A3 poster