Workshops, Tutorials and Competitions

Competition

Workshops (Schedule: pdf)

Tutorials

  • Franz Baader - Reasoning in Lightweight Description Logics
    Abstract: The Description Logic (DL) research of the last 25 years was mainly concerned with increasing the expressive power of the employed description language without losing the ability of implementing highly-optimized reasoning systems that behave well in practice, in spite of the ever increasing worst-case complexity of the underlying inference problems. OWL DL, the original version of the standard ontology language for the Semantic Web, was based on such an expressive DL, for which reasoning is highly intractable. Its sublanguage OWL Lite was intended to provide a tractable version of OWL, but turned out to be only of a slightly lower worst-case complexity than OWL DL. This and other reasons have led to the development of two new families of lightweight DLs, EL and DL-Lite, which for certain inference problems have a much better algorithmic behavior than for expressive DLs. In this tutorial, we first give a a brief introduction into Description Logics in general, to provide the context, but then concentrate on reasoning in the EL and DL-Lite families of Description Logics. We will describe the rationales behind the design of these new logics and explain the reasons for their good algorithmic properties by sketching the employed inference approaches.
  • Bernhard Beckert - Program Verification with the KeY System
    Abstract: The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a theorem prover for first-order Dynamic Logic for Java with a user-friendly graphical interface.

    The tutorial covers:

    1. Formal specification of object-oriented programs.
    2. Deductive verification of (Java) implementations w.r.t. their specification based on a sequent calculus for Dynamic Logic.
    3. Using verification technology as a basis for other purposes such as, for example, debugging and information-flow analysis.
    4. Case studies and critical assessment.

    Though we concentrate in this tutorial on particular languages (Java and the Java Modeling Language), the presented ideas, problems, and solutions apply to other object-oriented design and implementation languages as well.

    The presentation will alternate between the presentation of slides and live demos of the KeY system. Exercises with solutions are available for those who want to try things hands-on.

    More information on KeY can be found at the web site http://www.key-project.org.

  • Morgan Deters, Dejan Jovanović, Clark Barrett and Cesare Tinelli - Becoming a power user of SMT: The CVC4 solver, how it works, and how best to use it
    Please see http://cvc4.cs.nyu.edu/tutorial/cade-24/ for more details.
  • Marijn Heule - State-of-the-art SAT Solving
    Abstract: Satisfiability (SAT) solvers have become powerful search engines to solve a wide range of applications in fields such as formal verification, planning and bio-informatics. Due to the elementary representation of SAT problems, many low-level optimizations can be implemented. At the same time, there exist clause-based techniques that can simulate several high-level reasoning methods. The tutorial focuses on the search procedures in successful conflict-driven clause learning SAT solvers. It shows how to learn from conflicts and provides an overview of effective heuristics for variable and value selection. Additionally, the tutorial covers recent developments, in particular a technique used in today's strongest solvers: the alternation between "classic" depth-first search with learning, and breadth-first search for simplification.
  • Carsten Schuermann, Taus Brock-Nannestad and Chris Martens - Twelf
    Please see http://www.twelf.org/wiki/CADE_Tutorial for more details.