Martin Bromberger

28 papers A 8B 3Journal 9Unranked 7

Year	Rank	Type	Title / Venue / Authors
2025	A	`conf`	A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. CADE Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2024	B	`conf`	Automatic Bit- and Memory-Precise Verification of eBPF Code. LPAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2024	—	`conf`	First-Order Automatic Literal Model Generation. IJCAR (1) Martin Bromberger, Florent Krasnopol, Sibylle Möhle, Christoph Weidenbach
2023	A	`conf`	An Isabelle/HOL Formalization of the SCL(FOL) Calculus. CADE Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2023	B	`conf`	Exploring Partial Models with SCL. LPAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2023	A	`conf`	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CADE Martin Bromberger, Chaahat Jain, Christoph Weidenbach
2023	J	`jnl`	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. CoRR Martin Bromberger, Chaahat Jain, Christoph Weidenbach
2023	J	`jnl`	SCL(FOL) Revisited. CoRR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2023	—	`conf`	Symbolic Model Construction for Saturated Constrained Horn Clauses. FroCoS Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2023	J	`jnl`	Symbolic Model Construction for Saturated Constrained Horn Clauses. CoRR Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2022	—	`conf`	A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. TACAS (1) Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach
2022	J	`jnl`	A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach
2022	—	`conf`	A Two-Watched Literal Scheme for First-Order Logic. PAAR@IJCAR Martin Bromberger, Tobias Gehl, Lorenz Leutgeb, Christoph Weidenbach
2022	A	`conf`	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. IJCAR Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
2022	—	`conf`	Exploring Partial Models with SCL. PAAR@IJCAR Martin Bromberger, Simon Schwarz, Christoph Weidenbach
2021	—	`conf`	A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. FroCoS Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
2021	J	`jnl`	A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. CoRR Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
2021	B	`conf`	Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. VMCAI Martin Bromberger, Alberto Fiori, Christoph Weidenbach
2020	J	`jnl`	A complete and terminating approach to linear integer solving. J. Symb. Comput. Martin Bromberger, Thomas Sturm, Christoph Weidenbach
2019	—	`—`	Decision Procedures for Linear Arithmetic. (Quelques procédures de décision pour l'arithmétique linéaire). Martin Bromberger
2019	A	`conf`	SPASS-SATT - A CDCL(LA) Solver. CADE Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach
2018	A	`conf`	A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. IJCAR Martin Bromberger
2018	J	`jnl`	A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. CoRR Martin Bromberger
2017	J	`jnl`	New techniques for linear arithmetic: cubes and equalities. Formal Methods Syst. Des. Martin Bromberger, Christoph Weidenbach
2016	—	`conf`	Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. SMT@IJCAR Martin Bromberger, Christoph Weidenbach
2016	A	`conf`	Fast Cube Tests for LIA Constraint Solving. IJCAR Martin Bromberger, Christoph Weidenbach
2015	A	`conf`	Linear Integer Arithmetic Revisited. CADE Martin Bromberger, Thomas Sturm, Christoph Weidenbach
2015	J	`jnl`	Linear Integer Arithmetic Revisited. CoRR Martin Bromberger, Thomas Sturm, Christoph Weidenbach