Travelled to:
1 × Italy
Collaborated with:
A.Niemetz A.Biere A.Reynolds C.W.Barrett C.Tinelli C.Wolf F.Lonsing M.Seidl Y.Zohar M.Brain
Talks about:
invert (2) condit (2) btor (2) base (2) bit (2) boolector (1) quantifi (1) independ (1) satisfi (1) resolut (1)
Person: Mathias Preiner
DBLP: Preiner:Mathias
Contributed to:
Wrote 6 papers:
- SAT-2012-NiemetzPLSB
- Resolution-Based Certificate Extraction for QBF — (AN, MP, FL, MS, AB), pp. 430–435.
- CAV-2016-NiemetzPB #modulo theories #precise #satisfiability
- Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (AN, MP, AB), pp. 199–217.
- CAV-2018-NiemetzPWB
- Btor2 , BtorMC and Boolector 3.0 (AN, MP, CW, AB), pp. 587–595.
- CAV-2018-NiemetzPRBT #quantifier #using
- Solving Quantified Bit-Vectors Using Invertibility Conditions (AN, MP, AR, CWB, CT), pp. 236–255.
- CADE-2019-NiemetzPRZBT #independence #proving #smt #towards
- Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
- CAV-2019-BrainNPRBT #float
- Invertibility Conditions for Floating-Point Formulas (MB, AN, MP, AR, CWB, CT), pp. 116–136.