Computer science/Algorithms

Subject Classification

ACM: Theory of computation~Design and analysis of algorithms

AMS: Computer science / Algorithms in computer science

2026

Nominal Unification

by Guilherme Borges Brandão, Thomas Ammer, Daniele Nantes Sobrinho, Mauricio Ayala-Rinción, Christian Urban, Maribel Fernández and Mohammad Abdulaziz

Apr 23

Concentrated Liquidity Market Making Operations

by Mnacho Echenim

Jan 30

2025

Set Reconciliation

by Paul Hofmeier and Emin Karayel

Dec 03

Formalised Burrows-Wheeler Transform

by Louis Cheung and Christine Rizkallah

Jan 17

2024

Formally Verified Suffix Array Construction

by Louis Cheung and Christine Rizkallah

Sep 25

The Karatsuba Square Root Algorithm

by Manuel Eberl

Sep 18

Parallel Shear Sort

by Manuel Eberl and Peter Lammich

Sep 17

Alpha-Beta Pruning

by Tobias Nipkow

Jun 13

Formalizing Coppersmith's Method

by Katherine Kosaian and Yong Kiam Tan

Jun 10

Partial Correctness of the Top-Down Solver

by Yannick Stade, Sarah Tilscher and Helmut Seidl

May 09

LL(1) Parser Generator

by Sarah Tilscher and Simon Wimmer

May 02

A Verified Proof Checker for Metric First-Order Temporal Logic

by Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima, Martin Raszyk and Dmitriy Traytel

Apr 16

Verified QBF Solving

by Axel Bergström and Tjark Weber

Mar 06

Karatsuba Multiplication on Integers

by Jakob Schulz and Emin Karayel

Feb 19

2023

Knuth–Morris–Pratt String Search

by Lawrence C. Paulson

Nov 27

Earley Parser

by Martin Rau

Jul 16

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

2022

Combinatorial Enumeration Algorithms

by Paul Hofmeier and Emin Karayel

Nov 11

Maximum Segment Sum

by Nils Cremer

Sep 29

Verified Complete Test Strategies for Finite State Machines

by Robert Sachtleben

Aug 09

A Combinator Library for Prefix-Free Codes

by Emin Karayel

Apr 08

Multi-Head Monitoring of Metric Dynamic Logic

by Martin Raszyk

Feb 13

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

Regression Test Selection

by Susannah Mansky

Apr 30

2020

Practical Algebraic Calculus Checker

by Mathias Fleury and Daniela Kaufmann

Aug 31

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

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

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

by Joshua Schneider and Dmitriy Traytel

Jul 04

Binary Heaps for IMP2

by Simon Griebel

Jun 13

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

by Bohua Zhan

Dec 21

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

VerifyThis 2018 - Polished Isabelle Solutions

by Peter Lammich and Simon Wimmer

Apr 27

First-Order Terms

by Christian Sternagel and René Thiemann

Feb 06

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 number of comparisons in QuickSort

by Manuel Eberl

Mar 15

Lower bound on comparison-based sorting algorithms

by Manuel Eberl

Mar 15

2016

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

2015

The Tortoise and Hare Algorithm

by Peter Gammie

Nov 18

2014

Imperative Insertion Sort

by Christian Sternagel

Sep 25

Boolean Expression Checkers

by Tobias Nipkow

Jun 08

Verification of Selection and Heap Sort Using Locales

by Danijela Petrovic

Feb 11

2011

Efficient Mergesort

by Christian Sternagel

Nov 09

2008

Formal Verification of Modern SAT Solvers

by Filip Marić

Jul 23

2007

Much Ado About Two

by Sascha Böhme

Nov 06