Abstract is missing.
- Microcode Verification - Another Piece of the Microprocessor Verification PuzzleJared Davis, Anna Slobodová, Sol Swords. 1-16 [doi]
- Are We There Yet? 20 Years of Industrial Theorem Proving with SPARKRoderick Chapman, Florian Schanda. 17-26 [doi]
- Towards a Formally Verified Proof AssistantAbhishek Anand, Vincent Rahli. 27-44 [doi]
- Implicational Rewriting Tactics in HOLVincent Aravantinos, Sofiène Tahar. 45-60 [doi]
- A Heuristic Prover for Real InequalitiesJeremy Avigad, Robert Y. Lewis, Cody Roux. 61-76 [doi]
- A Formal Library for Elliptic Curves in the Coq Proof AssistantEvmorfia-Iro Bartzia, Pierre-Yves Strub. 77-92 [doi]
- Truly Modular (Co)datatypes for Isabelle/HOLJasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu 0001, Dmitriy Traytel. 93-110 [doi]
- Cardinals in Isabelle/HOLJasmin Christian Blanchette, Andrei Popescu 0001, Dmitriy Traytel. 111-127 [doi]
- Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying CodeSandrine Blazy, Vincent Laporte, David Pichardie. 128-143 [doi]
- Showing Invariance Compositionally for a Process Algebra for Network ProtocolsTimothy Bourke, Rob J. van Glabbeek, Peter Höfner. 144-159 [doi]
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi. 160-176 [doi]
- From Operational Models to Information Theory; Side Channels in pGCL with IsabelleDavid Cock. 177-192 [doi]
- A Coq Formalization of Finitely Presented ModulesCyril Cohen, Anders Mörtberg. 193-208 [doi]
- Formalized, Effective Domain Theory in CoqRobert Dockins. 209-225 [doi]
- Completeness and Decidability Results for CTL in CoqChristian Doczkal, Gert Smolka. 226-241 [doi]
- Hypermap Specification and Certified Linked Implementation Using OrbitsJean-François Dufourd. 242-257 [doi]
- A Verified Generate-Test-Aggregate Coq Library for Parallel Programs ExtractionKento Emoto, Frédéric Loulergue, Julien Tesson. 258-274 [doi]
- Experience Implementing a Performant Category-Theory Library in CoqJason Gross, Adam J. Chlipala, David I. Spivak. 275-291 [doi]
- A New and Formalized Proof of Abstract CompletionNao Hirokawa, Aart Middeldorp, Christian Sternagel. 292-307 [doi]
- HOL with Definitions: Semantics, Soundness, and a Verified ImplementationRamana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens. 308-324 [doi]
- Verified Efficient Implementation of Gabow's Strongly Connected Component AlgorithmPeter Lammich. 325-340 [doi]
- Recursive Functions on Lazy Lists via Domains and TopologiesAndreas Lochbihler, Johannes Hölzl. 341-357 [doi]
- Formal Verification of Optical Quantum Flip GateMohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar. 358-373 [doi]
- Compositional Computational ReflectionGregory Malecha, Adam J. Chlipala, Thomas Braibant. 374-389 [doi]
- An Isabelle Proof Method LanguageDaniel Matichuk, Makarius Wenzel, Toby C. Murray. 390-405 [doi]
- Proof Pearl: Proving a Simple Von Neumann Machine Turing CompleteJ. Strother Moore. 406-420 [doi]
- The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It)Magnus O. Myreen, Jared Davis. 421-436 [doi]
- Balancing Lists: A Proof PearlGuyslain Naves, Arnaud Spiwack. 437-449 [doi]
- Unified Decision Procedures for Regular Expression EquivalenceTobias Nipkow, Dmitriy Traytel. 450-466 [doi]
- Collaborative Interactive Theorem Proving with ClideMartin Ring, Christoph Lüth. 467-482 [doi]
- On the Formalization of Z-Transform in HOLUmair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar. 483-498 [doi]
- Universe Polymorphism in CoqMatthieu Sozeau, Nicolas Tabareau. 499-514 [doi]
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDEMakarius Wenzel. 515-530 [doi]
- HOL Constant Definition Done RightRob Arthan. 531-536 [doi]
- Rough Diamond: An Extension of Equivalence-Based RewritingMatt Kaufmann, J. Strother Moore. 537-542 [doi]
- Formal C Semantics: CompCert and the C StandardRobbert Krebbers, Xavier Leroy, Freek Wiedijk. 543-548 [doi]
- Mechanical Certification of Loop Pipelining Transformations: A PreviewDisha Puri, Sandip Ray, Kecheng Hao, Fei Xie. 549-554 [doi]