Thiemann, René Bottesch, Ralph Divasón, Jose Haslbeck, Max W. Joosten, Sebastiaan J. C. Yamada, Akihisa
Published in
Journal of Automated Reasoning

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number...

Beyersdorff, Olaf Blinkhorn, Joshua Mahajan, Meena
Published in
Journal of Automated Reasoning

Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple oper...

Joosten, Sebastiaan J C Thiemann, René Yamada, Akihisa
Published in
Journal of automated reasoning

We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injecti...

Heule, Marijn J H Kiesl, Benjamin Biere, Armin
Published in
Journal of automated reasoning

We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that their addition preserves satisfiability. To guaran...

Li, Wenda Paulson, Lawrence C.

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximat...

Divasón, Jose Joosten, Sebastiaan J. C. Thiemann, René Yamada, Akihisa
Published in
Journal of Automated Reasoning

We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm f...

Besson, Frédéric Blazy, Sandrine Wilke, Pierre
Published in
Journal of Automated Reasoning

The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging f...

Zhang, Xingyuan Urban, Christian
Published in
Journal of Automated Reasoning

Charguéraud, Arthur Pottier, François
Published in
Journal of Automated Reasoning

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is nontrivial. We present a Coq formalization of this analysis, following Alstrup et al.’s recent proof. Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional ...

Mahboubi, Assia Melquiond, Guillaume Sibut-Pinote, Thomas
Published in
Journal of Automated Reasoning

Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Y...