| Authors | Title | Paper | Talk |
|---|
| Jean-Christophe Filliatre | Deductive Program Verification |  | |
| Daniel Grayson | Voevodsky's work on formalization of proofs and the foundations of mathematics | | |
| John Harrison | Mike Gordon: Tribute to a pioneer in theorem proving and formal verification | | |
| Reto Achermann, Lukas Humbel, David Cock and Timothy Roscoe | Physical addressing on real hardware in Isabelle/HOL | | Jul 11 09:30 |
| Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau | Towards Certified Meta-Programming with Typed Template-Coq | | Jul 10 16:30 |
| Andréia B. Avelar, Thaynara A. de Lima and André Luiz Galdino | Formalizing Ring Theory in PVS (short paper) | | Jul 11 17:00 |
| Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra Palmigiano | Software tool support for modular reasoning in modal logics of actions | | Jul 09 14:30 |
| Callum Bannister, Peter Höfner and Gerwin Klein | Backwards and Forwards with Separation Logic | | Jul 10 14:00 |
| Véronique Benzaken, Evelyne Contejean, Chantal Keller and Eunice Martins | A Coq formalisation of SQL’s execution engines | | Jul 10 15:00 |
| Sylvain Boulmé and Alexandre Maréchal | A Coq Tactic for Equality Learning in Linear Arithmetic | | Jul 10 12:00 |
| Venanzio Capretta and Colm Baston | The Coinductive Formulation of Common Knowledge | | Jul 09 15:00 |
| Raphaël Cauderlier | Tactics and certificates in Meta Dedukti | | Jul 11 12:00 |
| Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada | A Formalization of the LLL Basis Reduction Algorithm | | Jul 10 11:00 |
| Christian Doczkal, Guillaume Combette and Damien Pous | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs | | Jul 12 09:00 |
| Manuel Eberl, Max W. Haslbeck and Tobias Nipkow | Verified Analysis of Random Binary Tree Structures | | Jul 12 16:30 |
| William Farmer, Jacques Carette and Patrick Laskowski | HOL Light QE | | Jul 11 11:30 |
| Denis Firsov, Richard Blair and Aaron Stump | Efficient Mendler-Style Lambda-Encodings in Cedille | | Jul 09 12:00 |
| Yannick Forster, Edith Heiter and Gert Smolka | Verification of PCP-Related Computational Reductions in Coq | | Jul 12 10:00 |
| Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz and Josef Urban | ProofWatch: Watchlist Guidance for Large Theories in E | | Jul 12 15:00 |
| Jason Gross, Andres Erbsen and Adam Chlipala | Reification by Parametricity | | Jul 10 14:30 |
| Simon Jantsch and Michael Norrish | Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata | | Jul 12 09:30 |
| Wolfram Kahl | CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” | | Jul 10 10:00 |
| Alexander Knüppel, Thomas Thüm, Carsten Pardylla and Ina Schaefer | Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY | | Jul 09 16:00 |
| Ramana Kumar, Eric Mullen, Zachary Tatlock and Magnus O. Myreen | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper) | | Jul 11 17:20 |
| Dominique Larchey-Wendling | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms | | Jul 12 12:00 |
| Andreas Lochbihler | Fast machine words in Isabelle/HOL | | Jul 12 11:30 |
| Andreas Lochbihler and Joshua Schneider | Relational parametricity and quotient preservation for modular (co)datatypes | | Jul 11 11:00 |
| Alexandra Mendes and Joao F. Ferreira | Towards Verified Handwritten Calculational Proofs (short paper) | | Jul 11 16:40 |
| Florian Meßner, Julian Parsert, Jonas Schöpf and Christian Sternagel | A Formally Verified Solver for Homogeneous Linear Diophantine Equations | | Jul 10 11:30 |
| Étienne Miquey | Formalizing Implicative Algebras in Coq | | Jul 09 14:00 |
| Mariano Moscato, Carlos Lopez Pombo, Cesar Munoz and Marco Antonio Feliu Gabaldon | Boosting the Reuse of Formal Specifications | | Jul 09 16:30 |
| Julian Parsert and Cezary Kaliszyk | Towards Formal Foundations for Game Theory (short paper) | | Jul 11 16:00 |
| João Paulo Pizani Flor and Wouter Swierstra | Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware | | Jul 11 10:00 |
| Christine Rizkallah, Dmitri Garbuzov and Steve Zdancewic | A Formal Equational Theory for Call-By-Push-Value | | Jul 09 17:30 |
| Hira Syeda and Gerwin Klein | Program Verification in the Presence of Cached Address Translation | | Jul 11 09:00 |
| Joseph Tassarotti and Robert Harper | Verified Tail Bounds for Randomized Programs | | Jul 12 16:00 |
| Simon Wimmer, Shuwei Hu and Tobias Nipkow | Verified Memoization and Dynamic Programming | | Jul 12 11:00 |
| Simon Wimmer and Johannes Hölzl | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) | | Jul 11 16:20 |
| Jinxu Zhao, Bruno C. D. S. Oliveira and Tom Schrijvers | Formalization of a Polymorphic Subtyping Algorithm | | Jul 09 17:00 |
| Ran Zmigrod, Matthew L. Daggitt and Timothy G. Griffin | An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory | | Jul 10 16:00 |