Linear Integer Arithmetic Revisited. - Martin Bromberger; Thomas Sturm 001; Christoph Weidenbach (CADE, 2015)

Fast Cube Tests for LIA Constraint Solving. - Martin Bromberger; Christoph Weidenbach (IJCAR, 2016)

Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. - Martin Bromberger; Christoph Weidenbach (SMT@IJCAR, 2016)

New techniques for linear arithmetic: cubes and equalities. - Martin Bromberger; Christoph Weidenbach (Formal Methods Syst. Des., 2017)

A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. - Martin Bromberger (IJCAR, 2018)

SPASS-SATT - A CDCL(LA) Solver. - Martin Bromberger; Mathias Fleury; Simon Schwarz; Christoph Weidenbach (CADE, 2019)

Decision Procedures for Linear Arithmetic. (Quelques procédures de décision pour l'arithmétique linéaire). - Martin Bromberger (2019)

A complete and terminating approach to linear integer solving. - Martin Bromberger; Thomas Sturm 001; Christoph Weidenbach (J. Symb. Comput., 2020)

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. - Martin Bromberger; Irina Dragoste; Rasha Faqeh; Christof Fetzer; Markus Krötzsch; Christoph Weidenbach (FroCoS, 2021)

Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. - Martin Bromberger; Alberto Fiori; Christoph Weidenbach (VMCAI, 2021)

An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. - Martin Bromberger; Lorenz Leutgeb; Christoph Weidenbach (IJCAR, 2022)

A Two-Watched Literal Scheme for First-Order Logic. - Martin Bromberger; Tobias Gehl; Lorenz Leutgeb; Christoph Weidenbach (PAAR@IJCAR, 2022)

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 001; Harish K. Murali; Christoph Weidenbach (TACAS (1), 2022)

An Isabelle/HOL Formalization of the SCL(FOL) Calculus. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2023)

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. - Martin Bromberger; Chaahat Jain; Christoph Weidenbach (CADE, 2023)

Symbolic Model Construction for Saturated Constrained Horn Clauses. - Martin Bromberger; Lorenz Leutgeb; Christoph Weidenbach (FroCoS, 2023)

Exploring Partial Models with SCL. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (LPAR, 2023)

SCL(FOL) Revisited. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (CoRR, 2023)

First-Order Automatic Literal Model Generation. - Martin Bromberger; Florent Krasnopol; Sibylle Möhle; Christoph Weidenbach (IJCAR (1), 2024)

Automatic Bit- and Memory-Precise Verification of eBPF Code. - Martin Bromberger; Simon Schwarz; Christoph Weidenbach (LPAR, 2024)

A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2025)