Dr. Martin Bromberger

Postdoctoral researcher for
Arithmetic Reasoning

 

Max-Planck-Institut für Informatik
Campus E1 4
66123 Saarbrücken

+49 681 9325-2922, fax -2999

mbromber@mpi-inf.mpg.de

 

Physical address: building E1 5, room 634

Personal Information

Research Interests

  • (Linear) Arithmetic Decision Procedures
  • Theorem Proving
  • Combination of Theories
  • Parsing

Academic Activities

Teaching

Recent Positions

Education

  • July 2014 - December 2019:
    PhD student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany and the Max-Planck-Institut für Informatik
    December 2019: finished PhD in Computer Science (Dr. rer. nat.); thesis title: Decision Procedures for Linear Arithmetic
  • October 2012 - July 2014:
    Student in the preparatory phase of the Graduate School of Computer Science at Universität des Saarlandes, Saarbrücken, Germany
  • October 2009 - March 2016:
    Bachelor and Master student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany
    Oct. 2010: finished BSc in Computer Science; thesis title: Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic (supervisor: Prof. Dr. Christoph Weidenbach)
    Mar. 2016: finished MSc in Computer Science; thesis title: Analysis and Implementation of LIA Solvers: CutSAT and BBSAT (supervisor: Prof. Dr. Christoph Weidenbach)

Software Projects

SPASS

Wrote the parser for SPASS version 3.9

SPASS-IQ

Main developer of the linear arithmetic theory solver SPASS-IQ

SPASS-SATT

Main developer of the CDCL(LA) solver SPASS-SATT

Awards:

SMT-COMP 2018 (13th International Satisfiability Modulo Theories Competition)
  • First Place in the main track in the QF_LIA division
  • Best Newcomer Award
SMT-COMP 2019 (14th International Satisfiability Modulo Theories Competition)
  • First Place in the single query track in the QF_LRA (Seq.) division

Publications

  • A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic, Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach. To appear in the proceedings of TACAS 2022. Springer, 2022. Author's version (PDF);
  • A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic, Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach. In FroCoS 2021, volume 12941 of LNCS, pages 3–24. Springer, 2021.
  • Decision Procedures for Linear Arithmetic, Martin Bromberger. PhD thesis (submitted in July 2019, defended in December 2019).
    DOI: 10.22028/D291-30636; PDF version; (***Dr.-Eduard-Martin-Preis***)