Invited lectures Location Organisation Registration Programme Participants Photos

Second Workshop on Formal and Automated Theorem Proving and Applications (Jan 30-Jan 31, 2009, Belgrade)

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 First Workshop on Formal Theorem Proving and Applications is here.

Invited lectures

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


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.

Workshop programme

The workshop programme and book of abstracts

January 30, 2008.
10:00-10:05 Openning
Formal Theorem Proving
10:05-10:50 Makarius Wenzel (TU Munich): Pure Logical Reasoning in Isabelle/Isar slides
11:00-11:45 Hugo Herbelin (INRIA, Ecole polytechnique, Paris): Validating Decision Procedures for Coq in Coq slides
12:00-12:45 Filip Marić (University of Belgrade): Formalization of SAT Solvers slides
13:00-14.30 Lunch break
Logical foundations
14:30-15:15 Silvia Ghilezan (University of Novi Sad): Computational Interpretations of Logic slides
15:30-15:55 Alexis Saurin (Ecole Normale Suprieure, Paris): An Interactive Foundation for Computation as Proof-Search slides
15:55-16:20 Jovanka Pantović (University of Novi Sad): Web data modelling and security slides
16:30-16:55 Dragiša Žunić, Pierre Lescanne (Ecole Normale Superieure de Lyon, France): Diagrammatic Reasoning in Classical Logic
16:55-17:20 Dragan Doder (University of Belgrade), Bojan Marinković, Petar Maksimović (Mathematical Institute, Belgrade), Aleksandar Perović (University of Belgrade): A Logic with a Conditional Probability Operator slides


January 31, 2008.
Formal Theorem Proving
10:05-10:50 Florian Haftmann (TU Munich): Functional Programming with Isabelle/HOL slides
11:00-11:25 Vesna Pavlović, (University of Belgrade): XML suite for Isar slides
11:25-11:50 Sana Stojanović, Vesna Pavlović, Predrag Janičić (University of Belgrade): Formalization and Automation of Euclidean Geometry slides
12:00-12:45 Walther Neuper (TU Graz): Educational Tools as Interactive Models of Mathematics slides
13:00-14.30 Lunch break
SAT and SMT Solving and Applications
14:30-15:15 Viktor Kunčak (EPF, Lausanne): Automated Reasoning for Reliable Software slides
15:30-15:55 Mladen Nikolić, Filip Marić, Predrag Janičić (University of Belgrade): Instance-based Selection of Strategies for SAT Solvers slides
15:55-16:20 Milan Šešum, Predrag Janičić (University of Belgrade): Uniform Reduction of Cryptographic Problems to SAT slides
16:30-16:55 Milan Banković, Filip Marić (University of Belgrade): An SMT Solver For the Theory All-different slides
16:55-17:20 Milena Vujošević Janičić (University of Belgrade): Using SMT Solver in Detection of Buffer Overflow Bugs slides