Workshop Progress in Decision Procedures: From Formalizations to Applications

Programme Participants Location Organisation Registration Photos

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

Book of Abstracts

Participants

Milan Banković, Matf, University of Belgrade, Serbia
Regis Blanc, EPFL, Switzerland
Jelena Čolić Oravec, FTN, University of Novi Sad, Serbia
Tihomir Gvero, EPFL, Switzerland
Mirjana Ivanović, DMI, University of Novi Sad, Serbia
Predrag Janičić, Matf, University of Belgrade, Serbia
Chantal Keller, Laboratoire d'Informatique de Polytechnique (LIX), Palaiseau, France
Etienne Kneuss, EPFL, Switzerland
Filip Konecny, EPFL, Switzerland
Damjan Krstajić, Research Centre for Cheminformatics, Serbia
Viktor Kuncak, EPFL, Switzerland
Ivan Kuraj, EPFL, Switzerland
Vladimir Kurbalija, DMI, University of Novi Sad, Serbia
Peter Lammich, TU Munich, Germany
Tatjana Lutovac, ETF, University of Belgrade, Serbia
Filip Marić, Matf, University of Belgrade, Serbia
Bojan Marinković, MI SANU, Serbia
Vesna Marinković, Matf, University of Belgrade, Serbia
Mladen Nikolić, Matf, University of Belgrade, Serbia
Filip Nikšić, MPI-SWS, Saarbrücken, Germany
Aljoša Obuljen, Microsoft Development Center, Belgrade, Serbia
Jovana Obradović FTN, University of Novi Sad, Serbia
Jovanka Pantović, FTN, University of Novi Sad, Serbia
Zoran Petrić, MI SANU, Serbia
Danijela Petrović, Matf, University of Belgrade, Serbia
Ivan Petrović, Matf, University of Belgrade, Serbia
Pedro Quaresma de Almeida, University of Coimbra, Portugal
Jovana Radenović, FTN, University of Novi Sad, Serbia
Enric Rodríguez Carbonell, Technical University of Catalonia (UPC), Barcelona, Spain
Andrijana Stamenković, FTN, University of Novi Sad, Serbia
Sana Stojanović, Matf, University of Belgrade, Serbia
Mirko Stojadinović, Matf, University of Belgrade, Serbia
Srđan Škrbić, DMI, University of Novi Sad, Serbia

Predrag Tanović, MI SANU, Serbia

Dmitriy Traytel, TU Munich, Germany
Milan Todorović, MI SANU, Serbia
Milena Vujošević-Janičić, Matf, University of Belgrade, Serbia
Aleksandar Zeljić, Uppsala University, Sweden
Dragiša Žunić, FIMEK, Novi Sad, 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

and

Lab for Automated Reasoning and Analysis
EPFL

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.