|From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT
Cesare Tinelli — The University of Iowa (USA)
|Abstract: Despite decades of research, reasoning efficiently about formulas containing both quantifiers and built-in symbols for a given background theory remains a challenge in automated deduction. Nevertheless, several exciting advances have been made in the last few years, mainly in two directions: (i) integrating theory reasoning in saturation-based calculi for first-order logic and (ii) integrating quantified reasoning into frameworks for ground Satisfiability Modulo Theories (SMT). Focusing at the latter, this talk provides an overview of a general, refutation-based approach to reason about quantified formulas in SMT. The approach maintains a set S of ground formulas that is incrementally expanded with selected instances of quantified input formulas, with the selection based on counter-models of S. In addition to being quite effective in practice, for several logical theories that admit quantifier elimination and have a decidable universal fragment this approach also leads to practically efficient decision procedures for the full theory. While the approach applies to traditional theories with quantifier elimination such as linear real and integer arithmetic, this talk will present new promising developments for the theory of fixed-sized bit vectors and the theory of floating point arithmetic whose full-fragments are notoriously difficult to reason about.|
|Automated Reasoning for Security Protocols
Cas Cremers — CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
|Abstract: Security protocols are a prime example of seemingly simple algorithms for which it would be highly desirable, and possibly feasible, to provide formal proofs of their security. Yet despite several decades of active research, this goal has remained elusive. In this talk we will revisit the security protocol problem, why it is so crucial, and how forms of automated reasoning have helped advance the state of the art, using the TLS 1.3 protocol as an example . We highlight some of the many open general questions and how future advancements in automated reasoning might help towards the ultimate goal of deploying provably secure protocols.|
|Computer Deduction and (Formal) Proofs in Mathematics
Assia Mahboubi — Inria, LS2N, Université de Nantes, France, and Vrije Universiteit Amsterdam, the Netherlands
|Abstract: In 1976, K. Appel and W. Haken announced a computer-assisted proof of the Four Color theorem, solving a long standing open question in graph theory. Since, experimental mathematics have gained momentum and computers have even changed the very nature of peer-reviewed mathematical proofs. This phenomenon can be observed in a broad spectrum of fields, including number theory, dynamical systems, combinatorics, etc.
A vast variety of software is available today for doing computer-aided mathematics. Tools, and the algorithms they implement, are usually grouped in two partially overlapping categories: the symbolic ones, typically computer algebra systems, and the numerical ones. This talk is about a different flavor of software for doing mathematics with a computer: proof assistants. So far proof assistants have been mostly used for research projects in computer science, often related to program verification. But proof assistants, and in particular those based on dependent type theory, are receiving these days an increased attention from users with a background in mathematics. Designing formal libraries about contemporary mathematics raises specific issues and challenges for proof assistants, that we will discuss.