Computer Science

Subject Classification

AMS: Computer science

2023

Fixed-length vectors

Aug 14

Modal quantales, involutive quantales, Dedekind Quantales

by Georg Struth and Cameron Calk

Jul 25

Earley Parser

Jul 16

Gray Codes for Arbitrary Numeral Systems

by Maximilian Spitz

Jul 11

Executable Randomized Algorithms

by Emin Karayel and Manuel Eberl

Jun 19

DCR Syntax and Execution Equivalent Markings

by Axel Christfort and Søren Debois

Jun 16

Cryptographic Standards

Jun 06

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

Tree Enumeration

May 09

The Halting Problem is Soluble in Malament-Hogarth Spacetimes

by Mike Stannett

Apr 29

The Schwartz-Zippel Lemma

by Sunpill Kim and Yong Kiam Tan

Apr 27

Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties

by Thibault Dardinier

Apr 03

Distributed Distinct Elements

by Emin Karayel

Apr 03

Distributed Distinct Elements

by Emin Karayel

Apr 03

Distributed Distinct Elements

by Emin Karayel

Apr 03

Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs

by Thibault Dardinier

Mar 15

Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs

by Thibault Dardinier

Mar 15

Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs

by Thibault Dardinier

Mar 15

Expander Graphs

by Emin Karayel

Mar 03

Expander Graphs

by Emin Karayel

Mar 03

Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion

by Andrei Popescu

Feb 28

Hardness of Lattice Problems

by Katharina Kreuzer

Feb 02

ABY3 Multiplication and Array Shuffling

Jan 27

A Hoare Logic for Diverging Programs

by Johannes Åman Pohjola, Magnus O. Myreen and Miki Tanaka

Jan 20

The Cook-Levin theorem

by Frank J. Balbach

Jan 08

Intersection of two monoids generated by two element codes

by Štěpán Holub and Štěpán Starosta

Jan 03

Binary codes that do not preserve primitivity

by Štěpán Holub and Martin Raška

Jan 03

2022

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

by Katherine Kosaian, Yong Kiam Tan and André Platzer

Dec 15

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

by Christian Dalvit and René Thiemann

Nov 30

A Formal CHERI-C Memory Model

by Seung Hoon Park

Nov 25

Combinatorial Enumeration Algorithms

by Paul Hofmeier and Emin Karayel

Nov 11

Verification of Query Optimization Algorithms

by Lukas Stevens and Bernhard Stöckl

Oct 04

Maximum Segment Sum

Sep 29

Making Arbitrary Relational Calculus Queries Safe-Range

by Martin Raszyk and Dmitriy Traytel

Sep 28

CRYSTALS-Kyber

by Katharina Kreuzer

Sep 08

Unbounded Separation Logic

by Thibault Dardinier

Sep 05

Number Theoretic Transform

by Thomas Ammer and Katharina Kreuzer

Aug 18

Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph

by Stephan Merz and Vincent Trélat

Aug 17

Verified Complete Test Strategies for Finite State Machines

by Robert Sachtleben

Aug 09

Verified Complete Test Strategies for Finite State Machines

by Robert Sachtleben

Aug 09

Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML

by Achim D. Brucker

Jul 29

Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL

by Diego Marmsoler and Achim D. Brucker

Jul 18

Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL

by Diego Marmsoler and Achim D. Brucker

Jul 18

A Reuse-Based Multi-Stage Compiler Verification for Language IMP

by Pasquale Noce

Jul 10

Real-Time Double-Ended Queue

by Balazs Toth and Tobias Nipkow

Jun 23

IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols

by Tobias Klenze and Christoph Sprenger

Jun 08

IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols

by Tobias Klenze and Christoph Sprenger

Jun 08

A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

by Thibault Dardinier

May 30

Formalization of a Framework for the Sound Automation of Magic Wands

by Thibault Dardinier

May 18

Formalization of Randomized Approximation Algorithms for Frequency Moments

by Emin Karayel

Apr 08

Formalization of Randomized Approximation Algorithms for Frequency Moments

by Emin Karayel

Apr 08

A Combinator Library for Prefix-Free Codes

by Emin Karayel

Apr 08

A Combinator Library for Prefix-Free Codes

by Emin Karayel

Apr 08

Residuated Transition Systems

by Eugene W. Stark

Feb 28

Residuated Transition Systems

by Eugene W. Stark

Feb 28

Residuated Transition Systems

by Eugene W. Stark

Feb 28

Universal Hash Families

by Emin Karayel

Feb 20

First-Order Query Evaluation

by Martin Raszyk

Feb 15

Multi-Head Monitoring of Metric Dynamic Logic

by Martin Raszyk

Feb 13

Enumeration of Equivalence Relations

by Emin Karayel

Feb 04

Quasi-Borel Spaces

by Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato

Feb 03

First-Order Theory of Rewriting

by Alexander Lochmann and Bertram Felgenhauer

Feb 02

Median Method

by Emin Karayel

Jan 25

2021

Gale-Shapley Algorithm

by Tobias Nipkow

Dec 29

Verified Algorithms for Solving Markov Decision Processes

by Maximilian Schäffeler and Mohammad Abdulaziz

Dec 16

Regular Tree Relations

by Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann and Thomas Sternagel

Dec 15

van Emde Boas Trees

by Thomas Ammer and Peter Lammich

Nov 23

Quantum and Classical Registers

by Dominique Unruh

Oct 28

Quantum and Classical Registers

by Dominique Unruh

Oct 28

Quantum and Classical Registers

by Dominique Unruh

Oct 28

X86 instruction semantics and basic block symbolic execution

by Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag and Binoy Ravindran

Oct 13

X86 instruction semantics and basic block symbolic execution

by Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag and Binoy Ravindran

Oct 13

Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations

by Walter Guttmann

Oct 12

Verified Quadratic Virtual Substitution for Real Arithmetic

by Matias Scharager, Katherine Kosaian, Stefan Mitsch and André Platzer

Oct 02

A data flow analysis algorithm for computing dominators

Sep 05

Logging-independent Message Anonymity in the Relational Method

by Pasquale Noce

Aug 26

Fresh identifiers

by Andrei Popescu and Thomas Bauereiss

Aug 16

CoSMeDis: A confidentiality-verified distributed social media platform

by Thomas Bauereiss and Andrei Popescu

Aug 16

CoSMed: A confidentiality-verified social media platform

by Thomas Bauereiss and Andrei Popescu

Aug 16

Compositional BD Security

by Thomas Bauereiss and Andrei Popescu

Aug 16

CoCon: A Confidentiality-Verified Conference Management System

by Andrei Popescu, Peter Lammich and Thomas Bauereiss

Aug 16

MiniSail - A kernel language for the ISA specification language SAIL

by Mark Wassell

Jun 18

A Shorter Compiler Correctness Proof for Language IMP

by Pasquale Noce

Jun 04

Lyndon words

by Štěpán Holub and Štěpán Starosta

May 24

Graph Lemma

by Štěpán Holub, Martin Raška and Štěpán Starosta

May 24

Combinatorics on Words Basics

by Štěpán Holub, Martin Raška and Štěpán Starosta

May 24

Regression Test Selection

by Susannah Mansky

Apr 30

The BKR Decision Procedure for Univariate Real Arithmetic

by Katherine Kosaian, Yong Kiam Tan and André Platzer

Apr 24

Formalization of Timely Dataflow's Progress Tracking Protocol

by Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel

Apr 13

Information Flow Control via Dependency Tracking

by Benedikt Nordhoff

Apr 01

Constructive Cryptography in HOL: the Communication Modeling Aspect

by Andreas Lochbihler and S. Reza Sefidgar

Mar 17

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

by Ralph Bottesch, Jose Divasón and René Thiemann

Mar 12

Quantum projective measurements and the CHSH inequality

by Mnacho Echenim

Mar 03

A Verified Imperative Implementation of B-Trees

by Niels Mündler

Feb 24

A Verified Imperative Implementation of B-Trees

by Niels Mündler

Feb 24

Hood-Melville Queue

by Alejandro Gómez-Londoño

Jan 18

JinjaDCI: a Java semantics with dynamic class initialization

by Susannah Mansky

Jan 11

2020

Relational Minimum Spanning Tree Algorithms

by Walter Guttmann and Nicolas Robinson-O’Brien

Dec 08

Inline Caching and Unboxing Optimization for Interpreters

by Martin Desharnais

Dec 07

The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols

by Pasquale Noce

Dec 05

Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information

by Anthony Bordg, Hanna Lachnitt and Yijun He

Nov 22

The HOL-CSP Refinement Toolkit

by Safouan Taha, Burkhart Wolff and Lina Ye

Nov 19

The HOL-CSP Refinement Toolkit

by Safouan Taha, Burkhart Wolff and Lina Ye

Nov 19

Verified SAT-Based AI Planning

by Mohammad Abdulaziz and Friedrich Kurz

Oct 29

AI Planning Languages Semantics

by Mohammad Abdulaziz and Peter Lammich

Oct 29

A Sound Type System for Physical Quantities, Units, and Measurements

by Simon Foster and Burkhart Wolff

Oct 20

Finite Map Extras

by Javier Díaz

Oct 12

The Safely Composable DOM

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formalization of Web Components

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formalization of Safely Composable Web Components

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formal Model of the Safely Composable Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formal Model of the Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

Sep 28

Inference of Extended Finite State Machines

by Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick

Sep 07

A Formal Model of Extended Finite State Machines

by Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick

Sep 07

Some classical results in inductive inference of recursive functions

by Frank J. Balbach

Aug 31

Practical Algebraic Calculus Checker

by Mathias Fleury and Daniela Kaufmann

Aug 31

Relational Disjoint-Set Forests

by Walter Guttmann

Aug 26

Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching

by Peter Gammie

Aug 25

A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

by Ben Fiedler and Dmitriy Traytel

Jul 21

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

by Albert Rizaldi and Fabian Immler

Jun 01

A verified algorithm for computing the Smith normal form of a matrix

by Jose Divasón

May 23

An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

by Salomon Sickert

May 08

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

by Florian Kammüller

Apr 27

Authenticated Data Structures As Functors

by Andreas Lochbihler and Ognjen Marić

Apr 16

Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows

by Lukas Heimes, Dmitriy Traytel and Joshua Schneider

Apr 10

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

by Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel

Apr 09

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

by Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel

Apr 09

Stateful Protocol Composition and Typing

by Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker

Apr 08

Automated Stateful Protocol Verification

by Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull

Apr 08

Strong Eventual Consistency of the Collaborative Editing Framework WOOT

by Emin Karayel and Edgar Gonzàlez

Mar 25

An Under-Approximate Relational Logic

Mar 12

An Under-Approximate Relational Logic

Mar 12

Hello World

by Cornelius Diekmann and Lars Hupel

Mar 07

A Generic Framework for Verified Compilers

by Martin Desharnais

Feb 10

Verified Approximation Algorithms

by Robin Eßmann, Tobias Nipkow, Simon Robillard and Ujkan Sulejmani

Jan 16

Closest Pair of Points Algorithms

by Martin Rau and Tobias Nipkow

Jan 13

Skip Lists

by Max W. Haslbeck and Manuel Eberl

Jan 09

Skip Lists

by Max W. Haslbeck and Manuel Eberl

Jan 09

2019

An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges

by Pasquale Noce

Dec 04

An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges

by Pasquale Noce

Dec 04

Interval Arithmetic on 32-bit Words

Nov 27

Isabelle/C

by Frédéric Tuong and Burkhart Wolff

Oct 22

Isabelle/C

by Frédéric Tuong and Burkhart Wolff

Oct 22

VerifyThis 2019 -- Polished Isabelle Solutions

by Peter Lammich and Simon Wimmer

Oct 16

Sigma Protocols and Commitment Schemes

by David Butler and Andreas Lochbihler

Oct 07

Clean - An Abstract Imperative Programming Language and its Theory

by Frédéric Tuong and Burkhart Wolff

Oct 04

Clean - An Abstract Imperative Programming Language and its Theory

by Frédéric Tuong and Burkhart Wolff

Oct 04

Formalization of Multiway-Join Algorithms

by Thibault Dardinier

Sep 16

Formalization of Multiway-Join Algorithms

by Thibault Dardinier

Sep 16

Formalisation of an Adaptive State Counting Algorithm

by Robert Sachtleben

Aug 16

Formalisation of an Adaptive State Counting Algorithm

by Robert Sachtleben

Aug 16

Communicating Concurrent Kleene Algebra for Distributed Systems Specification

by Maxime Buyse and Jason Jaskolka

Aug 06

Stellar Quorum Systems

by Giuliano Losa

Aug 01

A Formal Development of a Polychronous Polytimed Coordination Language

by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff

Jul 30

A Formal Development of a Polychronous Polytimed Coordination Language

by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff

Jul 30

A Formal Development of a Polychronous Polytimed Coordination Language

by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff

Jul 30

A Verified Code Generator from Isabelle/HOL to CakeML

Jul 08

Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

by Joshua Schneider and Dmitriy Traytel

Jul 04

Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

by Joshua Schneider and Dmitriy Traytel

Jul 04

Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra

by Peter Lammich and Tobias Nipkow

Jun 25

Priority Search Trees

by Peter Lammich and Tobias Nipkow

Jun 25

Binary Heaps for IMP2

by Simon Griebel

Jun 13

Binary Heaps for IMP2

by Simon Griebel

Jun 13

Differential Game Logic

by André Platzer

Jun 03

Multidimensional Binary Search Trees

May 30

Formalization of Generic Authenticated Data Structures

by Matthias Brun and Dmitriy Traytel

May 14

Formalization of Generic Authenticated Data Structures

by Matthias Brun and Dmitriy Traytel

May 14

Multi-Party Computation

by David Aspinall and David Butler

May 09

HOL-CSP Version 2.0

by Safouan Taha, Lina Ye and Burkhart Wolff

Apr 26

HOL-CSP Version 2.0

by Safouan Taha, Lina Ye and Burkhart Wolff

Apr 26

A Compositional and Unified Translation of LTL into ω-Automata

by Benedikt Seidl and Salomon Sickert

Apr 16

A General Theory of Syntax with Bindings

by Lorenzo Gheri and Andrei Popescu

Apr 06

A General Theory of Syntax with Bindings

by Lorenzo Gheri and Andrei Popescu

Apr 06

Quantum Hoare Logic

by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan

Mar 24

Quantum Hoare Logic

by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan

Mar 24

Safe OCL

by Denis Nikiforov

Mar 09

Kruskal's Algorithm for Minimum Spanning Forest

by Maximilian P. L. Haslbeck, Peter Lammich and Julian Biendarra

Feb 14

Probabilistic Primality Testing

by Daniel Stüwe and Manuel Eberl

Feb 11

Universal Turing Machine

by Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten and Franz Regensburger

Feb 08

The Inversions of a List

by Manuel Eberl

Feb 01

Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

by Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro and Burkhart Wolff

Feb 01

IMP2 – Simple Program Verification in Isabelle/HOL

by Peter Lammich and Simon Wimmer

Jan 15

IMP2 – Simple Program Verification in Isabelle/HOL

by Peter Lammich and Simon Wimmer

Jan 15

An Algebra for Higher-Order Terms

Jan 15

A Reduction Theorem for Store Buffers

by Ernie Cohen and Norbert Schirmer

Jan 07

2018

A Formal Model of the Document Object Model

by Achim D. Brucker and Michael Herzberg

Dec 26

Formalization of Concurrent Revisions

by Roy Overbeek

Dec 25

Verifying Imperative Programs using Auto2

Dec 21

Verifying Imperative Programs using Auto2

Dec 21

Constructive Cryptography in HOL

by Andreas Lochbihler and S. Reza Sefidgar

Dec 17

Transformer Semantics

by Georg Struth

Dec 11

Deriving generic class instances for datatypes

by Jonas Rädle and Lars Hupel

Nov 06

Randomised Binary Search Trees

by Manuel Eberl

Oct 19

Randomised Binary Search Trees

by Manuel Eberl

Oct 19

Upper Bounding Diameters of State Spaces of Factored Transition Systems

by Friedrich Kurz and Mohammad Abdulaziz

Oct 12

Signature-Based Gröbner Basis Algorithms

by Alexander Maletzky

Sep 20

An Incremental Simplex Algorithm with Unsatisfiable Core Generation

by Filip Marić, Mirko Spasić and René Thiemann

Aug 24

Partial Order Reduction

by Julian Brunner

Jun 05

Optimal Binary Search Trees

by Tobias Nipkow and Dániel Somogyi

May 27

Optimal Binary Search Trees

by Tobias Nipkow and Dániel Somogyi

May 27

Hidden Markov Models

by Simon Wimmer

May 25

Probabilistic Timed Automata

by Simon Wimmer and Johannes Hölzl

May 24

Monadification, Memoization and Dynamic Programming

by Simon Wimmer, Shuwei Hu and Tobias Nipkow

May 22

Monadification, Memoization and Dynamic Programming

by Simon Wimmer, Shuwei Hu and Tobias Nipkow

May 22

OpSets: Sequential Specifications for Replicated Datatypes

by Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan and Alastair R. Beresford

May 10

OpSets: Sequential Specifications for Replicated Datatypes

by Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan and Alastair R. Beresford

May 10

An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties

by Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock and Markus Tasch

May 07

WebAssembly

Apr 29

VerifyThis 2018 - Polished Isabelle Solutions

by Peter Lammich and Simon Wimmer

Apr 27

Bounded Natural Functors with Covariance and Contravariance

by Andreas Lochbihler and Joshua Schneider

Apr 24

Weight-Balanced Trees

by Tobias Nipkow and Stefan Dirix

Mar 13

CakeML

by Lars Hupel and Yu Zhang

Mar 12

A Theory of Architectural Design Patterns

by Diego Marmsoler

Mar 01

Hoare Logics for Time Bounds

by Maximilian P. L. Haslbeck and Tobias Nipkow

Feb 26

Treaps

by Max W. Haslbeck, Manuel Eberl and Tobias Nipkow

Feb 06

First-Order Terms

by Christian Sternagel and René Thiemann

Feb 06

A verified LLL algorithm

by Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Feb 02

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

2017

The Median-of-Medians Selection Algorithm

by Manuel Eberl

Dec 21

The string search algorithm by Knuth, Morris and Pratt

by Fabian Hellauer and Peter Lammich

Dec 18

Stochastic Matrices and the Perron-Frobenius Theorem

by René Thiemann

Nov 22

The IMAP CmRDT

by Tim Jungnickel, Lennart Oldenburg and Matthias Loibl

Nov 09

The IMAP CmRDT

by Tim Jungnickel, Lennart Oldenburg and Matthias Loibl

Nov 09

Transition Systems and Automata

by Julian Brunner

Oct 19

Büchi Complementation

by Julian Brunner

Oct 19

Homogeneous Linear Diophantine Equations

by Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel

Oct 14

Root-Balanced Tree

by Tobias Nipkow

Aug 20

The LambdaMu-calculus

by Cristina Matache, Victor B. F. Gomes and Dominic P. Mulligan

Aug 16

Dynamic Architectures

by Diego Marmsoler

Jul 28

Declarative Semantics for Functional Languages

Jul 21

HOLCF-Prelude

by Joachim Breitner, Brian Huffman, Neil Mitchell and Christian Sternagel

Jul 15

Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus

by Michael Rawson

Jul 09

A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes

by Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford

Jul 07

A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes

by Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford

Jul 07

Formalizing Push-Relabel Algorithms

by Peter Lammich and S. Reza Sefidgar

Jun 01

Optics

by Simon Foster, Christian Pardillo-Laursen and Frank Zeyda

May 25

Developing Security Protocols by Refinement

by Christoph Sprenger and Ivano Somaini

May 24

The Floyd-Warshall Algorithm for Shortest Paths

by Simon Wimmer and Peter Lammich

May 08

Probabilistic while loop

by Andreas Lochbihler

May 05

Probabilistic while loop

by Andreas Lochbihler

May 05

Monad normalisation

by Joshua Schneider, Manuel Eberl and Andreas Lochbihler

May 05

Game-based cryptography in HOL

by Andreas Lochbihler, S. Reza Sefidgar and Bhargav Bhatt

May 05

Effect polymorphism in higher-order logic

by Andreas Lochbihler

May 05

CryptHOL

by Andreas Lochbihler

May 05

CryptHOL

by Andreas Lochbihler

May 05

Local Lexing

Apr 28

Expected Shape of Random Binary Search Trees

by Manuel Eberl

Apr 04

Expected Shape of Random Binary Search Trees

by Manuel Eberl

Apr 04

The number of comparisons in QuickSort

by Manuel Eberl

Mar 15

The number of comparisons in QuickSort

by Manuel Eberl

Mar 15

Lower bound on comparison-based sorting algorithms

by Manuel Eberl

Mar 15

The Group Law for Elliptic Curves

by Stefan Berghofer

Feb 28

Differential Dynamic Logic

Feb 13

Refining Authenticated Key Agreement with Strong Adversaries

by Joseph Lallemand and Christoph Sprenger

Jan 31

Minimal Static Single Assignment Form

by Max Wagner and Denis Lohner

Jan 17

Formal Network Models and Their Application to Firewall Policies

by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

Jan 08

Formal Network Models and Their Application to Firewall Policies

by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

Jan 08

Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method

by Pasquale Noce

Jan 03

2016

Concurrent Refinement Algebra and Rely Quotients

by Julian Fell, Ian J. Hayes and Andrius Velykis

Dec 30

COMPLX: A Verification Framework for Concurrent Imperative Programs

by Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong

Nov 29

COMPLX: A Verification Framework for Concurrent Imperative Programs

by Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong

Nov 29

Abstract Interpretation of Annotated Commands

by Tobias Nipkow

Nov 23

Separata: Isabelle tactics for Separation Algebra

by Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston

Nov 16

Expressiveness of Deep Learning

by Alexander Bentkamp

Nov 10

Modal Logics for Nominal Transition Systems

by Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström and Ramunas Gutkovas

Oct 25

LOFT — Verified Migration of Linux Firewalls to SDN

by Julius Michaelis and Cornelius Diekmann

Oct 21

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor

by Zhe Hou, David Sanan, Alwen Tiu and Yang Liu

Oct 19

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor

by Zhe Hou, David Sanan, Alwen Tiu and Yang Liu

Oct 19

Fisher–Yates shuffle

by Manuel Eberl

Sep 30

Iptables Semantics

by Cornelius Diekmann and Lars Hupel

Sep 09

Routing

by Julius Michaelis and Cornelius Diekmann

Aug 31

Simple Firewall

by Cornelius Diekmann, Julius Michaelis and Max W. Haslbeck

Aug 24

Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths

by Romain Aissat, Frederic Voisin and Burkhart Wolff

Aug 18

Formalizing the Edmonds-Karp Algorithm

by Peter Lammich and S. Reza Sefidgar

Aug 12

The Imperative Refinement Framework

by Peter Lammich

Aug 08

The Imperative Refinement Framework

by Peter Lammich

Aug 08

Pairing Heap

by Hauke Brinkop and Tobias Nipkow

Jul 14

A Framework for Verifying Depth-First Search Algorithms

by Peter Lammich and René Neumann

Jul 05

IP Addresses

by Cornelius Diekmann, Julius Michaelis and Lars Hupel

Jun 28

Compositional Security-Preserving Refinement for Concurrent Imperative Programs

by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

Jun 28

A Dependent Security Type System for Concurrent Imperative Programs

by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

Jun 25

A Dependent Security Type System for Concurrent Imperative Programs

by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

Jun 25

Conservation of CSP Noninterference Security under Concurrent Composition

by Pasquale Noce

Jun 13

Conservation of CSP Noninterference Security under Concurrent Composition

by Pasquale Noce

Jun 13

Finite Machine Word Library

by Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk and Thomas Sewell

Jun 09

POSIX Lexing with Derivatives of Regular Expressions

by Fahad Ausaf, Roy Dyckhoff and Christian Urban

May 24

A Constructive Proof for FLP

by Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters and Uwe Nestmann

May 18

Gröbner Bases Theory

by Fabian Immler and Alexander Maletzky

May 02

Algorithms for Reduced Ordered Binary Decision Diagrams

by Julius Michaelis, Max W. Haslbeck, Peter Lammich and Lars Hupel

Apr 27

Algorithms for Reduced Ordered Binary Decision Diagrams

by Julius Michaelis, Max W. Haslbeck, Peter Lammich and Lars Hupel

Apr 27

A formalisation of the Cocke-Younger-Kasami algorithm

by Maksym Bortin

Apr 27

A formalisation of the Cocke-Younger-Kasami algorithm

by Maksym Bortin

Apr 27

Conservation of CSP Noninterference Security under Sequential Composition

by Pasquale Noce

Apr 26

Conservation of CSP Noninterference Security under Sequential Composition

by Pasquale Noce

Apr 26

Kleene Algebras with Domain

by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber

Apr 12

Kleene Algebras with Domain

by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber

Apr 12

Timed Automata

by Simon Wimmer

Mar 08

Linear Temporal Logic

by Salomon Sickert

Mar 01

Analysis of List Update Algorithms

by Maximilian P. L. Haslbeck and Tobias Nipkow

Feb 17

Analysis of List Update Algorithms

by Maximilian P. L. Haslbeck and Tobias Nipkow

Feb 17

Verified Construction of Static Single Assignment Form

by Sebastian Ullrich and Denis Lohner

Feb 05

Tensor Product of Matrices

by T.V.H. Prathamesh

Jan 18

2015

Applicative Lifting

by Andreas Lochbihler and Joshua Schneider

Dec 22

The Tortoise and Hare Algorithm

by Peter Gammie

Nov 18

A Meta-Model for the Isabelle API

by Frédéric Tuong and Burkhart Wolff

Sep 16

Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata

by Salomon Sickert

Sep 04

The Inductive Unwinding Theorem for CSP Noninterference Security

by Pasquale Noce

Aug 18

Analysing and Comparing Encodability Criteria for Process Calculi

by Kirstin Peters and Rob van Glabbeek

Aug 10

Generating Cases from Labeled Subgoals

by Lars Noschinski

Jul 21

Hermite Normal Form

by Jose Divasón and Jesús Aransay

Jul 07

The Ipurge Unwinding Theorem for CSP Noninterference Security

by Pasquale Noce

Jun 11

The Generic Unwinding Theorem for CSP Noninterference Security

by Pasquale Noce

Jun 11

The Generic Unwinding Theorem for CSP Noninterference Security

by Pasquale Noce

Jun 11

Reasoning about Lists via List Interleaving

by Pasquale Noce

Jun 11

Parameterized Dynamic Tables

by Tobias Nipkow

Jun 07

Derivatives of Logical Formulas

by Dmitriy Traytel

May 28

A Zoo of Probabilistic Systems

by Johannes Hölzl, Andreas Lochbihler and Dmitriy Traytel

May 27

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO

by Peter Gammie, Tony Hosking and Kai Engelhardt

Apr 13

Concurrent IMP

by Peter Gammie

Apr 13

Trie

by Andreas Lochbihler and Tobias Nipkow

Mar 30

Consensus Refined

by Ognjen Marić and Christoph Sprenger

Mar 18

Deriving class instances for datatypes

by Christian Sternagel and René Thiemann

Mar 11

The Safety of Call Arity

by Joachim Breitner

Feb 20

QR Decomposition

by Jose Divasón and Jesús Aransay

Feb 12

Echelon Form

by Jose Divasón and Jesús Aransay

Feb 12

Finite Automata in Hereditarily Finite Set Theory

by Lawrence C. Paulson

Feb 05

Verification of the UpDown Scheme

by Johannes Hölzl

Jan 28

2014

The Unified Policy Framework (UPF)

by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

Nov 28

Loop freedom of the (untimed) AODV routing protocol

by Timothy Bourke and Peter Höfner

Oct 23

Lifting Definition Option

by René Thiemann

Oct 13

Stream Fusion in HOL with Code Generation

by Andreas Lochbihler and Alexandra Maximova

Oct 10

A Verified Compiler for Probability Density Functions

by Manuel Eberl, Johannes Hölzl and Tobias Nipkow

Oct 09

Formalization of Refinement Calculus for Reactive Systems

by Viorel Preoteasa

Oct 08

XML

by Christian Sternagel and René Thiemann

Oct 03

XML

by Christian Sternagel and René Thiemann

Oct 03

Certification Monads

by Christian Sternagel and René Thiemann

Oct 03

Imperative Insertion Sort

by Christian Sternagel

Sep 25

Priority Queues Based on Braun Trees

by Tobias Nipkow

Sep 04

Gauss-Jordan Algorithm and Its Applications

by Jose Divasón and Jesús Aransay

Sep 03

Skew Heap

by Tobias Nipkow

Aug 13

Splay Tree

by Tobias Nipkow

Aug 12

Haskell's Show Class in Isabelle/HOL

by Christian Sternagel and René Thiemann

Jul 29

Formal Specification of a Generic Separation Kernel

by Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz

Jul 18

pGCL for Isabelle

Jul 13

Amortized Complexity Verified

by Tobias Nipkow

Jul 07

Network Security Policy Verification

by Cornelius Diekmann

Jul 04

Pop-Refinement

by Alessandro Coglio

Jul 03

Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

by Dmitriy Traytel and Tobias Nipkow

Jun 12

Boolean Expression Checkers

by Tobias Nipkow

Jun 08

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

by Peter Lammich

May 28

The CAVA Automata Library

by Peter Lammich

May 28

Promela Formalization

by René Neumann

May 28

Converting Linear-Time Temporal Logic to Generalized Büchi Automata

by Alexander Schimpf and Peter Lammich

May 28

A Fully Verified Executable LTL Model Checker

by Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus

May 28

Transitive closure according to Roy-Floyd-Warshall

by Makarius Wenzel

May 23

Noninterference Security in Communicating Sequential Processes

by Pasquale Noce

May 23

Regular Algebras

by Simon Foster and Georg Struth

May 21

Formalisation and Analysis of Component Dependencies

by Maria Spichkova

Apr 28

A Formalization of Strong Security

by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

Apr 23

A Formalization of Strong Security

by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

Apr 23

A Formalization of Declassification with WHAT-and-WHERE-Security

by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

Apr 23

A Formalization of Declassification with WHAT-and-WHERE-Security

by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

Apr 23

A Formalization of Assumptions and Guarantees for Compositional Noninterference

by Sylvia Grewe, Heiko Mantel and Daniel Schoepe

Apr 23

A Formalization of Assumptions and Guarantees for Compositional Noninterference

by Sylvia Grewe, Heiko Mantel and Daniel Schoepe

Apr 23

Bounded-Deducibility Security

by Andrei Popescu, Peter Lammich and Thomas Bauereiss

Apr 22

A shallow embedding of HyperCTL*

by Markus N. Rabe, Peter Lammich and Andrei Popescu

Apr 16

Syntax and semantics of a GPU kernel programming language

by John Wickerson

Apr 03

Probabilistic Noninterference

by Andrei Popescu and Johannes Hölzl

Mar 11

Mechanization of the Algebra for Wireless Networks (AWN)

by Timothy Bourke

Mar 08

Mutually Recursive Partial Functions

by René Thiemann

Feb 18

Verification of Selection and Heap Sort Using Locales

by Danijela Petrovic

Feb 11

Unified Decision Procedures for Regular Expression Equivalence

by Tobias Nipkow and Dmitriy Traytel

Jan 30

Kleene Algebra with Tests and Demonic Refinement Algebras

by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

Jan 23

Kleene Algebra with Tests and Demonic Refinement Algebras

by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

Jan 23

Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

by Achim D. Brucker, Frédéric Tuong and Burkhart Wolff

Jan 16

Compositional Properties of Crypto-Based Components

by Maria Spichkova

Jan 11

2013

A General Method for the Proof of Theorems on Tail-recursive Functions

by Pasquale Noce

Dec 01

A Codatatype of Formal Languages

by Dmitriy Traytel

Nov 15

Stream Processing Components: Isabelle/HOL Formalisation and Case Studies

by Maria Spichkova

Nov 14

Automatic Data Refinement

by Peter Lammich

Oct 02

Native Word

by Andreas Lochbihler

Sep 17

A Formal Model of IEEE Floating Point Arithmetic

Jul 27

Light-weight Containers

by Andreas Lochbihler

Apr 15

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

by Joachim Breitner

Jan 31

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

by Joachim Breitner

Jan 31

Ribbon Proofs

by John Wickerson

Jan 19

Kleene Algebra

by Alasdair Armstrong, Georg Struth and Tjark Weber

Jan 15

Kleene Algebra

by Alasdair Armstrong, Georg Struth and Tjark Weber

Jan 15

2012

A Separation Logic Framework for Imperative HOL

by Peter Lammich and Rene Meis

Nov 14

Possibilistic Noninterference

by Andrei Popescu and Johannes Hölzl

Sep 10

Possibilistic Noninterference

by Andrei Popescu and Johannes Hölzl

Sep 10

Generating linear orders for datatypes

by René Thiemann

Aug 07

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

by Henri Debrat and Stephan Merz

Jul 27

Logical Relations for PCF

by Peter Gammie

Jul 01

Type Constructor Classes and Monad Transformers

by Brian Huffman

Jun 26

The pi-calculus in nominal logic

by Jesper Bengtson

May 29

Psi-calculi in Isabelle

by Jesper Bengtson

May 29

CCS in nominal logic

by Jesper Bengtson

May 29

Isabelle/Circus

by Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel

May 27

Isabelle/Circus

by Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel

May 27

Separation Algebra

by Gerwin Klein, Rafal Kolanski and Andrew Boyton

May 11

Stuttering Equivalence

by Stephan Merz

May 07

Inductive Study of Confidentiality

by Giampaolo Bella

May 02

Abortable Linearizable Modules

by Rachid Guerraoui, Viktor Kuncak and Giuliano Losa

Mar 01

Executable Transitive Closures

by René Thiemann

Feb 29

Refinement for Monadic Programs

by Peter Lammich

Jan 30

Dijkstra's Shortest Path Algorithm

by Benedikt Nordhoff and Peter Lammich

Jan 30

Markov Models

by Johannes Hölzl and Tobias Nipkow

Jan 03

2011

A Definitional Encoding of TLA* in Isabelle/HOL

by Gudmund Grov and Stephan Merz

Nov 19

Efficient Mergesort

by Christian Sternagel

Nov 09

Algebra of Monotonic Boolean Transformers

by Viorel Preoteasa

Sep 22

The Myhill-Nerode Theorem Based on Regular Expressions

by Chunhan Wu, Xingyuan Zhang and Christian Urban

Aug 26

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

Aug 19

Knowledge-based programs

by Peter Gammie

May 17

Executable Transitive Closures of Finite Relations

by Christian Sternagel and René Thiemann

Mar 14

Infinite Lists

by David Trachtenherz

Feb 23

AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics

by David Trachtenherz

Feb 23

Lightweight Java

by Rok Strniša and Matthew Parkinson

Feb 07

RIPEMD-160

by Fabian Immler

Jan 10

2010

Shivers' Control Flow Analysis

by Joachim Breitner

Nov 16

Functional Binomial Queues

by René Neumann

Oct 28

Finger Trees

by Benedikt Nordhoff, Stefan Körner and Peter Lammich

Oct 28

Binomial Heaps and Skew Binomial Heaps

by Rene Meis, Finn Nielsen and Peter Lammich

Oct 28

Strong Normalization of Moggis's Computational Metalanguage

by Christian Doczkal

Aug 29

Executable Multivariate Polynomials

by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp

Aug 10

Formalizing Statecharts using Hierarchical Automata

by Steffen Helke and Florian Kammüller

Aug 08

Executable Matrix Operations on Matrices of Arbitrary Dimensions

by Christian Sternagel and René Thiemann

Jun 17

Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement

by Viorel Preoteasa and Ralph-Johan Back

May 28

Semantics and Data Refinement of Invariant Based Programs

by Viorel Preoteasa and Ralph-Johan Back

May 28

Regular Sets and Expressions

by Alexander Krauss and Tobias Nipkow

May 12

Locally Nameless Sigma Calculus

by Ludovic Henrio, Florian Kammüller, Bianca Lutz and Henry Sudhof

Apr 30

Inter-Procedural Information Flow Noninterference via Slicing

by Daniel Wasserrab

Mar 23

Information Flow Noninterference via Slicing

by Daniel Wasserrab

Mar 23

List Index

by Tobias Nipkow

Feb 20

Coinductive

by Andreas Lochbihler

Feb 12

2009

Formalizing the Logic-Automaton Connection

by Stefan Berghofer and Markus Reiter

Dec 03

Tree Automata

by Peter Lammich

Nov 25

Collections Framework

by Peter Lammich

Nov 25

Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer

by Daniel Wasserrab

Nov 13

The Worker/Wrapper Transformation

by Peter Gammie

Oct 30

Code Generation for Functions as Data

by Andreas Lochbihler

May 06

Stream Fusion

by Brian Huffman

Apr 29

2008

A Bytecode Logic for JML and Types

by Lennart Beringer and Martin Hofmann

Dec 12

Secure information flow and program logics

by Lennart Beringer and Martin Hofmann

Nov 10

Secure information flow and program logics

by Lennart Beringer and Martin Hofmann

Nov 10

The Textbook Proof of Huffman's Algorithm

by Jasmin Christian Blanchette

Oct 15

Towards Certified Slicing

by Daniel Wasserrab

Sep 16

A Correctness Proof for the Volpano/Smith Security Typing System

by Gregor Snelting and Daniel Wasserrab

Sep 02

A Correctness Proof for the Volpano/Smith Security Typing System

by Gregor Snelting and Daniel Wasserrab

Sep 02

Formal Verification of Modern SAT Solvers

by Filip Marić

Jul 23

BDD Normalisation

by Veronika Ortner and Norbert Schirmer

Feb 29

A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

by Norbert Schirmer

Feb 29

A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

by Norbert Schirmer

Feb 29

Normalization by Evaluation

by Klaus Aehlig and Tobias Nipkow

Feb 18

2007

Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors

by Peter Lammich and Markus Müller-Olm

Dec 14

Jinja with Threads

by Andreas Lochbihler

Dec 03

Much Ado About Two

by Sascha Böhme

Nov 06

POPLmark Challenge Via de Bruijn Indices

by Stefan Berghofer

Aug 02

2006

Hotel Key Card System

by Tobias Nipkow

Sep 09

Abstract Hoare Logics

by Tobias Nipkow

Aug 08

CoreC++

by Daniel Wasserrab

May 15

A Theory of Featherweight Java in Isabelle/HOL

by J. Nathan Foster and Dimitrios Vytiniotis

Mar 31

Instances of Schneider's generalized protocol of clock synchronization

by Damián Barsotti

Mar 15

2005

Fast Fourier Transform

by Clemens Ballarin

Oct 12

Formalization of a Generalized Protocol for Clock Synchronization

Jun 24

Proving the Correctness of Disk Paxos

by Mauro Jaskelioff and Stephan Merz

Jun 22

Jive Data and Store Model

by Nicole Rauch and Norbert Schirmer

Jun 20

Jinja is not Java

by Gerwin Klein and Tobias Nipkow

Jun 01

SHA1, RSA, PSS and more

by Christina Lindenberg and Kai Wirt

May 02

2004

File Refinement

by Karen Zee and Viktor Kuncak

Dec 09

Compiling Exceptions Correctly

by Tobias Nipkow

Jul 09

Depth First Search

by Toshiaki Nishihara and Yasuhiko Minamide

Jun 24

Lazy Lists II

by Stefan Friedrich

Apr 26

Binary Search Trees

by Viktor Kuncak

Apr 05

Functional Automata

by Tobias Nipkow

Mar 30

Mini ML

by Wolfgang Naraschewski and Tobias Nipkow

Mar 19

AVL Trees

by Tobias Nipkow and Cornelia Pusch

Mar 19