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:
|
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:
|
|
| January 30, 2008. | |
|---|---|
| Session Formal Theorem Proving and Isabelle | |
| 10:00-10:05 | Openning |
| 10:05-10:50 | Makarius Wenzel (TU Munich): Pure Logical Reasoning in Isabelle/Isar |
| 11:00-11:45 | Hugo Herbelin (INRIA, Ecole polytechnique, Paris): Coq System |
| 12:00-12:45 | Filip Marić (University of Belgrade): Formalization of SAT Solvers |
| 13:00-14.30 | Lunch break |
| Session Logical foundations | |
| 16:00-16:45 | Silvia Ghilezan (University of Novi Sad): Computational Interpretations of Logic |
| 16:45-17:05 | Jovanka Pantović (University of Novi Sad): Web data modelling and security |
| January 31, 2008. | |
|---|---|
| Session Formal Theorem Proving and Isabelle | |
| 10:05-10:50 | Florian Haftmann (TU Munich): Functional Programming with Isabelle/HOL |
| 11:00-11:25 | Vesna Pavlović,
Dušan Tošić (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): Setting Suitable Parameters' Values of 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ć,
Dušan Tošić (University of Belgrade): Using SMT Solver in Detection of Buffer Overflow Bugs |