[  research | publications | talks | awards | teaching | fotos | office | contact | address ]

DI Dr. Robert Brummayer

Assistant

I was a research and teaching assistant at FMV, supervised by Prof. Armin Biere. I received my Ph.D. in "formal methods in computer science" from the Johannes Kepler University Linz in November 2009. I am now at DMCE.

My main research project has been Boolector, which is an Satisfiability Modulo Theories (SMT) solver for bit-vectors and arrays. Recently, I have also been working on testing and debugging tools for SMT and ASP solver development. If you are interested in SMT solving and SMT solver development, then you might want to read my Ph.D. thesis.

Research interests

• Satisfiability Modulo Theories (SMT)
• Formal Verification
• Fuzz Testing
• Delta-Debugging
• And-Inverter Graphs
• SAT

Publications

Talks

• Automated Testing and Debugging of SAT and QBF Solvers, SAT'10, Edinburgh, UK
• Fuzzing and Delta-Debugging SMT Solvers, SMT'09, Montreal, Canada
• Boolector 1.2, SMT-COMP'09, Montreal, Canada
• Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, TACAS'09, York, UK
• Effective Bit-Width and Under-Approximation, Eurocast'09, Las Palmas de Gran Canaria, Spain
• BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking, BPR'08, Princeton, New Jersey, USA
• Lemmas on Demand for the Extensional Theory of Arrays, SMT'08, Princeton, New Jersey, USA
• Boolector 0.4, SMT-COMP'08, Princeton, New Jersey, USA
• Offline SMT for Arrays, AVM'08, Semmering, Austria
• C32SAT: Checking C Expressions, CAV'07, Berlin, Germany

Awards

• Best Student BPR Paper Award (sponsored by Fortify Software), R. Brummayer, A. Biere and F. Lonsing. BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking, BPR'08, Princeton, New Jersey, USA, July 2008.

Teaching activities

• Systems Programming
• Formale Modelle (Formale Grundlagen 3)
• Model Checking
• Softwareentwicklung 1 (Wirtschaftsinformatik)
• Spezielle Kapitel aus Informatik: Pthreads Programming in C

Fotos

Office

TNF Tower, 7th Floor, North-West Wing
+43 732 2468 8894 (phone)
Room T0758

Contact

robert.brummayer@gmail.com
https://fmv.jku.at/brummayer
+43 732 2468 8893 (fax)

Address

Institute for Formal Models and Verification
Johannes Kepler University
Altenbergerstr. 69
4040 Linz
Austria