LZI - Schloss Dagstuhl - Talks + Materials of Seminar 07401

Collector buttons:

Seminar 07401
Deduction and Decision Procedures

F. Baader (TU Dresden, DE), B. Cook (Microsoft Research, Cambridge, GB), J. Giesl (RWTH Aachen, DE), R. Nieuwenhuis (UPC Barcelona, ES)

Seminar Wide Materials

07401 Executive Summary -- Deduction and Decision Procedures

Abstracts:

DROPS-Submission:

	Upload or overwrite a document file and/or change title of talk


	Due to caching problems of microsofts internet explorer concerning dynamic webpages, sometimes newly uploaded files are not shown. By pressing [CTRL]+[F5], the page is completely reloaded.

Markus Aderhold , TU Darmstadt

Improvements in Formula Generalization

Abstracts:

Slides:

Franz Baader , TU Dresden

Axiom Pinpointing in the Description Logic $\mathcal{EL}$

Abstracts:

Slides:

Domagoj Babic , University of British Columbia - Vancouver

Boosting Verification by Automatic Tuning of Decision Procedures

Abstracts:

Peter Baumgartner , NICTA - Canberra

Theories in Context - Model Evolution Modulo Integer Arithmetic

Abstracts:

Slides:

Bernhard Beckert , Universität Koblenz-Landau

A Dynamic Logic for Deductive Verification of Concurrent Programs

Abstracts:

Marc Bezem , University of Bergen

Aaron Bradley , University of Colorado

The Calculus of Computation

Abstracts:

Slides:

Sergiu Bursuc , ENS - Cachan

Alessandro Cimatti , ITC-irst - Trento

Computing predicate abstractions by integrating BDDs and SMT solvers

Abstracts:

Koen Claessen , Chalmers UT - Göteborg

Instance-based Theorem Proving and Approximating Models

Abstracts:

Germain Faure , TU of Catalonia - Barcelona

Alexander Fuchs , University of Iowa

Silvio Ghilardi , Università di Milano

From non-disjoint combination to model-checking of infinite state systems

Abstracts:

DROPS-Submission:

Jürgen Giesl , RWTH Aachen

Termination of Programs using Term Rewriting and SAT Solving

Abstracts:

DROPS-Submission:

Thomas Hillenbrand , MPI für Informatik - Saarbrücken

Superposition for Finite Domains

Abstracts:

Slides:

Paper:

Jochen Hoenicke , Universität Freiburg

Dieter Hutter , DFKI Saarbrücken

Reiner Hähnle , Chalmers UT - Göteborg

Deepak Kapur , University of New Mexico

Rewriting with Semantic Data Structures: Termination using Dependency Pairs

Abstracts:

Slides:

Laura Kovacs , EPFL - Lausanne

Sava Krstic , Intel Hillsboro

Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL

Abstracts:

Slides:

Viktor Kuncak , EPFL - Lausanne

Temur Kutsia , University of Linz

Relating Context and Sequence Unification

Abstracts:

Christopher Lynch , Clarkson University - Potsdam

SMELS: Satisfiability Modulo Equality with Lazy Superposition

Abstracts:

Aart Middeldorp , Universität Innsbruck

$KBO^3$

Abstracts:

Slides:

Enrica Nicolini , CNRS - Nancy

From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite-State Systems (Part I)

Abstracts:

Ilkka Niemelä , Helsinki University of Technology

Hard Satisfiable Clause Sets for Benchmarking SAT Solvers with Equivalence Reasoning Techniques

Abstracts:

Slides:

Robert Nieuwenhuis , TU of Catalonia - Barcelona

Tobias Nipkow , TU München

Reflecting Quantifier Elimination: From Dense Linear Orders to Presburger Arithmetic

Abstracts:

Slides:

Claudia Obermaier , Universität Koblenz-Landau

Albert Oliveras , TU of Catalonia - Barcelona

MiniMaxSat: an Efficient Weighted MaxSAT Solver

Abstracts:

Slides:

Ruzica Piskac , EPFL - Lausanne

Presburger arithmetic and reasoning about collections of elements

Abstracts:

Slides:

Andreas Podelski , Universität Freiburg

Christophe Ringeissen , INRIA - Nancy

Enric Rodríguez-Carbonell , TU of Catalonia - Barcelona

Experiments with CPLEX as a linear SMT solver

Abstracts:

Albert Rubio , TU of Catalonia - Barcelona

Andrey Rybalchenko , MPI für Software Systeme - Saarbrücken

Path Invariants

Abstracts:

Philipp Rümmer , Chalmers UT - Göteborg

Handling Integer Arithmetic and Quantifiers in a Sequent Calculus

Abstracts:

Slides:

Manfred Schmidt-Schauss , Universität Frankfurt

Renate Schmidt , Manchester University

Using Tableau to Decide Expressive Description Logics with Role Negation

Abstracts:

Peter Schneider-Kamp , RWTH Aachen

Implementing RPO and POLO using SAT

Abstracts:

Slides:

DROPS-Submission:

Stephan Schulz , TU München

Roberto Sebastiani , Università di Trento

Delayed Theory Combination

Abstracts:

Slides:

Viorica Sofronie-Stokkermans , MPI für Informatik - Saarbrücken

Local Reasoning in Verification

Abstracts:

DROPS-Submission:

Ofer Strichman , Technion - Haifa

Can linear hyperplane arrangements be relevant for deciding (disjunctive) linear arithmetic ?

Abstracts:

Slides:

Pierre-Yves Strub , Ecole Polytechnique - Palaiseau

Building Decision Procedures in the Calculus of Inductive Constructions

Abstracts:

René Thiemann , RWTH Aachen

Decision Procedures for Loop Detection

Abstracts:

Slides:

DROPS-Submission:

Cesare Tinelli , University of Iowa

Combined Satisfiability Modulo Parametric Theories

Abstracts:

Slides:

Andrei Voronkov , Manchester University

Integrating Linear Arithmetic into the Superposition Calculus

Abstracts:

Uwe Waldmann , MPI für Informatik - Saarbrücken

New developments in SPASS+T

Abstracts:

Slides:

Christoph Walther , TU Darmstadt

Christoph Weidenbach , MPI für Informatik - Saarbrücken

Automatic Analysis of LAN Infrastructures

Abstracts:

Volker Weispfenning , Universität Passau

Multiplicative Arithmetic Revisited

Abstracts:

Calogero G. Zarba , Saarland University

The Reduction Approach to Decision Procedures

Abstracts:

Slides:

Leonardo de Moura , Microsoft Research - Redmond

Copyright

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:

Attribution: You must attribute the work in the manner specified by the author or licensor (but not in any way that suggests that they endorse you or your use of the work).
Noncommercial: You may not use this work for commercial purposes.
No Derivative Works: You may not alter, transform, or build upon this work.

Seminar 07401 Deduction and Decision Procedures

Copyright

Seminar 07401
Deduction and Decision Procedures