Programme Participants Location Organisation Registration Photos

Fourth Workshop on Formal and Automated Theorem Proving and Applications
February 4-5, 2011, Belgrade, Serbia

The workshop addresses all aspects of formal and automated theorem proving, but with a special emphasis on SAT/SMT, geometry reasoning and their applications.

The workshop will follow the tradition of three successful workshops:

Over the last years, the atmosphere at the workshop was relaxed and friendly, but in the same time highly inspiring and productive. There is no formal submission procedure and there are no proceedings.

Please consider participating at the workshop (with or without a talk) and please inform about the workshop your colleagues that might be interested in participating.

Workshop programme

Book of Abstracts

February 4, 2011.
10:25---10:30Opening Remarks
Theoretical Computer Science; Session Chair: Silvia Ghilezan
10:30---11:30 Oded Maler (CNRS/Verimag, France):
 The Potential Roles of Informatics in Systems Biology slides
11:30---12:00 Coffee break
12:00---12:30 Hugo Herbelin (INRIA | PPS, Paris, France):
 An Excursion Into the Proofs-as-programs Correspondence slides
12:30---13:00Dejan Ničković (Institute of Science and Technology, Austria):
 From MTL to Deterministic Timed Automata slides
13:00---13:30Bojan Marinković: (Mathematical Institute, Belgrade, Serbia):
 Formal Description of the Chord Protocol using ASM slides
13:30---15:00 Lunch break (Restaurant "Ljubić")
Formal Theorem Proving and Applications; Session Chair: Dejan Ničković
15:00---15:30Marko Maliković: (University of Rijeka, Croatia):
 Automated Reasoning about Retrograde Chess Problems using Coq slides
15:30---16:00Petar Maksimović: (Mathematical Institute, Belgrade, Serbia):
 Formal Verication of Key Properties for Several Probability Logics in the Proof Assistant Coq slides
16:00---16:30Coffee break
16:30---17:00Walther Neuper (Graz University of Technology, Austria):
 Geometry Construction Languages Guiding User-interaction via a Lucas-Interpreter slides
17:00---17:30Filip Marić (University of Belgrade, Serbia):
 Verified Efficient Unsatisability Proof Checking for SAT slides
19:30---22:00Dinner at "Teatroteka"
February 5, 2011.
Automated Theorem Proving and Applications; Session Chair: Filip Marić
10:00---10:30Oliver Kullman (Swansea University, United Kingdom):
 How to Translate into SAT such that SAT Solvers Have a Good Time?!? slides
10:30---11:00Tihomir Gvero (EPFL, Lausanne, Switzerland):
 Interactive Synthesis of Code Snippets slides
11:00---11:30Coffee break
11:30---12:00Milan Banković (University of Belgrade, Serbia):
 ArgoSMTExpression: SMT-LIB 2.0 Compliant Expression Library slides
12:00---12:30Milena Vujošević-Janičić (University of Belgrade, Serbia):
 A New Verification Tool: From LLVM Code to SMT Formulae slides
12:30---13:00Mladen Nikolić (University of Belgrade, Serbia):
 ArgoCaLyPso - SAT Inspired Coherent Logic Prover slides
13:00---14:30 Lunch break (Restaurant "Ljubić")
Applications; Session Chair: Predrag Janičić
14:30---15:00Stevan Kordić and Nataša Kovač (University of Montenegro, Montenegro):
 One Combinatorial Algorithm for Berth Allocation Problem slides
15:00---15:30MDCS Math team (Microsoft Development Center Serbia, Serbia):
 Some Recent Developments in MDCS slides
15:30---16:00Coffee break
Early Stage Work; Session Chair: Predrag Janičić
16:00---16:15Vesna Pavlović (University of Belgrade, Serbia):
 Solving Geometric Construction Problems slides
16:15---16:30Danijela Petrović (University of Belgrade, Serbia):
 Automated Proving in Geometry using Grobner bases in Isabelle/HOL slides
16:30---16:45Ivan Petrović (University of Belgrade, Serbia):
 Java Implementation of Wu's Method for Automated Theorem Proving in Geometry slides
16:45---17:00Mirko Stojadinović (University of Belgrade, Serbia):
 How Efficient Can Fully Veried Functional Programs be? --- a Case Study of Graph Traversal Algorithms slides
17:00---17:15Mirko Spasić (University of Belgrade, Serbia):
 Formalizing Simplex within Isabelle/HOL slides
17:15---17:30Aleksandar Zeljić (University of Belgrade, Serbia):
 Solving Some NP-complete Problems Instances by Reductions slides
18:30---19:30Mini guided tour: Knez Mihajlova Street
19:30---22:00Dinner at Skadarlija (Restauraunt "Zlatni Bokal")


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

Information on Serbia


Hotel Palace
Toplicin venac 23
11000 Belgrade


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


There is no a formal registration procedure and there is no conference fee. If you are interested in participating the workshop please contact Predrag Janicic.