| Authors | Title | Paper | Talk |
|---|
| Anna Slobodova, Jared Davis and Sol Swords | Microcode Verification - Another Piece of the Microprocessor Verification Puzzle |  | Jul 14 15:00 |
| Peter Sewell | Retrofitting Rigour | | Jul 16 15:00 |
| Rod Chapman and Florian Schanda | Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK | | Jul 15 15:00 |
| Abhishek Anand and Vincent Rahli | Towards a Formally Verified Proof Assistant | | Jul 14 10:45 |
| Vincent Aravantinos and Sofiene Tahar | Implicational Rewriting Tactics in HOL | | Jul 17 15:30 |
| Jeremy Avigad, Robert Y. Lewis and Cody Roux | A heuristic prover for real inequalities | | Jul 16 16:30 |
| Evmorfia-Iro Bartzia and Pierre-Yves Strub | A Formal Library for Elliptic Curves in the Coq Proof Assistant | | Jul 15 10:45 |
| Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu and Dmitriy Traytel | Truly Modular (Co)datatypes for Isabelle/HOL | | Jul 14 16:30 |
| Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel | Cardinals in Isabelle/HOL | | Jul 15 12:15 |
| Sandrine Blazy, Vincent Laporte and David Pichardie | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code | | Jul 16 17:30 |
| Timothy Bourke, Rob Van Glabbeek and Peter Höfner | Showing invariance compositionally for a process algebra for network protocols | | Jul 16 14:30 |
| Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote and Enrico Tassi | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) | | Jul 16 10:45 |
| David Cock | From Operational Models to Information Theory - Side Channels in pGCL with Isabelle | | Jul 14 14:30 |
| Cyril Cohen and Anders Mörtberg | A Coq Formalization of Finitely Presented Modules | | Jul 16 11:15 |
| Robert Dockins | Formalized, effective domain theory in Coq | | Jul 17 10:45 |
| Christian Doczkal and Gert Smolka | Completeness and Decidability Results for CTL in Coq | | Jul 17 11:15 |
| Jean-François Dufourd | Hypermap Specification and Certified Linked Implementation using Orbits | | Jul 17 15:00 |
| Kento Emoto, Frédéric Loulergue and Julien Tesson | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction | | Jul 15 11:15 |
| Jason Gross, Adam Chlipala and David Spivak | Experience Implementing a Performant Category-Theory Library in Coq | | Jul 14 17:30 |
| Nao Hirokawa, Aart Middeldorp and Christian Sternagel | A New and Formalized Proof of Abstract Completion | | Jul 17 14:30 |
| Ramana Kumar, Rob Arthan, Magnus O. Myreen and Scott Owens | HOL with Definitions: Semantics, Soundness, and a Verified Implementation | | Jul 14 11:45 |
| Peter Lammich | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm | | Jul 15 11:45 |
| Andreas Lochbihler and Johannes Hölzl | Recursive Functions on Lazy Lists via Domains and Topologies | | Jul 14 17:00 |
| Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiene Tahar | Formal Verification of Optical Quantum Flip Gate | | Jul 16 11:45 |
| Gregory Malecha, Adam Chlipala and Thomas Braibant | Compositional Computational Reflection | | Jul 17 12:15 |
| Daniel Matichuk, Toby Murray and Makarius Wenzel | An Isabelle Proof Method Language | | Jul 15 16:30 |
| J Strother Moore | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete | | Jul 14 12:15 |
| Magnus O. Myreen and Jared Davis | The reflective Milawa theorem prover is sound (down to the machine code that runs it) | | Jul 14 11:15 |
| Guyslain Naves and Arnaud Spiwack | Balancing lists: a proof pearl | | Jul 15 14:30 |
| Tobias Nipkow and Dmitriy Traytel | Unified Decision Procedures for Regular Expression Equivalence | | Jul 16 17:00 |
| Martin Ring and Christoph Lüth | Collaborative Interactive Theorem Proving with Clide | | Jul 15 17:30 |
| Umair Siddique, Mohamed Yousri Mahmoud and Sofiene Tahar | On the Formalization of Z-Transform in HOL | | Jul 16 12:15 |
| Matthieu Sozeau and Nicolas Tabareau | Universe Polymorphism in Coq | | Jul 17 11:45 |
| Makarius Wenzel | Asynchronous User Interaction and Tool Integration in Isabelle/PIDE | | Jul 15 17:00 |
| Rob Arthan | HOL Constant Definitions Done Right | | Jul 15 12:45 |
| Matt Kaufmann and J Strother Moore | Rough Diamond: An Extension of Equivalence-based Rewriting | | Jul 14 12:45 |
| Robbert Krebbers, Xavier Leroy and Freek Wiedijk | Formal C semantics: CompCert and the C standard | | Jul 17 12:45 |
| Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie | Mechanical Certification of Loop Pipelining Transformations: A Preview | | Jul 16 12:45 |