Programme Participants Location Organisation Registration Photos

Progress in Decision Procedures: From Formalizations to Applications
March 30, 2013, Belgrade, Serbia

Supported by SNF SCOPES IZ73Z0_127979 research grant.

The workshop addresses a wide range of aspects of formal and automated theorem proving, but with a special emphasis on decision procedures, SAT/SMT, decision procedures in geometry, and their applications.

The workshop marks the end of succesful bilateral joint research grant SNF SCOPES IZ73Z0_127979 between LARA group from EPFL and ARGO group from University of Belgrade.

There is no formal submission procedure and there are no proceedings. We believe that the atmosphere at the workshop will be relaxed and friendly, but in the same time highly inspiring and productive.

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, March 29, 2013.
17:15---18:00Meeting at the Hotel Palace
18:00---19:30Guided Walking Tour
19:30---22:00Dinner (Restaurant "Kalemegdanska terasa")
Saturday, March 30, 2013.
09:45---09:50 Opening Remarks
Session: Overview Talks; Session Chair: Predrag Janičić
09:50---10:15 Filip Marić (MatF, University of Belgrade, Serbia):
 Overview of Research Activities of the ARGO Group over the Last Three Years slides
10:15---10:40Viktor Kuncak (EPFL, Switzerland):
 Implicit Programming: An Overview slides
10:40---11:00Coffee break
Session: Satisfiability Modulo Theories; Session Chair: Predrag Janičić
11:00---11:25Enric Rodriguez Carbonell (Technical University of Catalonia (UPC), Spain):
 Non-Linear Arithmetic Solving for Termination Analysis slides
11:25---11:40Aleksandar Zeljić (Uppsala University, Sweden):
 Towards SMT Style Reasoning about Floating-Point Arithmetic slides
11:40---12:00Coffee break
Session: Decision Procedures and Interactive Theorem Proving; Session Chair: Predrag Janičić
12:00---12:25Chantal Keller (LIX, Palaiseau, France):
 SMTCoq: Cooperation Between SAT/SMT Solvers and the Coq Proof Assistant through Proof Witnesses slides
12:25---12:50Dmitriy Traytel (TU-Munich, Germany):
 A Verified Decision Procedure for MSO on Words Based on Derivatives of Regular Expressions slides
12:50---14:50 Lunch break (Restaurant: "Jevrem")
Session: Decisions in Applications; Session Chair: Predrag Janičić
14:50---15:15Aljosa Obuljen (Microsoft Development Center, Serbia):
 Overview of Microsoft Development Center Serbia - Deliverables and Focus Areas slides
15:15---15:40Vladimir Kurbalija (DM, University of Novi Sad, Serbia):
 Analysis of Constrained Time-Series Similarity Measures slides
15:40---16:00Coffee break
Session: Dealing with Proofs I; Session Chair: Filip Marić
16:00---16:25Peter Lammich (TU-Munich, Germany):
 The Isabelle Refinement Framework slides
16:25---16:50Pedro Quaresma (University of Coimbra, Portugal):
 The Web Geometry Laboratory Project (Intelligent Geometric Tools) slides
16:50---17:10Coffee break
Session: Dealing with Proofs II; Session Chair: Filip Marić
17:10---17:35Tatjana Lutovac (ETF, University of Belgrade, Serbia):
 A Syntax Approach to Automated Detection of Some Redundancies in Linear Logic Sequent Derivations slides
17:35---17:50Jelena Čolić Oravec (FTN U Novi Sad, Serbia):
 Incompletely Specified Operations and Their Clones slides
17:50---18:10Coffee break
Session: Software Verification; Session Chair: Filip Marić
18:10---18:25Filip Nikšić (MPI-SWS, Saarbrücken, Germany):
 Incremental, Inductive Coverability slides
18:25---18:40Filip Konecny (EPFL, Switzerland):
 Underapproximation of Procedure Summaries for Integer Programs slides
18:40---18:55Regis Blank (EPFL, Switzerland):
 Verifying Functional Scala Programs in Leon slides
18:55---19:10Milena Vujošević-Janičić (MatF, University of Belgrade, Serbia):
 System LAV and its Applications slides
19:10---19:15Closing Remarks
20:00---23:00Dinner (Restaurant "Teatroteka")

Book of Abstracts


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

Information on Serbia


Hotel Palace
Toplicin venac 23
11000 Belgrade


The workshop is organized by:

Automated Reasoning GrOup
Faculty of Mathematics
University of Belgrade


Lab for Automated Reasoning and Analysis


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.