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.
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.
Book of Abstracts and Discussions with Workshop programme
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 |
The workhsop will be located at: Online maps of Belgrade: |
Little Belgrade City Guide for workshop participants
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.