2014 |
2014-11-28:
The Unified Policy Framework (UPF)
Author:
Achim D. Brucker,
Lukas Brügger and
Burkhart Wolff
|
2014-10-23:
Loop freedom of the (untimed) AODV routing protocol
Author:
Timothy Bourke and
Peter Höfner
|
2014-10-13:
Lifting Definition Option
Author:
René Thiemann
|
2014-10-10:
Stream Fusion in HOL with Code Generation
Author:
Andreas Lochbihler and
Alexandra Maximova
|
2014-10-09:
A Verified Compiler for Probability Density Functions
Author:
Manuel Eberl,
Johannes Hölzl and
Tobias Nipkow
|
2014-10-08:
Formalization of Refinement Calculus for Reactive Systems
Author:
Viorel Preoteasa
|
2014-10-03:
Certification Monads
Author:
Christian Sternagel and
René Thiemann
|
2014-10-03:
XML
Author:
Christian Sternagel and
René Thiemann
|
2014-09-25:
Imperative Insertion Sort
Author:
Christian Sternagel
|
2014-09-19:
The Sturm-Tarski Theorem
Author:
Wenda Li
|
2014-09-15:
The Cayley-Hamilton Theorem
Author:
Stephan Adelsberger,
Stefan Hetzl and
Florian Pollak
|
2014-09-09:
The Jordan-Hölder Theorem
Author:
Jakob von Raumer
|
2014-09-04:
Priority Queues Based on Braun Trees
Author:
Tobias Nipkow
|
2014-09-03:
Gauss-Jordan Algorithm and Its Applications
Author:
Jose Divasón and
Jesús Aransay
|
2014-08-29:
Vector Spaces
Author:
Holden Lee
|
2014-08-29:
Real-Valued Special Functions: Upper and Lower Bounds
Author:
Lawrence C. Paulson
|
2014-08-13:
Skew Heap
Author:
Tobias Nipkow
|
2014-08-12:
Splay Tree
Author:
Tobias Nipkow
|
2014-07-29:
Haskell's Show Class in Isabelle/HOL
Author:
Christian Sternagel and
René Thiemann
|
2014-07-18:
Formal Specification of a Generic Separation Kernel
Author:
Freek Verbeek,
Sergey Tverdyshev,
Oto Havle,
Holger Blasum,
Bruno Langenstein,
Werner Stephan,
Yakoub Nemouchi,
Abderrahmane Feliachi,
Burkhart Wolff and
Julien Schmaltz
|
2014-07-13:
pGCL for Isabelle
Author:
David Cock
|
2014-07-07:
Amortized Complexity Verified
Author:
Tobias Nipkow
|
2014-07-04:
Network Security Policy Verification
Author:
Cornelius Diekmann
|
2014-07-03:
Pop-Refinement
Author:
Alessandro Coglio
|
2014-06-12:
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Author:
Dmitriy Traytel and
Tobias Nipkow
|
2014-06-08:
Boolean Expression Checkers
Author:
Tobias Nipkow
|
2014-05-28:
The CAVA Automata Library
Author:
Peter Lammich
|
2014-05-28:
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Author:
Alexander Schimpf and
Peter Lammich
|
2014-05-28:
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Author:
Peter Lammich
|
2014-05-28:
Promela Formalization
Author:
René Neumann
|
2014-05-28:
A Fully Verified Executable LTL Model Checker
Author:
Javier Esparza,
Peter Lammich,
René Neumann,
Tobias Nipkow,
Alexander Schimpf and
Jan-Georg Smaus
|
2014-05-23:
Noninterference Security in Communicating Sequential Processes
Author:
Pasquale Noce
|
2014-05-23:
Transitive closure according to Roy-Floyd-Warshall
Author:
Makarius Wenzel
|
2014-05-21:
Regular Algebras
Author:
Simon Foster and
Georg Struth
|
2014-04-28:
Formalisation and Analysis of Component Dependencies
Author:
Maria Spichkova
|
2014-04-23:
A Formalization of Assumptions and Guarantees for Compositional Noninterference
Author:
Sylvia Grewe,
Heiko Mantel and
Daniel Schoepe
|
2014-04-23:
A Formalization of Strong Security
Author:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel and
Jens Sauer
|
2014-04-23:
A Formalization of Declassification with WHAT-and-WHERE-Security
Author:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel and
Jens Sauer
|
2014-04-22:
Bounded-Deducibility Security
Author:
Andrei Popescu and
Peter Lammich
|
2014-04-16:
A shallow embedding of HyperCTL*
Author:
Markus N. Rabe,
Peter Lammich and
Andrei Popescu
|
2014-04-16:
Abstract Completeness
Author:
Jasmin Christian Blanchette,
Andrei Popescu and
Dmitriy Traytel
|
2014-04-13:
Discrete Summation
Author:
Florian Haftmann
|
2014-04-03:
Syntax and semantics of a GPU kernel programming language
Author:
John Wickerson
|
2014-03-11:
Probabilistic Noninterference
Author:
Andrei Popescu and
Johannes Hölzl
|
2014-03-08:
Mechanization of the Algebra for Wireless Networks (AWN)
Author:
Timothy Bourke
|
2014-02-18:
Mutually Recursive Partial Functions
Author:
René Thiemann
|
2014-02-13:
Properties of Random Graphs -- Subgraph Containment
Author:
Lars Hupel
|
2014-02-11:
Verification of Selection and Heap Sort Using Locales
Author:
Danijela Petrovic
|
2014-02-07:
Affine Arithmetic
Author:
Fabian Immler
|
2014-02-06:
Implementing field extensions of the form Q[sqrt(b)]
Author:
René Thiemann
|
2014-01-30:
Unified Decision Procedures for Regular Expression Equivalence
Author:
Tobias Nipkow and
Dmitriy Traytel
|
2014-01-28:
Secondary Sylow Theorems
Author:
Jakob von Raumer
|
2014-01-25:
Relation Algebra
Author:
Alasdair Armstrong,
Simon Foster,
Georg Struth and
Tjark Weber
|
2014-01-23:
Kleene Algebra with Tests and Demonic Refinement Algebras
Author:
Alasdair Armstrong,
Victor B. F. Gomes and
Georg Struth
|
2014-01-16:
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
Author:
Achim D. Brucker,
Frédéric Tuong and
Burkhart Wolff
|
2014-01-11:
Sturm's Theorem
Author:
Manuel Eberl
|
2014-01-11:
Compositional Properties of Crypto-Based Components
Author:
Maria Spichkova
|