---

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:

• 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

Book of Abstracts

February 4, 2011.
10:00---10:25	Registration
10:25---10:30	Opening 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
11:30---12:00	Coffee break
12:00---12:30	Hugo Herbelin (INRIA | PPS, Paris, France):
	An Excursion Into the Proofs-as-programs Correspondence
12:30---13:00	Dejan Ničković (Institute of Science and Technology, Austria):
	From MTL to Deterministic Timed Automata
13:00---13:30	Bojan Marinković: (Mathematical Institute, Belgrade, Serbia):
	Formal Description of the Chord Protocol using ASM
13:30---15:00	Lunch break (Restaurant "Ljubić")
Formal Theorem Proving and Applications; Session Chair: Dejan Ničković
15:00---15:30	Marko Maliković: (University of Rijeka, Croatia):
	Automated Reasoning about Retrograde Chess Problems using Coq
15:30---16:00	Petar Maksimović: (Mathematical Institute, Belgrade, Serbia):
	Formal Verication of Key Properties for Several Probability Logics in the Proof Assistant Coq
16:00---16:30	Coffee break
16:30---17:00	Walther Neuper (Graz University of Technology, Austria):
	Geometry Construction Languages Guiding User-interaction via a Lucas-Interpreter
17:00---17:30	Filip Marić (University of Belgrade, Serbia):
	Verified Efficient Unsatisability Proof Checking for SAT
19:30---22:00	Dinner at "Teatroteka"

February 5, 2011.
Automated Theorem Proving and Applications; Session Chair: Filip Marić
10:00---10:30	Oliver Kullman (Swansea University, United Kingdom):
	How to Translate into SAT such that SAT Solvers Have a Good Time?!?
10:30---11:00	Tihomir Gvero (EPFL, Lausanne, Switzerland):
	Interactive Synthesis of Code Snippets
11:00---11:30	Coffee break
11:30---12:00	Milan Banković (University of Belgrade, Serbia):
	ArgoSMTExpression: SMT-LIB 2.0 Compliant Expression Library
12:00---12:30	Milena Vujošević-Janičić (University of Belgrade, Serbia):
	A New Verification Tool: From LLVM Code to SMT Formulae
12:30---13:00	Mladen Nikolić (University of Belgrade, Serbia):
	ArgoCaLyPso - SAT Inspired Coherent Logic Prover
13:00---14:30	Lunch break (Restaurant "Ljubić")
Applications; Session Chair: Predrag Janičić
14:30---15:00	Stevan Kordić and Nataša Kovač (University of Montenegro, Montenegro):
	One Combinatorial Algorithm for Berth Allocation Problem
15:00---15:30	MDCS Math team (Microsoft Development Center Serbia, Serbia):
	Some Recent Developments in MDCS
15:30---16:00	Coffee break
Early Stage Work; Session Chair: Predrag Janičić
16:00---16:15	Vesna Pavlović (University of Belgrade, Serbia):
	Solving Geometric Construction Problems
16:15---16:30	Danijela Petrović (University of Belgrade, Serbia):
	Automated Proving in Geometry using Grobner bases in Isabelle/HOL
16:30---16:45	Ivan Petrović (University of Belgrade, Serbia):
	Java Implementation of Wu's Method for Automated Theorem Proving in Geometry
16:45---17:00	Mirko Stojadinović (University of Belgrade, Serbia):
	How Efficient Can Fully Veried Functional Programs be? --- a Case Study of Graph Traversal Algorithms
17:00---17:15	Mirko Spasić (University of Belgrade, Serbia):
	Formalizing Simplex within Isabelle/HOL
17:15---17:30	Aleksandar Zeljić (University of Belgrade, Serbia):
	Solving Some NP-complete Problems Instances by Reductions
18:30---19:30	Mini guided tour: Knez Mihajlova Street
19:30---22:00	Dinner at Skadarlija (Restauraunt "Zlatni Bokal")

Participants

• Marija Acimovic, Microsoft Development Center Serbia, Serbia
• Milan Bankovic, University of Belgrade, Serbia
• Silvia Ghilezan, University of Novi Sad, Serbia
• Tihomir Gvero, EPFL, Lausanne, Switzerland
• Hugo Herbelin, INRIA- PPS, Paris, France
• Svetlana Jaksic, University of Novi Sad, Serbia
• Predrag Janicic, University of Belgrade, Serbia
• Oliver Kullmann, Swansea University, UK
• Stevan Kordic, University of Montenegro, Montenegro
• Petar Maksimovic, Mathematical Institute, Belgrade, Serbia
• Oded Maler, CNRS/Verimag, France
• Marko Malikovic, University of Rijeka, Croatia
• Filip Maric, University of Belgrade, Serbia
• Bojan Marinkovic, Mathematical Institute, Belgrade, Serbia
• Walther Neuper, Graz University of Technology, Austria
• Dejan Nickovic, Institute of Science and Technology (IST), Austria
• Mladen Nikolic, University of Belgrade, Serbia
• Jovanka Pantovic, University of Novi Sad, Serbia
• Vesna Pavlovic, University of Belgrade, Serbia
• Danijela Petrovic, University of Belgrade, Serbia
• Ivan Petrovic, University of Belgrade, Serbia
• Nina Radojicic, University of Belgrade, Serbia
• 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, University of 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.