![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
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).
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.