TNF / INF
[ research |
publications | talks | software |
awards | office | contact |
Dipl.-Ing. Dr. Mathias Preiner
From June 2012 to April 2017 I was a computer science Ph.D.
student within the National Research Network (NFN) on Rigorous Systems Engineering
(RiSE), supervised by Prof. Armin Biere at FMV. From April 2017
until June 2017 I continued my research at FMV as a postdoctoral
researcher. Since June 2017 I am a postdoctoral scholar at Stanford University working on CVC4 in Clark Barrett's group. I
am one of the developers and maintainers of the SMT solver Boolector.
A list of my publications can be found here: Publications
- Satisfiability Modulo Theories (SMT)
- Automated Testing and Debugging Techniques
- Better Lemmas
with Lambda Extraction, FMCAD'15, Austin, Texas, USA
- Lemmas on
Demand for Lambdas, DIFTS'13, Portland, Oregon, USA
Certificate Extraction for QBF, AVM'12, Passau, Germany
My work in boolector
contributed to the following awards:
- Boolector, an SMT
solver for bit-vectors and arrays.
- QRPcert, a tool for
extracting Skolem/Herbrand function-based QBF certificates.
- CertCheck, a tool
for validating QBF certificates extracted by QRPcert.
- QxBF, a QBF preprocessor
based on failed literal detection.
- QBFuzz, a fuzzer for
generating random QBF formulae.
Science Park 3 (SCP3), 2nd
Institute for Formal Models and Verification
Johannes Kepler University