Computer science/Algorithms/Mathematical

2024

Babai's Nearest Plane Algorithm

by Eric Ren, Sage Binder and Katherine Kosaian

Sep 26

A Preprocessor for Linear Diophantine Equalities and Inequalities

by René Thiemann

Jun 13

Schönhage-Strassen Multiplication

by Jakob Schulz

May 10

Karatsuba Multiplication on Integers

by Jakob Schulz and Emin Karayel

Feb 19

2023

Gray Codes for Arbitrary Numeral Systems

by Maximilian Spitz

Jul 11

2022

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

by Katherine Kosaian, Yong Kiam Tan and André Platzer

Dec 15

Number Theoretic Transform

by Thomas Ammer and Katharina Kreuzer

Aug 18

Enumeration of Equivalence Relations

by Emin Karayel

Feb 04

2021

Verified Quadratic Virtual Substitution for Real Arithmetic

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

Oct 02

The BKR Decision Procedure for Univariate Real Arithmetic

by Katherine Kosaian, Yong Kiam Tan and André Platzer

Apr 24

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

2020

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

2018

Signature-Based Gröbner Basis Algorithms

by Alexander Maletzky

Sep 20

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

Homogeneous Linear Diophantine Equations

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

Oct 14

2016

Gröbner Bases Theory

by Fabian Immler and Alexander Maletzky

May 02

2015

Hermite Normal Form

by Jose Divasón and Jesús Aransay

Jul 07

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

Gauss-Jordan Algorithm and Its Applications

by Jose Divasón and Jesús Aransay

Sep 03

2011

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

Aug 19

2010

Executable Multivariate Polynomials

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

Aug 10

2005

Fast Fourier Transform

by Clemens Ballarin

Oct 12