Programme Participants Location Organisation Registration Photos

Fifth Workshop on Formal and Automated Theorem Proving and Applications
February 3-4, 2012, 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 four 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

Friday, February 3, 2012.
09:55--10:00Opening Remarks
Session: SAT and SMT; Session Chair: Filip Marić
10:00---10:30 Oliver Kullmann (Swansea University, United Kingdom):
 Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads slides
10:30---11:00Philipp Rümmer (University of Uppsala, Sweden)
 E-Matching with Free Variables slides
11:00---11:30Coffee break
11:30---12:00Mladen Nikolić (University of Belgrade, Serbia):
 CDCL-Based Abstract State Transition System for Coherent Logic slides
12:00---12:15Milan Banković (University of Belgrade, Serbia):
 pArgoSAT – Parallelization of Boolean Constraint Propagation in DPLL-based SAT solvers slides
12:15---12:30Aleksandar Zeljić (University of Belgrade, Serbia):
 Instance Features for Non CNF Solver Portfolios slides
12:30---15:00 Lunch break (Restaurant "Teatroteka")
Session: Formal theorem proving; Session Chair: Predrag Janičić
15.00---15.30Hugo Herbelin (INRIA — PPS, Paris, France):
 An enumeration-free proof of Gödel's completeness theorem with side effect slides
15.30---15.45Petar Maksimović (Mathematical Institute, Belgrade, Serbia):
 A Logical Framework with External Predicates slides
15:45---16:15Coffee break
16.15---16.45Marko Maliković (University of Rijeka, Croatia):
 Formal Analysis of Correctness of a Strategy for the KRK Chess Endgame slides
16.45---17.15Filip Marić (University of Belgrade, Serbia):
 Formalized Search for FC Families within Isabelle/HOL slides
17:15---19:00Informal discussions and individual meetings
19:30---22:00Dinner (Restaurant "Klub Književnika")
Saturday, February 4, 2012.
Session: Geometry reasoning; Session Chair: Filip Marić
10:00---10:30 Julien Narboux (University of Strasbourg, France):
 Formalization of Simple Wu’s Method in Coq slides
10:30---11:00Pascal Schreck (University of Strasbourg, France):
 Geometric Constructions and First Order Logic slides
11:00---11:30Coffee break
11:30---11:45Predrag Janičić (University of Belgrade, Serbia):
 Automated Solving of Triangle Construction Problems slides
11:45---12:00Sana Stojanović (University of Belgrade, Serbia):
 Exploiting symmetries and axiom reformulation in automated generation of formal proofs slides
12:00---12:15Ivan Petrović (University of Belgrade, Serbia):
 Integration of OpenGeoProver with GeoGebra slides
12:30---15:00 Lunch break (Restaurant "Teatroteka")
Session: Applications of Theorem Proving; Session Chair: Predrag Janičić
15.00---15.30Walther Neuper (Graz University of Technology, Austria):
 How Theorem-Prover Technology Advances Educational Math Software — Lessons Learned from Preparation of a Grant Proposal slides
15.30---15.45Milena Vujošević-Janičić (University of Belgrade, Serbia):
 Automated Evaluation of Students' Programs: Testing, Verification and Similarity slides
15:45---16:15Coffee break
16.15---16.30Mladen Nikolić (University of Belgrade, Serbia):
 Program Similarity Measurement for Evaluation of Students' Programs slides
16.30---16.45Mirko Stojadinović (University of Belgrade, Serbia):
 Reduction of finite linear CSPs to SAT using different encodings slides
16:45---19:00Informal discussions and individual meetings
19:30---22:30Dinner (Restaurant "Little Bay")

Book of Abstracts


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.