Computer Science/Algorithms

Subject Classification

ACM: Theory of computation~Design and analysis of algorithms

AMS: Computer science / Algorithms in computer science

2023

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

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

Tree Enumeration

May 09

The Schwartz-Zippel Lemma

by Sunpill Kim and Yong Kiam Tan

Apr 27

Distributed Distinct Elements

by Emin Karayel

Apr 03

Distributed Distinct Elements

by Emin Karayel

Apr 03

Distributed Distinct Elements

by Emin Karayel

Apr 03

Expander Graphs

by Emin Karayel

Mar 03

Expander Graphs

by Emin Karayel

Mar 03

2022

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

by Katherine Kosaian, Yong Kiam Tan and André Platzer

Dec 15

Combinatorial Enumeration Algorithms

by Paul Hofmeier and Emin Karayel

Nov 11

Maximum Segment Sum

Sep 29

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

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

Universal Hash Families

by Emin Karayel

Feb 20

Multi-Head Monitoring of Metric Dynamic Logic

by Martin Raszyk

Feb 13

Enumeration of Equivalence Relations

by Emin Karayel

Feb 04

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

Quantum and Classical Registers

by Dominique Unruh

Oct 28

Verified Quadratic Virtual Substitution for Real Arithmetic

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

Oct 02

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

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

2020

Relational Minimum Spanning Tree Algorithms

by Walter Guttmann and Nicolas Robinson-O’Brien

Dec 08

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

by Anthony Bordg, Hanna Lachnitt and Yijun He

Nov 22

Practical Algebraic Calculus Checker

by Mathias Fleury and Daniela Kaufmann

Aug 31

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

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

Strong Eventual Consistency of the Collaborative Editing Framework WOOT

by Emin Karayel and Edgar Gonzàlez

Mar 25

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

2019

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

by Pasquale Noce

Dec 04

VerifyThis 2019 -- Polished Isabelle Solutions

by Peter Lammich and Simon Wimmer

Oct 16

Formalization of Multiway-Join Algorithms

by Thibault Dardinier

Sep 16

Formalisation of an Adaptive State Counting Algorithm

by Robert Sachtleben

Aug 16

Stellar Quorum Systems

by Giuliano Losa

Aug 01

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

Binary Heaps for IMP2

by Simon Griebel

Jun 13

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

The Inversions of a List

by Manuel Eberl

Feb 01

IMP2 – Simple Program Verification in Isabelle/HOL

by Peter Lammich and Simon Wimmer

Jan 15

2018

Verifying Imperative Programs using Auto2

Dec 21

Randomised Binary Search Trees

by Manuel Eberl

Oct 19

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

Optimal Binary Search Trees

by Tobias Nipkow and Dániel Somogyi

May 27

Hidden Markov Models

by Simon Wimmer

May 25

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

VerifyThis 2018 - Polished Isabelle Solutions

by Peter Lammich and Simon Wimmer

Apr 27

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

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

The IMAP CmRDT

by Tim Jungnickel, Lennart Oldenburg and Matthias Loibl

Nov 09

Homogeneous Linear Diophantine Equations

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

Oct 14

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

The Floyd-Warshall Algorithm for Shortest Paths

by Simon Wimmer and Peter Lammich

May 08

Probabilistic while loop

by Andreas Lochbihler

May 05

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

2016

Fisher–Yates shuffle

by Manuel Eberl

Sep 30

Formalizing the Edmonds-Karp Algorithm

by Peter Lammich and S. Reza Sefidgar

Aug 12

A Framework for Verifying Depth-First Search Algorithms

by Peter Lammich and René Neumann

Jul 05

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

A formalisation of the Cocke-Younger-Kasami algorithm

by Maksym Bortin

Apr 27

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

2015

The Tortoise and Hare Algorithm

by Peter Gammie

Nov 18

Hermite Normal Form

by Jose Divasón and Jesús Aransay

Jul 07

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

by Peter Gammie, Tony Hosking and Kai Engelhardt

Apr 13

Consensus Refined

by Ognjen Marić and Christoph Sprenger

Mar 18

QR Decomposition

by Jose Divasón and Jesús Aransay

Feb 12

Echelon Form

by Jose Divasón and Jesús Aransay

Feb 12

Verification of the UpDown Scheme

by Johannes Hölzl

Jan 28

2014

Imperative Insertion Sort

by Christian Sternagel

Sep 25

Gauss-Jordan Algorithm and Its Applications

by Jose Divasón and Jesús Aransay

Sep 03

Boolean Expression Checkers

by Tobias Nipkow

Jun 08

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

by Peter Lammich

May 28

Transitive closure according to Roy-Floyd-Warshall

by Makarius Wenzel

May 23

Verification of Selection and Heap Sort Using Locales

by Danijela Petrovic

Feb 11

2012

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

by Henri Debrat and Stephan Merz

Jul 27

Abortable Linearizable Modules

by Rachid Guerraoui, Viktor Kuncak and Giuliano Losa

Mar 01

Executable Transitive Closures

by René Thiemann

Feb 29

Dijkstra's Shortest Path Algorithm

by Benedikt Nordhoff and Peter Lammich

Jan 30

2011

Efficient Mergesort

by Christian Sternagel

Nov 09

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

Aug 19

Executable Transitive Closures of Finite Relations

by Christian Sternagel and René Thiemann

Mar 14

2010

Executable Multivariate Polynomials

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

Aug 10

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

by Viorel Preoteasa and Ralph-Johan Back

May 28

2008

Formal Verification of Modern SAT Solvers

by Filip Marić

Jul 23

2007

Much Ado About Two

by Sascha Böhme

Nov 06

2006

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

2004

Depth First Search

by Toshiaki Nishihara and Yasuhiko Minamide

Jun 24