default search action
Archive of Formal Proofs, Volume 2014
Volume 2014, 2014
- Maria Spichkova:
Compositional Properties of Crypto-Based Components. - Manuel Eberl:
Sturm's Theorem. - Achim D. Brucker, Frédéric Tuong, Burkhart Wolff:
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. - Georg Struth, Tjark Weber:
Relation Algebra. - Alasdair Armstrong, Victor B. F. Gomes, Georg Struth:
Kleene Algebra with Tests and Demonic Refinement Algebras. - Jakob von Raumer:
Secondary Sylow Theorems. - Tobias Nipkow, Dmitriy Traytel:
Unified Decision Procedures for Regular Expression Equivalence. - René Thiemann:
Implementing field extensions of the form Q[sqrt(b)]. - Danijela Petrovic:
Verification of Selection and Heap Sort Using Locales. - Lars Hupel:
Properties of Random Graphs - Subgraph Containment. - René Thiemann:
Mutually Recursive Partial Functions. - Timothy Bourke:
Mechanization of the Algebra for Wireless Networks (AWN). - Andrei Popescu, Johannes Hölzl:
Probabilistic Noninterference. - John Wickerson:
Syntax and semantics of a GPU kernel programming language. - Florian Haftmann:
Discrete Summation. - Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Completeness. - Markus N. Rabe, Peter Lammich, Andrei Popescu:
A shallow embedding of HyperCTL. - Andrei Popescu, Peter Lammich:
Bounded-Deducibility Security. - Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer:
A Formalization of Declassification with WHAT-and-WHERE-Security. - Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer:
A Formalization of Strong Security. - Sylvia Grewe, Heiko Mantel, Daniel Schoepe:
A Formalization of Assumptions and Guarantees for Compositional Noninterference. - Maria Spichkova:
Formalisation and Analysis of Component Dependencies. - Simon Foster, Georg Struth:
Regular Algebras. - Makarius Wenzel:
Transitive closure according to Roy-Floyd-Warshall. - Pasquale Noce:
Noninterference Security in Communicating Sequential Processes. - Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus:
A Fully Verified Executable LTL Model Checker. - René Neumann:
Promela Formalization. - Peter Lammich:
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm. - Alexander Schimpf, Peter Lammich:
Converting Linear-Time Temporal Logic to Generalized Büchi Automata. - Peter Lammich:
The CAVA Automata Library. - Tobias Nipkow:
Boolean Expression Checkers. - Dmitriy Traytel, Tobias Nipkow:
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions. - Alessandro Coglio:
Pop-Refinement. - Cornelius Diekmann:
Network Security Policy Verification. - David A. Cock:
pGCL for Isabelle. - Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, Julien Schmaltz:
Formal Specification of a Generic Separation Kernel. - Fabian Immler:
Affine Arithmetic. - Tobias Nipkow:
Amortized Complexity Verified. - Christian Sternagel, René Thiemann:
Haskell's Show-Class in Isabelle/HOL. - Tobias Nipkow:
Splay Tree. - Tobias Nipkow:
Skew Heap. - Lawrence C. Paulson:
Real-Valued Special Functions: Upper and Lower Bounds. - Holden Lee:
Vector Spaces. - Jose Divasón, Jesús Aransay:
Gauss-Jordan Algorithm and Its Applications. - Tobias Nipkow:
Priority Queues Based on Braun Trees. - Jakob von Raumer:
The Jordan-Hölder Theorem. - Stephan Adelsberger, Stefan Hetzl, Florian Pollak:
The Cayley-Hamilton Theorem. - Christian Sternagel:
Imperative Insertion Sort. - Christian Sternagel, René Thiemann:
XML. - Christian Sternagel, René Thiemann:
Certification Monads. - Viorel Preoteasa:
Formalization of Refinement Calculus for Reactive Systems. - Manuel Eberl, Johannes Hölzl, Tobias Nipkow:
A Verified Compiler for Probability Density Functions. - Andreas Lochbihler, Alexandra Maximova:
Stream Fusion in HOL with Code Generation. - René Thiemann:
Lifting Definition Option. - Timothy Bourke, Peter Höfner:
Loop freedom of the (untimed) AODV routing protocol. - Wenda Li:
The Sturm-Tarski Theorem. - Achim D. Brucker, Lukas Brügger, Burkhart Wolff:
The Unified Policy Framework (UPF).
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-15 19:40 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: