Editors: Jeremy Avigad and Assia Mahboubi

Jean-Christophe FilliatreDeductive Program Verification
Daniel GraysonVoevodsky's work on formalization of proofs and the foundations of mathematics
John HarrisonMike Gordon: Tribute to a pioneer in theorem proving and formal verification
Reto Achermann, Lukas Humbel, David Cock and Timothy RoscoePhysical addressing on real hardware in Isabelle/HOLJul 11 09:30
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas TabareauTowards Certified Meta-Programming with Typed Template-CoqJul 10 16:30
Andréia B. Avelar, Thaynara A. de Lima and André Luiz GaldinoFormalizing Ring Theory in PVS (short paper)Jul 11 17:00
Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra PalmigianoSoftware tool support for modular reasoning in modal logics of actionsJul 09 14:30
Callum Bannister, Peter Höfner and Gerwin KleinBackwards and Forwards with Separation LogicJul 10 14:00
Véronique Benzaken, Evelyne Contejean, Chantal Keller and Eunice MartinsA Coq formalisation of SQL’s execution enginesJul 10 15:00
Sylvain Boulmé and Alexandre MaréchalA Coq Tactic for Equality Learning in Linear ArithmeticJul 10 12:00
Venanzio Capretta and Colm BastonThe Coinductive Formulation of Common KnowledgeJul 09 15:00
Raphaël CauderlierTactics and certificates in Meta DeduktiJul 11 12:00
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa YamadaA Formalization of the LLL Basis Reduction AlgorithmJul 10 11:00
Christian Doczkal, Guillaume Combette and Damien PousA Formal Proof of the Minor-Exclusion Property for Treewidth-Two GraphsJul 12 09:00
Manuel Eberl, Max W. Haslbeck and Tobias NipkowVerified Analysis of Random Binary Tree StructuresJul 12 16:30
William Farmer, Jacques Carette and Patrick LaskowskiHOL Light QEJul 11 11:30
Denis Firsov, Richard Blair and Aaron StumpEfficient Mendler-Style Lambda-Encodings in CedilleJul 09 12:00
Yannick Forster, Edith Heiter and Gert SmolkaVerification of PCP-Related Computational Reductions in CoqJul 12 10:00
Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz and Josef UrbanProofWatch: Watchlist Guidance for Large Theories in EJul 12 15:00
Jason Gross, Andres Erbsen and Adam ChlipalaReification by ParametricityJul 10 14:30
Simon Jantsch and Michael NorrishVerifying the LTL to Büchi Automata Translation via Very Weak Alternating AutomataJul 12 09:30
Wolfram KahlCalcCheck: 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 SchaeferUnderstanding Parameters of Deductive Verification: An Empirical Investigation of KeYJul 09 16:00
Ramana Kumar, Eric Mullen, Zachary Tatlock and Magnus O. MyreenSoftware Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper)Jul 11 17:20
Dominique Larchey-WendlingProof Pearl: Constructive Extraction of Cycle Finding AlgorithmsJul 12 12:00
Andreas LochbihlerFast machine words in Isabelle/HOLJul 12 11:30
Andreas Lochbihler and Joshua SchneiderRelational parametricity and quotient preservation for modular (co)datatypesJul 11 11:00
Alexandra Mendes and Joao F. FerreiraTowards Verified Handwritten Calculational Proofs (short paper)Jul 11 16:40
Florian Meßner, Julian Parsert, Jonas Schöpf and Christian SternagelA Formally Verified Solver for Homogeneous Linear Diophantine EquationsJul 10 11:30
Étienne MiqueyFormalizing Implicative Algebras in CoqJul 09 14:00
Mariano Moscato, Carlos Lopez Pombo, Cesar Munoz and Marco Antonio Feliu GabaldonBoosting the Reuse of Formal SpecificationsJul 09 16:30
Julian Parsert and Cezary KaliszykTowards Formal Foundations for Game Theory (short paper)Jul 11 16:00
João Paulo Pizani Flor and Wouter SwierstraVerified Timing Transformations in Synchronous Circuits with LambdaPi-WareJul 11 10:00
Christine Rizkallah, Dmitri Garbuzov and Steve ZdancewicA Formal Equational Theory for Call-By-Push-ValueJul 09 17:30
Hira Syeda and Gerwin KleinProgram Verification in the Presence of Cached Address TranslationJul 11 09:00
Joseph Tassarotti and Robert HarperVerified Tail Bounds for Randomized ProgramsJul 12 16:00
Simon Wimmer, Shuwei Hu and Tobias NipkowVerified Memoization and Dynamic ProgrammingJul 12 11:00
Simon Wimmer and Johannes HölzlMDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)Jul 11 16:20
Jinxu Zhao, Bruno C. D. S. Oliveira and Tom SchrijversFormalization of a Polymorphic Subtyping AlgorithmJul 09 17:00
Ran Zmigrod, Matthew L. Daggitt and Timothy G. GriffinAn Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point TheoryJul 10 16:00