Abstract is missing.
- On the Utility of Formal Methods in the Development and Certification of SoftwareConstance L. Heitmeyer. 1-2 [doi]
- Formal Techniques in Software Engineering: Correct Software and Safe SystemsPeter Liggesmeyer. 3-4 [doi]
- Separation Logic for Small-Step cminorAndrew W. Appel, Sandrine Blazy. 5-21 [doi]
- Formalising Java s Data Race Free GuaranteeDavid Aspinall, Jaroslav Sevcík. 22-37 [doi]
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOLLukas Bulwahn, Alexander Krauss, Tobias Nipkow. 38-53 [doi]
- Formalising Generalised SubstitutionsJeremy E. Dawson. 54-69 [doi]
- Extracting Purely Functional Contents from Logical Inductive TypesDavid Delahaye, Catherine Dubois, Jean-Frédéric Étienne. 70-85 [doi]
- A Modular Formalisation of Finite Group TheoryGeorges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. 86-101 [doi]
- Verifying Nonlinear Real Formulas Via Sums of SquaresJohn Harrison. 102-118 [doi]
- Verification of Expectation Properties for Discrete Random Variables in HOLOsman Hasan, Sofiène Tahar. 119-134 [doi]
- A Formally Verified Prover for the ::::ALC:::: Description LogicJosé-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina. 135-150 [doi]
- Proof Pearl: The Termination Analysis of TerminatorJoe Hurd. 151-156 [doi]
- Improving the Usability of HOL Through Controlled Automation TacticsEunsuk Kang, Mark Aagaard. 157-172 [doi]
- Verified Decision Procedures on Context-Free GrammarsYasuhiko Minamide. 173-188 [doi]
- Using XCAP to Certify Realistic Systems Code: Machine Context ManagementZhaozhong Ni, Dachuan Yu, Zhong Shao. 189-206 [doi]
- Proof Pearl: De Bruijn Terms Really Do WorkMichael Norrish, René Vestergaard. 207-222 [doi]
- Proof Pearl: Looping Around the OrbitSteven Obua. 223-231 [doi]
- Source-Level Proof Reconstruction for Interactive Theorem ProvingLawrence C. Paulson, Kong Woei Susanto. 232-245 [doi]
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LFBrigitte Pientka. 246-261 [doi]
- Automatically Translating Type and Function Definitions from HOL to ACL2James Reynolds. 262-277 [doi]
- Operational Reasoning for Concurrent Caml Programs and Weak Memory ModelsTom Ridge. 278-293 [doi]
- Proof Pearl: Wellfounded Induction on the Ordinals Up to ::::epsilon:::: ::0::Matt Kaufmann, Konrad Slind. 294-301 [doi]
- A Monad-Based Modeling and Verification Toolbox with Application to Security ProtocolsChristoph Sprenger, David A. Basin. 302-318 [doi]
- Primality Proving with Elliptic CurvesLaurent Théry, Guillaume Hanrot. 319-333 [doi]
- HOL2P - A System of Classical Higher Order Logic with Second Order PolymorphismNorbert Völker. 334-351 [doi]
- Building Formal Method Tools in the Isabelle/Isar FrameworkMakarius Wenzel, Burkhart Wolff. 352-367 [doi]
- Simple Types in Type Theory: Deep and Shallow EncodingsFrançois Garillot, Benjamin Werner. 368-382 [doi]
- Mizar s Soft Type SystemFreek Wiedijk. 383-399 [doi]