LZI - Schloss Dagstuhl - Talks + Materials of Seminar 11272

Seminar 11272
Decision Procedures in Soft, Hard and Bio-ware - Follow Up

Nikolaj Bjorner (Microsoft Research - Redmond, US), Robert Nieuwenhuis (UPC - Barcelona, ES), Helmut Veith (TU Wien, AT), Andrei Voronkov (University of Manchester, GB)

Caveat: Due to caching problems of dynamic webpages, sometimes newly
uploaded files are not shown. Please reload the page accordingly.


Seminar Wide Materials

Joshua Berdine , Microsoft Research UK - Cambridge
 Combined First-Order and Separation Logic Reasoning
Abstracts: txt Slides: pdf


Nikolaj Bjorner , Microsoft Research - Redmond
 Open Constraint Logic Programming with SMT
Abstracts: txt


Christoph Flamm , Universität Wien

Vijay Ganesh , MIT - Cambridge
 Solvers for Theories of Strings
Abstracts: txt Slides: pdf Other: pdf


Sicun Gao , Carnegie Mellon University - Pittsburgh
 Robust Formulas over Reals and Delta-Complete Decision Procedures
Abstracts: txt


Silvio Ghilardi , Università di Milano
 On Quantifier-free Interpolation for Arrays
Abstracts: txtpdf


Krystof Hoder , University of Manchester
 μZ, Fixed Point Engine in Z3
Abstracts: txt Slides: pdf


Deepak Kapur , University of New Mexico - Albuquerque

Laura Kovacs , TU Wien

Christopher Lynch , Clarkson University - Potsdam
 Modular Theorem Proving
Abstracts: txt


João Marques-Silva , University College - Dublin
 Haplotype Inference with Boolean Optimization
Abstracts: txt Slides: pdf


Feifei Ma , Chinese Academy of Sciences
 Computing the Size of the Solution Space
Abstracts: txt


David Monniaux , VERIMAG - Gières

Robert Nieuwenhuis , UPC - Barcelona

Albert Oliveras , TU of Catalonia - Barcelona
 Title: SAT/SMT Techniques for Scheduling Problems with Sequence-Dependent Setup Times
Abstracts: txt


Ruzica Piskac , EPFL - Lausanne

Enric Rodriguez-Carbonell , UPC - Barcelona

Albert Rubio , UPC - Barcelona
 SAT modulo Non-linear Integer Arithmetic and Linear Invariant Generation


Viorica Sofronie-Stokkermans , MPI für Informatik - Saarbrücken
 Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
Abstracts: txt


Helmut Veith , TU Wien

Andrei Voronkov , University of Manchester

Thomas Wies , IST Austria - Klosterneuburg

Christoph Wintersteiger , Microsoft Research UK - Cambridge
 Lazy Decomposition for Distributed Decision Procedures
Abstracts: txt


Jian Zhang , Chinese Academy of Sciences
 Computing the Size of the Solution Space
Abstracts: txt Slides: pdf


Ting Zhang , Iowa State University - Ames
 Word Equations with Integer Arithmetic?
Abstracts: txt Slides: pdf



Creative Commons License
This webpage and the material that is made available on this webpage is licensed under a
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License.

The CC by-nc-nd license allows you to copy, distribute and transmit the work under the following conditions: