Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Martin Bromberger
@inproceedings{DBLP:conf/cade/BrombergerDW23,
author = {Martin Bromberger and
Martin Desharnais and
Christoph Weidenbach},
editor = {Brigitte Pientka and
Cesare Tinelli},
title = {An Isabelle/HOL Formalization of the {SCL(FOL)} Calculus},
booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on
Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14132},
pages = {116--133},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38499-8\_7},
doi = {10.1007/978-3-031-38499-8\_7},
timestamp = {Thu, 14 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrombergerDW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrombergerJW23,
author = {Martin Bromberger and
Chaahat Jain and
Christoph Weidenbach},
editor = {Brigitte Pientka and
Cesare Tinelli},
title = {{SCL(FOL)} Can Simulate Non-Redundant Superposition Clause Learning},
booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on
Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14132},
pages = {134--152},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38499-8\_8},
doi = {10.1007/978-3-031-38499-8\_8},
timestamp = {Tue, 12 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrombergerJW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BrombergerLW23,
author = {Martin Bromberger and
Lorenz Leutgeb and
Christoph Weidenbach},
editor = {Uli Sattler and
Martin Suda},
title = {Symbolic Model Construction for Saturated Constrained Horn Clauses},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS
2023, Prague, Czech Republic, September 20-22, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14279},
pages = {137--155},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_8},
doi = {10.1007/978-3-031-43369-6\_8},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/frocos/BrombergerLW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BrombergerSW23,
author = {Martin Bromberger and
Simon Schwarz and
Christoph Weidenbach},
editor = {Ruzica Piskac and
Andrei Voronkov},
title = {Exploring Partial Models with {SCL}},
booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning, Manizales,
Colombia, 4-9th June 2023},
series = {EPiC Series in Computing},
volume = {94},
pages = {48--72},
publisher = {EasyChair},
year = {2023},
url = {https://doi.org/10.29007/8br1},
doi = {10.29007/8BR1},
timestamp = {Wed, 12 Jul 2023 16:50:32 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BrombergerSW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2302-05954,
author = {Martin Bromberger and
Simon Schwarz and
Christoph Weidenbach},
title = {{SCL(FOL)} Revisited},
journal = {CoRR},
volume = {abs/2302.05954},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2302.05954},
doi = {10.48550/ARXIV.2302.05954},
eprinttype = {arXiv},
eprint = {2302.05954},
timestamp = {Sun, 19 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2302-05954.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2305-05064,
author = {Martin Bromberger and
Lorenz Leutgeb and
Christoph Weidenbach},
title = {Symbolic Model Construction for Saturated Constrained Horn Clauses},
journal = {CoRR},
volume = {abs/2305.05064},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2305.05064},
doi = {10.48550/ARXIV.2305.05064},
eprinttype = {arXiv},
eprint = {2305.05064},
timestamp = {Mon, 18 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2305-05064.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2305-12926,
author = {Martin Bromberger and
Chaahat Jain and
Christoph Weidenbach},
title = {{SCL(FOL)} Can Simulate Non-Redundant Superposition Clause Learning},
journal = {CoRR},
volume = {abs/2305.12926},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2305.12926},
doi = {10.48550/ARXIV.2305.12926},
eprinttype = {arXiv},
eprint = {2305.12926},
timestamp = {Fri, 26 May 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2305-12926.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrombergerLW22,
author = {Martin Bromberger and
Lorenz Leutgeb and
Christoph Weidenbach},
editor = {Jasmin Blanchette and
Laura Kov{\'{a}}cs and
Dirk Pattinson},
title = {An Efficient Subsumption Test Pipeline for {BS(LRA)} Clauses},
booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
2022, Haifa, Israel, August 8-10, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13385},
pages = {147--168},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-10769-6\_10},
doi = {10.1007/978-3-031-10769-6\_10},
timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrombergerLW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/paar/BrombergerGLW22,
author = {Martin Bromberger and
Tobias Gehl and
Lorenz Leutgeb and
Christoph Weidenbach},
editor = {Boris Konev and
Claudia Schon and
Alexander Steen},
title = {A Two-Watched Literal Scheme for First-Order Logic},
booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning
Co-located with the 11th International Joint Conference on Automated
Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3201},
publisher = {CEUR-WS.org},
year = {2022},
url = {https://ceur-ws.org/Vol-3201/paper2.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:34 +0100},
biburl = {https://dblp.org/rec/conf/paar/BrombergerGLW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/paar/BrombergerSW22,
author = {Martin Bromberger and
Simon Schwarz and
Christoph Weidenbach},
editor = {Boris Konev and
Claudia Schon and
Alexander Steen},
title = {Exploring Partial Models with {SCL}},
booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning
Co-located with the 11th International Joint Conference on Automated
Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3201},
publisher = {CEUR-WS.org},
year = {2022},
url = {https://ceur-ws.org/Vol-3201/paper5.pdf},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/paar/BrombergerSW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BrombergerDFFGK22,
author = {Martin Bromberger and
Irina Dragoste and
Rasha Faqeh and
Christof Fetzer and
Larry Gonz{\'{a}}lez and
Markus Kr{\"{o}}tzsch and
Maximilian Marx and
Harish K. Murali and
Christoph Weidenbach},
editor = {Dana Fisman and
Grigore Rosu},
title = {A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo
Simple Linear Arithmetic},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 28th International Conference, {TACAS} 2022, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {13243},
pages = {480--501},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-030-99524-9\_27},
doi = {10.1007/978-3-030-99524-9\_27},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BrombergerDFFGK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2201-09769,
author = {Martin Bromberger and
Irina Dragoste and
Rasha Faqeh and
Christof Fetzer and
Larry Gonz{\'{a}}lez and
Markus Kr{\"{o}}tzsch and
Maximilian Marx and
Harish K. Murali and
Christoph Weidenbach},
title = {A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo
Simple Linear Arithmetic},
journal = {CoRR},
volume = {abs/2201.09769},
year = {2022},
url = {https://arxiv.org/abs/2201.09769},
eprinttype = {arXiv},
eprint = {2201.09769},
timestamp = {Tue, 01 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2201-09769.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BrombergerDFFKW21,
author = {Martin Bromberger and
Irina Dragoste and
Rasha Faqeh and
Christof Fetzer and
Markus Kr{\"{o}}tzsch and
Christoph Weidenbach},
editor = {Boris Konev and
Giles Reger},
title = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple
Linear Arithmetic},
booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS
2021, Birmingham, UK, September 8-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12941},
pages = {3--24},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-86205-3\_1},
doi = {10.1007/978-3-030-86205-3\_1},
timestamp = {Fri, 03 Sep 2021 16:17:39 +0200},
biburl = {https://dblp.org/rec/conf/frocos/BrombergerDFFKW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/BrombergerFW21,
author = {Martin Bromberger and
Alberto Fiori and
Christoph Weidenbach},
editor = {Fritz Henglein and
Sharon Shoham and
Yakir Vizel},
title = {Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference
Constraints by Simple Clause Learning over Theories},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 22nd International
Conference, {VMCAI} 2021, Copenhagen, Denmark, January 17-19, 2021,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12597},
pages = {511--533},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-67067-2\_23},
doi = {10.1007/978-3-030-67067-2\_23},
timestamp = {Wed, 13 Jan 2021 17:58:39 +0100},
biburl = {https://dblp.org/rec/conf/vmcai/BrombergerFW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2107-03189,
author = {Martin Bromberger and
Irina Dragoste and
Rasha Faqeh and
Christof Fetzer and
Markus Kr{\"{o}}tzsch and
Christoph Weidenbach},
title = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple
Linear Arithmetic},
journal = {CoRR},
volume = {abs/2107.03189},
year = {2021},
url = {https://arxiv.org/abs/2107.03189},
eprinttype = {arXiv},
eprint = {2107.03189},
timestamp = {Tue, 20 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2107-03189.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsc/BrombergerSW20,
author = {Martin Bromberger and
Thomas Sturm and
Christoph Weidenbach},
title = {A complete and terminating approach to linear integer solving},
journal = {J. Symb. Comput.},
volume = {100},
pages = {102--136},
year = {2020},
url = {https://doi.org/10.1016/j.jsc.2019.07.021},
doi = {10.1016/J.JSC.2019.07.021},
timestamp = {Tue, 07 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsc/BrombergerSW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/hal/Bromberger19,
author = {Martin Bromberger},
title = {Decision Procedures for Linear Arithmetic. (Quelques proc{\'{e}}dures
de d{\'{e}}cision pour l'arithm{\'{e}}tique lin{\'{e}}aire)},
school = {Saarland University, Saarbr{\"{u}}cken, Germany},
year = {2019},
url = {https://tel.archives-ouvertes.fr/tel-02427371},
timestamp = {Tue, 21 Jul 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/hal/Bromberger19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrombergerFSW19,
author = {Martin Bromberger and
Mathias Fleury and
Simon Schwarz and
Christoph Weidenbach},
editor = {Pascal Fontaine},
title = {{SPASS-SATT} - {A} {CDCL(LA)} Solver},
booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11716},
pages = {111--122},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-29436-6\_7},
doi = {10.1007/978-3-030-29436-6\_7},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrombergerFSW19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Bromberger18,
author = {Martin Bromberger},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded
Problems},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {329--345},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_22},
doi = {10.1007/978-3-319-94205-6\_22},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/Bromberger18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1804-07703,
author = {Martin Bromberger},
title = {A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded
Problems},
journal = {CoRR},
volume = {abs/1804.07703},
year = {2018},
url = {http://arxiv.org/abs/1804.07703},
eprinttype = {arXiv},
eprint = {1804.07703},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1804-07703.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/BrombergerW17,
author = {Martin Bromberger and
Christoph Weidenbach},
title = {New techniques for linear arithmetic: cubes and equalities},
journal = {Formal Methods Syst. Des.},
volume = {51},
number = {3},
pages = {433--461},
year = {2017},
url = {https://doi.org/10.1007/s10703-017-0278-7},
doi = {10.1007/S10703-017-0278-7},
timestamp = {Fri, 13 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/BrombergerW17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrombergerW16a,
author = {Martin Bromberger and
Christoph Weidenbach},
editor = {Tim King and
Ruzica Piskac},
title = {Computing a Complete Basis for Equalities Implied by a System of {LRA}
Constraints},
booktitle = {Proceedings of the 14th International Workshop on Satisfiability Modulo
Theories affiliated with the International Joint Conference on Automated
Reasoning, SMT@IJCAR 2016, Coimbra, Portugal, July 1-2, 2016},
series = {{CEUR} Workshop Proceedings},
volume = {1617},
pages = {15--30},
publisher = {CEUR-WS.org},
year = {2016},
url = {https://ceur-ws.org/Vol-1617/paper2.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:14 +0100},
biburl = {https://dblp.org/rec/conf/cade/BrombergerW16a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrombergerW16,
author = {Martin Bromberger and
Christoph Weidenbach},
editor = {Nicola Olivetti and
Ashish Tiwari},
title = {Fast Cube Tests for {LIA} Constraint Solving},
booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9706},
pages = {116--132},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40229-1\_9},
doi = {10.1007/978-3-319-40229-1\_9},
timestamp = {Mon, 26 Jun 2023 20:45:22 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrombergerW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Bromberger0W15,
author = {Martin Bromberger and
Thomas Sturm and
Christoph Weidenbach},
editor = {Amy P. Felty and
Aart Middeldorp},
title = {Linear Integer Arithmetic Revisited},
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9195},
pages = {623--637},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21401-6\_42},
doi = {10.1007/978-3-319-21401-6\_42},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Bromberger0W15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BrombergerSW15,
author = {Martin Bromberger and
Thomas Sturm and
Christoph Weidenbach},
title = {Linear Integer Arithmetic Revisited},
journal = {CoRR},
volume = {abs/1503.02948},
year = {2015},
url = {http://arxiv.org/abs/1503.02948},
eprinttype = {arXiv},
eprint = {1503.02948},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BrombergerSW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-04-25 02:09 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
