You have Guest access.
Log In
Stefan Berghofer, Tobias Nipkow, Christian Urban and Makarius Wenzel
Front matter
1-22
Let’s Get Physical: Models and Methods for Real-World Security Protocols
23-42
VCC: A Practical System for Verifying Concurrent C
43-59
Without Loss of Generality
60-66
HOL Light: An Overview
67-72
A Brief Overview of Mizar
73-78
A Brief Overview of Agda – A Functional Language with Dependent Types
79-83
The Twelf Proof Assistant
84-98
Hints in Unification
99-114
Psi-calculi in Isabelle
115-130
Some Domain Theory and Denotational Semantics in Coq
131-146
Turning Inductive into Equational Specifications
147-163
Formalizing the Logic-Automaton Connection
164-179
Extended First-Order Logic
180-195
Formalising Observer Theory for Environment-Sensitive Bisimulation
196-211
Formal Certification of a Resource-Aware Language Implementation
212-227
A Certified Data Race Analysis for a Java-like Language
228-243
Formal Analysis of Optical Waveguides in HOL
244-259
The HOL-Omega Logic
260-275
A Purely Definitional Universal Domain
276-292
Types, Maps and Separation Logic
293-309
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
310-326
Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
327-342
Packaging Mathematical Structures
343-358
Practical Tactics for Separation Logic
359-374
Verified LISP Implementations on ARM, x86 and PowerPC
375-390
Trace-Based Coinductive Operational Semantics for While Big-Step and Small-Step, Relational and Functional Styles
391-407
A Better x86 Memory Model: x86-TSO
408-423
Formal Verification of Exact Computations Using Newton’s Method
424-439
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
440-451
A Hoare Logic for the State Monad Proof Pearl
452-468
Certification of Termination Proofs Using CeTA
469-484
A Formalisation of Smallfoot in HOL
485-499
Liveness Reasoning with Isabelle/HOL
500-515
Mind the Gap A Verification Framework for Low-Level C
Back matter
This page requires script.
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info