This is the website for my hobby project, Minkeyrink, tools which reasons about software.
Currently, the only tool that I publically release is the open-source STP solver. For many types of software verification problems, STP is the fastest available solver.
I've been working on bit-vector and array solvers since 2008. I was awarded my PhD in 2012 for a dissertation describing contributions to bit-vector and array solving.
Since 2009, I've entered solvers in the annual SMTCOMP in the quantifier-free bit-vector solver division. Finishing with some kind of first place in 2022 with STP, 2021 with STP, 2018 with Minkeyrink Solver, 2017 with Minkeyrink Solver and 2010 with simplifyingSTP.
Typically quantifier-free, array and bit-vector solvers are used to efficiently solve problems generated by software verification tools. But their use is more general because lots of problems can be expressed as these via the SMTLIB2 format.
The solvers I develop all reduce bit-vector and array problems to boolean satisfiability(SAT) problems, then pass them onto a SAT solver. Before being passed to the SAT solver, rewriting, at various levels, is the most important technique to speed up solving. Given the significance of rewriting, and that the only formal description of how rewriting is applied in these solvers is in my PhD thesis, I'm working to describe it better.