Invited lectures Location Organisation Registration Programme Participants Photos
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.
|
The workhsop will be located at: Online maps of Belgrade:
|
|
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.
The workshop programme and book of abstracts
| January 30, 2008. | |
|---|---|
| 10:00-10:05 | Openning |
| Session: Formal Theorem Proving | |
| 10:05-10:50 | Makarius Wenzel (TU Munich):
Pure Logical Reasoning in Isabelle/Isar
|
| 11:00-11:45 | Hugo Herbelin (INRIA, Ecole polytechnique, Paris):
Validating Decision Procedures for Coq in Coq
|
| 12:00-12:45 | Filip Marić (University of Belgrade): Formalization of SAT Solvers
|
| 13:00-14.30 | Lunch break |
| Session: Logical foundations | |
| 14:30-15:15 | Silvia Ghilezan (University of Novi Sad):
Computational Interpretations of Logic
|
| 15:30-15:55 | Alexis Saurin (Ecole Normale Suprieure, Paris):
An Interactive Foundation for Computation as Proof-Search
|
| 15:55-16:20 | Jovanka Pantović (University of Novi Sad):
Web data modelling and security
|
| 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
|
| January 31, 2008. | |
|---|---|
| Session: Formal Theorem Proving | |
| 10:05-10:50 | Florian Haftmann (TU Munich):
Functional Programming with Isabelle/HOL
|
| 11:00-11:25 | Vesna Pavlović,
(University of Belgrade):
XML suite for Isar
|
| 11:25-11:50 | Sana Stojanović,
Vesna Pavlović,
Predrag Janičić (University of Belgrade):
Formalization and Automation of Euclidean Geometry
|
| 12:00-12:45 | Walther Neuper (TU Graz):
Educational Tools as Interactive Models of Mathematics
|
| 13:00-14.30 | Lunch break |
| Session: SAT and SMT Solving and Applications | |
| 14:30-15:15 | Viktor Kunčak (EPF, Lausanne):
Automated Reasoning for Reliable Software
|
| 15:30-15:55 | Mladen Nikolić,
Filip Marić,
Predrag Janičić (University of Belgrade):
Instance-based Selection of Strategies for SAT Solvers
|
| 15:55-16:20 | Milan Šešum,
Predrag Janičić (University of Belgrade):
Uniform Reduction of Cryptographic Problems to SAT
|
| 16:30-16:55 | Milan Banković,
Filip Marić (University of Belgrade):
An SMT Solver For the Theory All-different
|
| 16:55-17:20 | Milena Vujošević Janičić
(University of Belgrade):
Using SMT Solver in Detection of Buffer Overflow Bugs
|
