Abstract is missing.
- Towards Verification of Product LinesDon S. Batory. 1 [doi]
- Advances in the Formalization of the Odd Order TheoremGeorges Gonthier. 2 [doi]
- Logical Formalisation and Analysis of the Mifare Classic Card in PVSBart Jacobs, Ronny Wichers Schreur. 3-17 [doi]
- Challenges in Verifying Communication FabricsMichael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov. 18-21 [doi]
- Verifying Object-Oriented Programs with Higher-Order Separation Logic in CoqJesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal. 22-38 [doi]
- Relational DecompositionLennart Beringer. 39-54 [doi]
- Structural Analysis of Narratives with the Coq Proof AssistantAnne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza. 55-70 [doi]
- Towards Robustness Analysis Using PVSRenaud Clavel, Laurence Pierre, Régis Leveugle. 71-86 [doi]
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous EnvironmentsPeter Gammie. 87-102 [doi]
- Point-Free, Set-Free Concrete Linear AlgebraGeorges Gonthier. 103-118 [doi]
- A Formalization of Polytime FunctionsSylvain Heraud, David Nowak. 119-134 [doi]
- Three Chapters of Measure Theory in Isabelle/HOLJohannes Hölzl, Armin Heller. 135-151 [doi]
- Termination of Isabelle Functions via Termination of RewritingAlexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl. 152-167 [doi]
- Validating QBF Validity in HOL4Ramana Kumar, Tjark Weber. 168-183 [doi]
- Proving Valid Quantified Boolean Formulas in HOL LightOndrej Kuncar. 184-199 [doi]
- Applying ACL2 to the Formalization of Algebraic Topology: Simplicial PolynomialsLaureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina. 200-215 [doi]
- Animating the Formalised Semantics of a Java-Like LanguageAndreas Lochbihler, Lukas Bulwahn. 216-232 [doi]
- Formalization of Entropy Measures in HOLTarek Mhamdi, Osman Hasan, Sofiène Tahar. 233-248 [doi]
- On the Generation of Positivstellensatz Witnesses in Degenerate CasesDavid Monniaux, Pierre Corbineau. 249-264 [doi]
- A Verified Runtime for a Verified Theorem ProverMagnus O. Myreen, Jared Davis. 265-280 [doi]
- Verified Efficient Enumeration of Plane Graphs Modulo IsomorphismTobias Nipkow. 281-296 [doi]
- Mechanised Computability TheoryMichael Norrish. 297-311 [doi]
- Automatic Differentiation in ACL2Peter Reid, Ruben Gamboa. 312-324 [doi]
- seL4 Enforces IntegrityThomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, Gerwin Klein. 325-340 [doi]
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)Chunhan Wu, Xingyuan Zhang, Christian Urban. 341-356 [doi]
- LCF-Style Bit-Blasting in HOL4Anthony C. J. Fox. 357-362 [doi]
- Lem: A Lightweight Tool for Heavyweight SemanticsScott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell. 363-369 [doi]
- Composable Discovery Engines for Interactive Theorem ProvingPhil Scott, Jacques D. Fleuriot. 370-375 [doi]
- Heterogeneous Proofs: Spider Diagrams Meet Higher-Order ProversMatej Urbas, Mateja Jamnik. 376-382 [doi]