A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL by Katherine Kosaian, Yong Kiam Tan and André Platzer Dec 15
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
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles by Albert Rizaldi and Fabian Immler Jun 01
A verified LLL algorithm by Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada Feb 02
Homogeneous Linear Diophantine Equations by Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel Oct 14
Executable Multivariate Polynomials by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp Aug 10