TNF / INF
[ research |
publications | talks | software |
awards | office | contact |
Dipl.-Ing. Dr. Aina Niemetz
From June 2012 to April 2017 I was a Ph.D. student in Computer
Science at FMV, supervised by Prof. Armin Biere within the National
Research Network (NFN) on Rigorous
Systems Engineering (RiSE).
I am one of the developers of our SMT solver Boolector and I am mainly working
on quantifier-free bit-vectors.
A list of my publications can be found here: Publications
- Satisfiability Modulo Theories (SMT)
- Automated Testing and Debugging Techniques
- Quantified Boolean Formulas (QBF)
- Precise and
Complete Propagation Based Local Search for Satisfiability Modulo
Theories, CAV 2016, Toronto, Ontario, Canada.
Local Search for Bit-Vector Logics with Path Propagation, DIFTS
2015, Austin, TX, USA.
Lemmas on Demand with Don't Care Reasoning, FMCAD 2014,
- ddSMT: A Delta
Debugger for the SMT-LIB v2 Format, SMT Workshop 2013,
Certificate Extraction for QBF (Tool Presentation), SAT'12,
My work in Boolector
contributed to the following awards:
- Boolector, an SMT
solver for bit-vectors and arrays.
- ddSMT, a delta debugger
for the SMT-LIB v2 format.
- QRPcheck, a tool for
extracting and checking resolution proofs of (un)satisfiability in
- QxBF, a QBF preprocessor
based on failed literal detection.
- QBFDD, a delta-debugger
for QBF in QDIMACS format.
Science Park 3 (SCP3), 2nd
+43 732 2468 4549 (phone)
Institute for Formal Models and Verification
Johannes Kepler University