---

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:

• The Fourth Workshop on Formal Theorem Proving and Applications.
• The Third Workshop on Formal Theorem Proving and Applications.
• The Second Workshop on Formal Theorem Proving and Applications.
• The First Workshop on Formal Theorem Proving and Applications.

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

Book of Abstracts

Participants

• Milan Bankovic, University of Belgrade, Serbia
• Jelena Colic, University of Novi Sad, Serbia
• Silvia Ghilezan, University of Novi Sad, Serbia
• Hugo Herbelin, INRIA- PPS, Paris, France
• Predrag Janicic, University of Belgrade, Serbia
• Oliver Kullmann, Swansea University, UK
• Petar Maksimovic, Mathematical Institute, Belgrade, Serbia
• Marko Malikovic, University of Rijeka, Croatia
• Filip Maric, University of Belgrade, Serbia
• Julien Narboux, University of Strasbourg, France
• Walther Neuper, Graz University of Technology, Austria
• Mladen Nikolic, University of Belgrade, Serbia
• Zoran Petric, Mathematical Institute, Belgrade, Serbia
• Danijela Petrovic, University of Belgrade, Serbia
• Ivan Petrovic, University of Belgrade, Serbia
• Nina Radojicic, University of Belgrade, Serbia
• Philipp Ruemmer, Uppsala University, Sweden
• Pascal Schreck, University of Strasbourg, France
• Ana Spasic, University of Belgrade, Serbia
• Mirko Spasic, University of Belgrade, Serbia
• Mirko Stojadinovic, University of Belgrade, Serbia
• Sana Stojanovic, University of Belgrade, Serbia
• Milan Todorovic, University of Belgrade, Serbia
• Milena Vujosevic-Janicic, University of Belgrade, Serbia
• Aleksandar Zeljic, Mathematical Institute, Belgrade, 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:

Information on Serbia

Accommodation

Hotel Palace
Toplicin venac 23
11000 Belgrade

Organisation

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

Registration

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.