Re: [isabelle] Announcement: Verified SAT Solver ISASAT wins EDA Fixed CNF Encoding Race



On Wed, Jul 28, 2021 at 12:07 PM Tobias Nipkow <nipkow at 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!
> >
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.