Conferences in DBLP
Constance L. Heitmeyer On the Utility of Formal Methods in the Development and Certification of Software. [Citation Graph (0, 0)][DBLP ] Conf ] Peter Liggesmeyer Formal Techniques in Software Engineering: Correct Software and Safe Systems. [Citation Graph (0, 0)][DBLP ] Conf ] Andrew W. Appel , Sandrine Blazy Separation Logic for Small-Step cminor. [Citation Graph (0, 0)][DBLP ] Conf ] David Aspinall , Jaroslav Sevcík Formalising Java's Data Race Free Guarantee. [Citation Graph (0, 0)][DBLP ] Conf ] Lukas Bulwahn , Alexander Krauss , Tobias Nipkow Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Jeremy E. Dawson Formalising Generalised Substitutions. [Citation Graph (0, 0)][DBLP ] Conf ] David Delahaye , Catherine Dubois , Jean-Frédéric Étienne Extracting Purely Functional Contents from Logical Inductive Types. [Citation Graph (0, 0)][DBLP ] Conf ] Georges Gonthier , Assia Mahboubi , Laurence Rideau , Enrico Tassi , Laurent Théry A Modular Formalisation of Finite Group Theory. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison Verifying Nonlinear Real Formulas Via Sums of Squares. [Citation Graph (0, 0)][DBLP ] Conf ] Osman Hasan , Sofiène Tahar Verification of Expectation Properties for Discrete Random Variables in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] José-Antonio Alonso , Joaquín Borrego-Díaz , María-José Hidalgo , Francisco-Jesús Martín-Mateos , José-Luis Ruiz-Reina A Formally Verified Prover for the ALC Description Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Joe Hurd Proof Pearl: The Termination Analysis of Terminator. [Citation Graph (0, 0)][DBLP ] Conf ] Eunsuk Kang , Mark Aagaard Improving the Usability of HOL Through Controlled Automation Tactics. [Citation Graph (0, 0)][DBLP ] Conf ] Yasuhiko Minamide Verified Decision Procedures on Context-Free Grammars. [Citation Graph (0, 0)][DBLP ] Conf ] Zhaozhong Ni , Dachuan Yu , Zhong Shao Using XCAP to Certify Realistic Systems Code: Machine Context Management. [Citation Graph (0, 0)][DBLP ] Conf ] Michael Norrish , René Vestergaard Proof Pearl: De Bruijn Terms Really Do Work. [Citation Graph (0, 0)][DBLP ] Conf ] Steven Obua Proof Pearl: Looping Around the Orbit. [Citation Graph (0, 0)][DBLP ] Conf ] Lawrence C. Paulson , Kong Woei Susanto Source-Level Proof Reconstruction for Interactive Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Brigitte Pientka Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. [Citation Graph (0, 0)][DBLP ] Conf ] James Reynolds Automatically Translating Type and Function Definitions from HOL to ACL2. [Citation Graph (0, 0)][DBLP ] Conf ] Tom Ridge Operational Reasoning for Concurrent Caml Programs and Weak Memory Models. [Citation Graph (0, 0)][DBLP ] Conf ] Matt Kaufmann , Konrad Slind Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0 . [Citation Graph (0, 0)][DBLP ] Conf ] Christoph Sprenger , David A. Basin A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. [Citation Graph (0, 0)][DBLP ] Conf ] Laurent Théry , Guillaume Hanrot Primality Proving with Elliptic Curves. [Citation Graph (0, 0)][DBLP ] Conf ] Norbert Völker HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism. [Citation Graph (0, 0)][DBLP ] Conf ] Makarius Wenzel , Burkhart Wolff Building Formal Method Tools in the Isabelle/Isar Framework. [Citation Graph (0, 0)][DBLP ] Conf ] François Garillot , Benjamin Werner Simple Types in Type Theory: Deep and Shallow Encodings. [Citation Graph (0, 0)][DBLP ] Conf ] Freek Wiedijk Mizar's Soft Type System. [Citation Graph (0, 0)][DBLP ] Conf ] 