View: session overviewtalk overviewside by side with other conferences

09:00-10:15 Session 87F: Invited Tutorials (SAT- and SMT-Solvers)
Location: FH, Seminarraum 325/1
Satisfiability Solvers
SPEAKER: Marijn Heule

ABSTRACT.  Satisfiability (SAT) solvers  have become powerful tools to solve a wide range of applications. In case SAT problems are satisfiable, it is easy to validate a witness. However, if SAT problems have no solutions, a proof of unsatisfiability is required to validate that result. Apart from validation, proofs of unsatisfiability are useful in several applications, such as interpolation and extracting a minimal unsatisfiable set  and in tools that use SAT solvers such as  theorem provers. We discuss the two main approaches for unsatisfiability proofs: resolution proofs and clausal proofs. Resolution proofs are used for several application, but they are hard to produce. Clausal proofs are easy to emit, but more costly to check. We compare both approaches, present how to produce and validate proofs, and provide some challenges regarding unsatisfiability proofs.

Proofs in Satisfiability Modulo Theories
SPEAKER: unknown

ABSTRACT. We discuss history, techniques, and challenges in producing and checking proofs from SMT solvers.

10:15-10:45Coffee Break
10:45-11:45 Session 90AK: Invited Tutorials (First- and Higher-order Automated Theorem Provers)
Location: FH, Seminarraum 325/1
First-Order Automated Theorem Provers
Higher-Order Automated Theorem Provers
12:00-13:00 Session 94B: Invited Tutorials (Interactive Theorem Provers and Calculus of Inductive Constructions)
Location: FH, Seminarraum 325/1
Interactive Theorem Provers from the perspective of Isabelle/Isar

ABSTRACT. Interactive Theorem Provers have a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20-30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and dis-provers routinely in their portfolio.

The subsequent exposition of interactive theorem proving (ITP) takes Isabelle/Isar as the focal point to explain concepts of the greater "LCF family'', which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its overall architecture and extra-logical infrastructure.

The "Isar'' aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus "Isabelle/Isar'' today refers to an advanced proof assistant with extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).

Calculus of Inductive Constructions
13:00-14:30Lunch Break
14:30-16:00 Session 96AM: Invited Tutorials (Foundational Proof Certificates, Deduction Modulo and Proof Analysis)
Location: FH, Seminarraum 325/1
Foundational Proof Certificates
SPEAKER: Dale Miller
Deduction Modulo
SPEAKER: Gilles Dowek
Mathematical Proof Analysis
16:00-16:30Coffee Break
16:30-18:00 Session 99AL: Invited Tutorials (Verification, Security and Deep Inference)
Location: FH, Seminarraum 325/1
Program Verification (B Method)
SPEAKER: Gilles Barthe
Deep Inference