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 |