diff --git a/web/entries/AODV.html b/web/entries/AODV.html --- a/web/entries/AODV.html +++ b/web/entries/AODV.html @@ -1,234 +1,239 @@
|
Loop freedom of the (untimed) AODV routing protocol
|
|
AVL Trees
|
|
Mechanization of the Algebra for Wireless Networks (AWN)
|
|
Abortable Linearizable Modules
|
|
Abstract Interpretation of Annotated Commands
|
|
Abstract Hoare Logics
|
|
Abstract Rewriting
|
|
Abstract Completeness
|
|
Abstract Soundness
|
|
Formalisation of an Adaptive State Counting Algorithm
|
|
Affine Arithmetic
|
|
Aggregation Algebras
|
|
The Akra-Bazzi theorem and the Master theorem
|
|
Algebraic Numbers in Isabelle/HOL
|
|
Program Construction and Verification Components Based on Kleene Algebra
|
|
Allen's Interval Calculus
|
|
Amortized Complexity Verified
|
|
Anselm's God in Isabelle/HOL
|
|
Applicative Lifting
|
|
Verified Approximation Algorithms
|
|
A Theory of Architectural Design Patterns
|
|
Aristotle's Assertoric Syllogistic
|
|
Arithmetic progressions and relative primes
|
|
Arrow and Gibbard-Satterthwaite
|
|
Auto2 Prover
|
|
Verifying Imperative Programs using Auto2
|
|
AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
|
|
Automatic Data Refinement
|
|
Axiom Systems for Category Theory in Free Logic
|
|
BDD Normalisation
|
|
Bounded Natural Functors with Covariance and Contravariance
|
|
Operations on Bounded Natural Functors
|
|
Spivey's Generalized Recurrence for Bell Numbers
|
|
The Factorization Algorithm of Berlekamp and Zassenhaus
|
|
Bernoulli Numbers
|
|
Bertrand's postulate
|
|
Bicategories
|
|
Binary Search Trees
|
|
A General Theory of Syntax with Bindings
|
|
Binomial Heaps and Skew Binomial Heaps
|
|
Functional Binomial Queues
|
|
Bondy's Theorem
|
|
Boolean Expression Checkers
|
|
Bounded-Deducibility Security
|
|
Büchi Complementation
|
|
The Budan-Fourier Theorem and Counting Real Roots with Multiplicity
|
|
Buffon's Needle Problem
|
|
Chamber Complexes, Coxeter Systems, and Buildings
|
|
A Bytecode Logic for JML and Types
|
|
Communicating Concurrent Kleene Algebra for Distributed Systems Specification
|
|
The CAVA Automata Library
|
|
A Fully Verified Executable LTL Model Checker
|
|
CCS in nominal logic
|
|
Formal Specification of a Generic Separation Kernel
|
|
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
|
|
A formalisation of the Cocke-Younger-Kasami algorithm
|
|
CakeML
|
|
A Verified Code Generator from Isabelle/HOL to CakeML
|
|
The Safety of Call Arity
|
|
Cardinality of Equivalence Relations
|
|
Cardinality of Multisets
|
|
Cardinality of Number Partitions
|
|
Cardinality of Set Partitions
|
|
The Cartan Fixed Point Theorems
|
|
Generating Cases from Labeled Subgoals
|
|
Catalan Numbers
|
|
Category Theory to Yoneda's Lemma
|
|
Category Theory
|
|
Category Theory with Adjunctions and Limits
|
|
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
|
|
The Cayley-Hamilton Theorem
|
|
Certification Monads
|
|
Intersecting Chords Theorem
|
|
Isabelle/Circus
|
|
Clean - An Abstract Imperative Programming Language and its Theory
|
|
Instances of Schneider's generalized protocol of clock synchronization
|
|
Closest Pair of Points Algorithms
|
|
An Example of a Cofinitary Group in Isabelle/HOL
|
|
Coinductive
|
|
A Codatatype of Formal Languages
|
|
Collections Framework
|
|
Lower bound on comparison-based sorting algorithms
|
|
Complete Non-Orders and Fixed Points
|
|
Completeness theorem
|
|
Complex Geometry
|
|
COMPLX: A Verification Framework for Concurrent Imperative Programs
|
|
Formalisation and Analysis of Component Dependencies
|
|
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
|
|
Concurrent IMP
|
|
Concurrent Refinement Algebra and Rely Quotients
|
|
Formalization of Concurrent Revisions
|
|
Consensus Refined
|
|
Constructive Cryptography in HOL
|
|
Constructor Functions
|
|
Light-weight Containers
|
|
CoreC++
|
|
A Formal Model of the Document Object Model
|
|
Count the Number of Complex Roots
|
|
CryptHOL
|
|
Compositional Properties of Crypto-Based Components
|
|
A Framework for Verifying Depth-First Search Algorithms
|
|
A Fast SAT Solver for Isabelle in Standard ML
|
|
Semantics and Data Refinement of Invariant Based Programs
|
|
Generating linear orders for datatypes
|
|
Declarative Semantics for Functional Languages
|
|
Decreasing Diagrams II
|
|
Decreasing Diagrams
|
|
Expressiveness of Deep Learning
|
|
A Verified Compiler for Probability Density Functions
|
|
Compositional Security-Preserving Refinement for Concurrent Imperative Programs
|
|
A Dependent Security Type System for Concurrent Imperative Programs
|
|
Depth First Search
|
|
Derangements Formula
|
|
Deriving class instances for datatypes
|
|
Descartes' Rule of Signs
|
|
Dictionary Construction
|
|
Differential Dynamic Logic
|
|
Differential Game Logic
|
|
Dijkstra's Shortest Path Algorithm
|
|
Homogeneous Linear Diophantine Equations
|
|
Dirichlet L-Functions and Dirichlet's Theorem
|
|
Dirichlet Series
|
|
Pricing in discrete financial models
|
|
Discrete Summation
|
|
Proving the Correctness of Disk Paxos
|
|
Dynamic Architectures
|
|
Parameterized Dynamic Tables
|
|
The Transcendence of e
|
|
Echelon Form
|
|
Formalizing the Edmonds-Karp Algorithm
|
|
Efficient Mergesort
|
|
The Group Law for Elliptic Curves
|
|
Analysing and Comparing Encodability Criteria for Process Calculi
|
|
Epistemic Logic
|
|
Ergodic Theory
|
|
The Error Function
|
|
The Euler–MacLaurin Formula
|
|
Euler's Partition Theorem
|
|
Fast Fourier Transform
|
|
A Constructive Proof for FLP
|
|
First-Order Logic According to Fitting
|
|
First-Order Logic According to Harrison
|
|
A Sequent Calculus for First-Order Logic
|
|
Upper Bounding Diameters of State Spaces of Factored Transition Systems
|
|
The Falling Factorial of a Sum
|
|
Farkas' Lemma and Motzkin's Transposition Theorem
|
|
A Theory of Featherweight Java in Isabelle/HOL
|
|
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
|
|
Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
|
|
File Refinement
|
|
Code Generation for Functions as Data
|
|
Finger Trees
|
|
Finite Automata in Hereditarily Finite Set Theory
|
|
First-Order Terms
|
|
Microeconomics and the First Welfare Theorem
|
|
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
|
|
Fisher–Yates shuffle
|
|
Flow Networks and the Min-Cut-Max-Flow Theorem
|
|
The Floyd-Warshall Algorithm for Shortest Paths
|
|
Flyspeck I: Tame Graphs
|
|
Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
|
|
Verified Construction of Static Single Assignment Form
|
|
Derivatives of Logical Formulas
|
|
Fourier Series
|
|
Free Boolean Algebra
|
|
Free Groups
|
|
Fun With Functions
|
|
Fun With Tilings
|
|
Functional Automata
|
|
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
|
|
Furstenberg's topology and his proof of the infinitude of primes
|
|
Syntax and semantics of a GPU kernel programming language
|
|
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
|
|
Game-based cryptography in HOL
|
|
Gauss-Jordan Elimination for Matrices Represented as Functions
|
|
Gauss-Jordan Algorithm and Its Applications
|
|
Gauss Sums and the Pólya–Vinogradov Inequality
|
|
Formalization of a Generalized Protocol for Clock Synchronization
|
|
The General Triangle Is Unique
|
|
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
|
|
Deriving generic class instances for datatypes
|
|
Formalization of Multiway-Join Algorithms
|
|
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
|
|
A Probabilistic Proof of the Girth-Chromatic Number Theorem
|
|
Gödel's God in Isabelle/HOL
|
|
Implementing the Goodstein Function in λ-Calculus
|
|
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
|
|
Graph Saturation
|
|
Graph Theory
|
|
An Isabelle/HOL formalisation of Green's Theorem
|
|
Gröbner Bases Theory
|
|
Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
|
|
Gromov Hyperbolicity
|
|
Groups, Rings and Modules
|
|
HOL-CSP Version 2.0
|
|
HOLCF-Prelude
|
|
Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
|
|
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
|
|
Hello World
|
|
The Hereditarily Finite Sets
|
|
Hermite Normal Form
|
|
Hidden Markov Models
|
|
An Algebra for Higher-Order Terms
|
|
Hoare Logics for Time Bounds
|
|
Hotel Key Card System
|
|
The Textbook Proof of Huffman's Algorithm
|
|
Formalizing a Seligman-Style Tableau System for Hybrid Logic
|
|
Hybrid Multi-Lane Spatial Logic
|
|
Verification Components for Hybrid Systems
|
|
A shallow embedding of HyperCTL*
|
|
A Formal Model of IEEE Floating Point Arithmetic
|
|
The IMAP CmRDT
|
|
Selected Problems from the International Mathematical Olympiad 2019
|
|
IMP2 – Simple Program Verification in Isabelle/HOL
|
|
Binary Heaps for IMP2
|
|
IP Addresses
|
|
Imperative Insertion Sort
|
|
Proving the Impossibility of Trisecting an Angle and Doubling the Cube
|
|
Gödel's Incompleteness Theorems
|
|
The meta theory of the Incredible Proof Machine
|
|
Inductive Study of Confidentiality
|
|
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
|
|
Information Flow Noninterference via Slicing
|
|
Inter-Procedural Information Flow Noninterference via Slicing
|
|
Integration theory and random variables
|
|
Interval Arithmetic on 32-bit Words
|
|
Iptables Semantics
|
|
Irrational Rapidly Convergent Series
|
|
Isabelle/C
|
|
A Meta-Model for the Isabelle API
|
|
A Case Study in Basic Algebra
|
|
Jinja is not Java
|
|
Jinja with Threads
|
|
Jive Data and Store Model
|
|
The Jordan-Hölder Theorem
|
|
Matrices, Jordan Normal Forms, and Spectral Radius Theory
|
|
Kleene Algebras with Domain
|
|
Kleene Algebra with Tests and Demonic Refinement Algebras
|
|
Knowledge-based programs
|
|
Multidimensional Binary Search Trees
|
|
Refining Authenticated Key Agreement with Strong Adversaries
|
|
Kleene Algebra
|
|
Knot Theory
|
|
The string search algorithm by Knuth, Morris and Pratt
|
|
The Königsberg Bridge Problem and the Friendship Theorem
|
|
Kruskal's Algorithm for Minimum Spanning Forest
|
|
The Kuratowski Closure-Complement Theorem
|
|
A verified LLL algorithm
|
|
A verified factorization algorithm for integer polynomials with polynomial complexity
|
|
LOFT — Verified Migration of Linux Firewalls to SDN
|
|
Linear Temporal Logic
|
|
A Compositional and Unified Translation of LTL into ω-Automata
|
|
Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
|
|
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
|
|
Strong Normalization of Moggis's Computational Metalanguage
|
|
Formalization of Generic Authenticated Data Structures
|
|
The LambdaMu-calculus
|
|
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
|
|
Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
|
|
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
|
|
Landau Symbols
|
|
Laplace Transform
|
|
Latin Square
|
|
Lattice Properties
|
|
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
|
|
Lazy Lists II
|
|
Lazifying case constants
|
|
Lehmer's Theorem
|
|
Lifting Definition Option
|
|
Lightweight Java
|
|
Quantifier Elimination for Linear Arithmetic
|
|
Linear Inequalities
|
|
Linear Programming
|
|
Linear Recurrences
|
|
Liouville numbers
|
|
List Index
|
|
Infinite Lists
|
|
Reasoning about Lists via List Interleaving
|
|
The Inversions of a List
|
|
Analysis of List Update Algorithms
|
|
Local Lexing
|
|
The Localization of a Commutative Ring
|
|
Locally Nameless Sigma Calculus
|
|
Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
|
|
Lower Semicontinuous Functions
|
|
Lp spaces
|
|
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
|
|
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
|
|
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
|
|
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
|
|
Markov Models
|
|
Hall's Marriage Theorem
|
|
The Mason–Stothers Theorem
|
|
Executable Matrix Operations on Matrices of Arbitrary Dimensions
|
|
Tensor Product of Matrices
|
|
Matroids
|
|
Maximum Cardinality Matching
|
|
The Median-of-Medians Selection Algorithm
|
|
Menger's Theorem
|
|
Mersenne primes and the Lucas–Lehmer test
|
|
Mini ML
|
|
Minimal Static Single Assignment Form
|
|
Minkowski's Theorem
|
|
Minsky Machines
|
|
Modal Logics for Nominal Transition Systems
|
|
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
|
|
Monadification, Memoization and Dynamic Programming
|
|
Monad normalisation
|
|
Algebra of Monotonic Boolean Transformers
|
|
Monoidal Categories
|
|
Effect polymorphism in higher-order logic
|
|
Much Ado About Two
|
|
Multi-Party Computation
|
|
Binary Multirelations
|
|
The Myhill-Nerode Theorem Based on Regular Expressions
|
|
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
|
|
Interval Temporal Logic on Natural Numbers
|
|
Native Word
|
|
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
|
|
Network Security Policy Verification
|
|
Von-Neumann-Morgenstern Utility Theorem
|
|
No Faster-Than-Light Observers
|
|
Nominal 2
|
|
Noninterference Security in Communicating Sequential Processes
|
|
Conservation of CSP Noninterference Security under Concurrent Composition
|
|
The Generic Unwinding Theorem for CSP Noninterference Security
|
|
The Inductive Unwinding Theorem for CSP Noninterference Security
|
|
The Ipurge Unwinding Theorem for CSP Noninterference Security
|
|
Conservation of CSP Noninterference Security under Sequential Composition
|
|
Normalization by Evaluation
|
|
Hilbert's Nullstellensatz
|
|
Octonions
|
|
OpSets: Sequential Specifications for Replicated Datatypes
|
|
Open Induction
|
|
Optics
|
|
Optimal Binary Search Trees
|
|
Orbit-Stabiliser Theorem with Application to Rotational Symmetries
|
|
Properties of Orderings and Lattices
|
|
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
|
|
Countable Ordinals
|
|
Ordinals and Cardinals
|
|
Ordinary Differential Equations
|
|
Logical Relations for PCF
|
|
Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
|
|
POPLmark Challenge Via de Bruijn Indices
|
|
Partial Semigroups and Convolution Algebras
|
|
Pairing Heap
|
|
Paraconsistency
|
|
Positional Determinacy of Parity Games
|
|
Mutually Recursive Partial Functions
|
|
Partial Order Reduction
|
|
Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
|
|
Pell's Equation
|
|
Perfect Number Theorem
|
|
Perron-Frobenius Theorem for Spectral Radius Analysis
|
|
The pi-calculus in nominal logic
|
|
The Transcendence of π
|
|
Planarity Certificates
|
|
The Poincaré-Bendixson Theorem
|
|
Poincaré Disc Model
|
|
Polynomial Factorization
|
|
Polynomial Interpolation
|
|
Executable Multivariate Polynomials
|
|
Pop-Refinement
|
|
POSIX Lexing with Derivatives of Regular Expressions
|
|
Possibilistic Noninterference
|
|
Pratt's Primality Certificates
|
|
Formalizing the Logic-Automaton Connection
|
|
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
|
|
Elementary Facts About the Distribution of Primes
|
|
The Divergence of the Prime Harmonic Series
|
|
The Prime Number Theorem
|
|
Priority Queues Based on Braun Trees
|
|
Priority Search Trees
|
|
Probabilistic Noninterference
|
|
Probabilistic Primality Testing
|
|
A Zoo of Probabilistic Systems
|
|
Probabilistic Timed Automata
|
|
Probabilistic while loop
|
|
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
|
|
Projective Geometry
|
|
Promela Formalization
|
|
Proof Strategy Language
|
|
Propositional Resolution and Prime Implicates Generation
|
|
Propositional Proof Systems
|
|
Formalizing Push-Relabel Algorithms
|
|
Pseudo Hoops
|
|
Psi-calculi in Isabelle
|
|
Ptolemy's Theorem
|
|
Quantum Hoare Logic
|
|
QR Decomposition
|
|
Quantales
|
|
Quaternions
|
|
The number of comparisons in QuickSort
|
|
RIPEMD-160
|
|
Algorithms for Reduced Ordered Binary Decision Diagrams
|
|
SHA1, RSA, PSS and more
|
|
Ramsey's theorem, infinitary version
|
|
Expected Shape of Random Binary Search Trees
|
|
Properties of Random Graphs -- Subgraph Containment
|
|
Randomised Binary Search Trees
|
|
Randomised Social Choice Theory
|
|
Rank-Nullity Theorem in Linear Algebra
|
|
Implementing field extensions of the form Q[sqrt(b)]
|
|
Recursion Theory I
|
|
The Imperative Refinement Framework
|
|
Refinement for Monadic Programs
|
|
Formalization of Refinement Calculus for Reactive Systems
|
|
Unified Decision Procedures for Regular Expression Equivalence
|
|
Regular Sets and Expressions
|
|
Regular Algebras
|
|
Relation Algebra
|
|
An Under-Approximate Relational Logic
|
|
Representations of Finite Groups
|
|
Residuated Lattices
|
|
The Resolution Calculus for First-Order Logic
|
|
The Z Property
|
|
Ribbon Proofs
|
|
A Complete Proof of the Robbins Conjecture
|
|
Root-Balanced Tree
|
|
Routing
|
|
Transitive closure according to Roy-Floyd-Warshall
|
|
Formal Verification of Modern SAT Solvers
|
|
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
|
|
Secure information flow and program logics
|
|
A Formalization of Assumptions and Guarantees for Compositional Noninterference
|
|
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
|
|
Safe OCL
|
|
A Comprehensive Framework for Saturation Theorem Proving
|
|
Secondary Sylow Theorems
|
|
Developing Security Protocols by Refinement
|
|
Verification of Selection and Heap Sort Using Locales
|
|
Some classical results in Social Choice Theory
|
|
Separata: Isabelle tactics for Separation Algebra
|
|
Separation Algebra
|
|
A Separation Logic Framework for Imperative HOL
|
|
Invertibility in Sequent Calculi
|
|
Shivers' Control Flow Analysis
|
|
An Axiomatic Characterization of the Single-Source Shortest Path Problem
|
|
Haskell's Show Class in Isabelle/HOL
|
|
Sigma Protocols and Commitment Schemes
|
|
Signature-Based Gröbner Basis Algorithms
|
|
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
|
|
Simple Firewall
|
|
An Incremental Simplex Algorithm with Unsatisfiable Core Generation
|
|
Skew Heap
|
|
Skip Lists
|
|
Towards Certified Slicing
|
|
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
|
|
Smooth Manifolds
|
|
Sound and Complete Sort Encodings for First-Order Logic
|
|
Source Coding Theorem
|
|
Real-Valued Special Functions: Upper and Lower Bounds
|
|
Splay Tree
|
|
Computing N-th Roots using the Babylonian Method
|
|
Stable Matching
|
|
Formalizing Statecharts using Hierarchical Automata
|
|
Stellar Quorum Systems
|
|
The Stern-Brocot Tree
|
|
Stewart's Theorem and Apollonius' Theorem
|
|
Stirling's formula
|
|
Stochastic Matrices and the Perron-Frobenius Theorem
|
|
Stone Algebras
|
|
Stone-Kleene Relation Algebras
|
|
Stone Relation Algebras
|
|
A Reduction Theorem for Store Buffers
|
|
Stream Fusion
|
|
Stream Fusion in HOL with Code Generation
|
|
A Formalization of Strong Security
|
|
Sturm's Theorem
|
|
The Sturm-Tarski Theorem
|
|
Stuttering Equivalence
|
|
Subresultants
|
|
A Hierarchy of Algebras for Boolean Subsets
|
|
Sums of Two and Four Squares
|
|
A Variant of the Superposition Calculus
|
|
Surprise Paradox
|
|
Symmetric Polynomials
|
|
Szpilrajn Extension Theorem
|
|
A Formal Development of a Polychronous Polytimed Coordination Language
|
|
A Definitional Encoding of TLA* in Isabelle/HOL
|
|
A General Method for the Proof of Theorems on Tail-recursive Functions
|
|
The independence of Tarski's Euclidean axiom
|
|
Taylor Models
|
|
Timed Automata
|
|
Topology
|
|
The Tortoise and Hare Algorithm
|
|
The Transcendence of Certain Infinite Series
|
|
Transformer Semantics
|
|
Transition Systems and Automata
|
|
Executable Transitive Closures
|
|
Executable Transitive Closures of Finite Relations
|
|
Treaps
|
|
Tree Automata
|
|
Tree Decomposition
|
|
Basic Geometric Properties of Triangles
|
|
Trie
|
|
The Twelvefold Way
|
|
Type Constructor Classes and Monad Transformers
|
|
Types, Tableaus and Gödel’s God in Isabelle/HOL
|
|
The Unified Policy Framework (UPF)
|
|
Formal Network Models and Their Application to Firewall Policies
|
|
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
|
|
Universal Turing Machine
|
|
Verification of the UpDown Scheme
|
|
Fundamental Properties of Valuation Theory and Hensel's Lemma
|
|
Vector Spaces
|
|
A Generic Framework for Verified Compilers
|
|
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
|
|
VerifyThis 2018 - Polished Isabelle Solutions
|
|
VerifyThis 2019 -- Polished Isabelle Solutions
|
|
VCG - Combinatorial Vickrey-Clarke-Groves Auctions
|
|
A Correctness Proof for the Volpano/Smith Security Typing System
|
|
A Formalization of Declassification with WHAT-and-WHERE-Security
|
|
Strong Eventual Consistency of the Collaborative Editing Framework WOOT
|
|
WebAssembly
|
|
Weight-Balanced Trees
|
|
Well-Quasi-Orders
|
|
Evaluate Winding Numbers through Cauchy Indices
|
|
Finite Machine Word Library
|
|
The Worker/Wrapper Transformation
|
|
XML
|
|
Zermelo Fraenkel Set Theory in Higher-Order Logic
|
|
The Irrationality of ζ(3)
|
|
The Hurwitz and Riemann ζ Functions
|
|
pGCL for Isabelle
|
|
Statistics
|