Email Gateway (Jul 28 2021 at 10:51): Email Gateway (Jul 28 2021 at 10:51):From: Peter Lammich <lammich@in.tum.de>
The SAT solver ISASAT by Mathias Fleury has won the
EDA Fixed CNF Encoding Race, a competition affiliated with this years
SAT conference.
Except for parsing of the input and printing of results, full
functional correctness of this solver is verified, down to LLVM
intermediate code,
using Isabelle/LLVM.
As far as I know, this was the only formally verified solver in the
field!
Email Gateway (Jul 28 2021 at 11:04):From: Tobias Nipkow <nipkow@in.tum.de>
Mathias, congratulations, this is just amazing! Formal verification triumphs
over hackery - let there be light! And thanks to Peter for all of his refinement
tools down to LLVM.
Tobias
smime.p7s
Email Gateway (Jul 28 2021 at 21:12):From: Andrei Popescu <andrei.h.popescu@gmail.com>
On Wed, Jul 28, 2021 at 12:07 PM Tobias Nipkow <nipkow@in.tum.de> wrote:
Mathias, congratulations, this is just amazing! Formal verification triumphs
over hackery - let there be light!
Indeed. :-) Congrats, Mathias and Peter, awesome achievement!
Best wishes,
Andrei
And thanks to Peter for all of his refinement
tools down to LLVM.Tobias
On 28/07/2021 12:50, Peter Lammich wrote:
The SAT solver ISASAT <https://m-fleury.github.io/isasat/isasat.html> by Mathias
Fleury has won the EDA Fixed CNF Encoding Race <https://www.eda-ai.org/>, a
competition affiliated with this years SAT conference.Except for parsing of the input and printing of results, full functional
correctness of this solver is verified, down to LLVM intermediate code,
using Isabelle/LLVM <https://www21.in.tum.de/~lammich/isabelle_llvm/>.As far as I know, this was the only formally verified solver in the field!
Last updated: Jul 15 2022 at 23:21 UTC