Accepted Papers

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


Comments are closed.