Publications - Last Year

Conference paper

RG1

M. Bromberger, S. Schwarz, and C. Weidenbach

“Automatic Bit- and Memory-Precise Verification of eBPF Code,” in Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024), Port Louis, Mauritius, 2024.

@inproceedings{BrombergerLPAR24,
TITLE = {Automatic Bit- and Memory-Precise Verification of {eBPF} Code},
AUTHOR = {Bromberger, Martin and Schwarz, Simon and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {2040-557X},
DOI = {10.29007/sj4l},
PUBLISHER = {EasyChair},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
BOOKTITLE = {Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)},
EDITOR = {Bj{\o}rner, Nikolaj and Heule, Martin and Voronkov, Andrei},
PAGES = {198--221},
SERIES = {EasyChair Proceedings in Computing},
VOLUME = {100},
ADDRESS = {Port Louis, Mauritius},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Schwarz, Simon
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Automatic Bit- and Memory-Precise Verification of eBPF Code : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-3E75-6
%R 10.29007/sj4l
%D 2024
%B 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
%Z date of event: 2024-05-23 - 2024-05-29
%C Port Louis, Mauritius
%B Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
%E Bj&#248;rner, Nikolaj; Heule, Martin; Voronkov, Andrei
%P 198 - 221
%I EasyChair
%B EasyChair Proceedings in Computing
%N 100
%@ false

Conference paper

RG1

M. Bromberger, F. Krasnopol, S. Möhle, and C. Weidenbach

“First-Order Automatic Literal Model Generation,” in Automated Reasoning (IJCAR 2024), Nancy, France, 2024.

@inproceedings{Bromberger_IJCAR2024,
TITLE = {First-Order Automatic Literal Model Generation},
AUTHOR = {Bromberger, Martin and Krasnopol, Florent and M{\"o}hle, Sibylle and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-031-63497-0},
DOI = {10.1007/978-3-031-63498-7_9},
PUBLISHER = {Springer},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
BOOKTITLE = {Automated Reasoning (IJCAR 2024)},
EDITOR = {Benzm{\"u}ller, Christoph and Heule, Marijn J. H. and Schmidt, Renate A.},
PAGES = {133--153},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14739},
ADDRESS = {Nancy, France},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Krasnopol, Florent
%A M&#246;hle, Sibylle
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T First-Order Automatic Literal Model Generation : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-3E72-9
%R 10.1007/978-3-031-63498-7_9
%D 2024
%B 12th International Joint Conference on Automated Reasoning
%Z date of event: 2024-07-03 - 2024-07-06
%C Nancy, France
%B Automated Reasoning
%E Benzm&#252;ller, Christoph; Heule, Marijn J. H.; Schmidt, Renate A.
%P 133 - 153
%I Springer
%@ 978-3-031-63497-0
%B Lecture Notes in Artificial Intelligence
%N 14739

Conference paper

RG1

M. Desharnais, B. Toth, U. Waldmann, J. Blanchette, and S. Tourret

“A Modular Formalization of Superposition in Isabelle/HOL,” in 15th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia, 2024.

@inproceedings{Desharnais24,
TITLE = {A Modular Formalization of Superposition in {Isabelle}/{HOL}},
AUTHOR = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie},
LANGUAGE = {eng},
ISBN = {978-3-95977-337-9},
URL = {urn:nbn:de:0030-drops-207401},
DOI = {10.4230/LIPIcs.ITP.2024.12},
PUBLISHER = {Schloss Dagstuhl},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
BOOKTITLE = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
EDITOR = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
PAGES = {1--20},
EID = {12},
SERIES = {Leibniz International Proceedings in Informatics},
VOLUME = {309},
ADDRESS = {Tbilisi, Georgia},
}

Endnote

%0 Conference Proceedings
%A Desharnais, Martin
%A Toth, Balazs
%A Waldmann, Uwe
%A Blanchette, Jasmin
%A Tourret, Sophie
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Modular Formalization of Superposition in Isabelle/HOL : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-3E7C-F
%R 10.4230/LIPIcs.ITP.2024.12
%U  urn:nbn:de:0030-drops-207401
%D 2024
%B 15th International Conference on Interactive Theorem Proving
%Z date of event: 2024-09-09 - 2024-09-14
%C Tbilisi, Georgia
%B 15th International Conference on Interactive Theorem Proving
%E Bertot, Yves; Kutsia, Temur; Norrish, Michael
%P 1 - 20
%Z sequence number: 12
%I Schloss Dagstuhl
%@  978-3-95977-337-9
%B Leibniz International Proceedings in Informatics
%N 309

Article

RG1

A. Desoeuvres, A. Iosif, C. Lüders, O. Radulescu, H. Rahkooy, M. Seiß, and T. Sturm

“Reduction of Chemical Reaction Networks with Approximate Conservation Laws,” SIAM Journal on Applied Dynamical Systems, vol. 23, no. 1, 2024.

@article{Desoeuvre24b,
TITLE = {Reduction of Chemical Reaction Networks with Approximate Conservation Laws},
AUTHOR = {Desoeuvres, Aurelien and Iosif, Alexandru and L{\"u}ders, Christoph and Radulescu, Ovidiu and Rahkooy, Hamid and Sei{\ss}, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1536-0040},
DOI = {10.1137/22M1543963},
PUBLISHER = {SIAM},
ADDRESS = {Philadelphia, PA},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
JOURNAL = {SIAM Journal on Applied Dynamical Systems},
VOLUME = {23},
NUMBER = {1},
PAGES = {256--296},
}

Endnote

%0 Journal Article
%A Desoeuvres, Aurelien
%A Iosif, Alexandru
%A L&#252;ders, Christoph
%A Radulescu, Ovidiu
%A Rahkooy, Hamid
%A Sei&#223;, Matthias
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Reduction of Chemical Reaction Networks with Approximate Conservation Laws : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000F-13AF-7
%R 10.1137/22M1543963
%D 2024
%J SIAM Journal on Applied Dynamical Systems
%V 23
%N 1
%& 256
%P 256 - 296
%I SIAM
%C Philadelphia, PA
%@ false

Article

RG1

A. Desoeuvres, A. Iosif, C. Lüders, O. Radulescu, H. Rahkooy, M. Seiß, and T. Sturm

“A Computational Approach to Polynomial Conservation Laws,” SIAM Journal on Applied Dynamical Systems, vol. 23, no. 1, 2024.

@article{Desoeuvres24,
TITLE = {A Computational Approach to Polynomial Conservation Laws},
AUTHOR = {Desoeuvres, Aur{\'e}lien and Iosif, Alexandru and L{\"u}ders, Christoph and Radulescu, Ovidiu and Rahkooy, Hamid and Sei{\ss}, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1536-0040},
DOI = {10.1137/22M1544014},
PUBLISHER = {SIAM},
ADDRESS = {Philadelphia, PA},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
JOURNAL = {SIAM Journal on Applied Dynamical Systems},
VOLUME = {23},
NUMBER = {1},
PAGES = {813--854},
}

Endnote

%0 Journal Article
%A Desoeuvres, Aur&#233;lien
%A Iosif, Alexandru
%A L&#252;ders, Christoph
%A Radulescu, Ovidiu
%A Rahkooy, Hamid
%A Sei&#223;, Matthias
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Computational Approach to Polynomial Conservation Laws : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000F-7429-1
%R 10.1137/22M1544014
%7 2024
%D 2024
%J SIAM Journal on Applied Dynamical Systems
%V 23
%N 1
%& 813
%P 813 - 854
%I SIAM
%C Philadelphia, PA
%@ false

Conference paper

RG1

L. Gerlach, S. Schwarz, N. Faroß, and M. Schwarz

“Efficient and Generic Microarchitectural Hash-Function Recovery,” in 45th IEEE Symposium on Security and Privacy (SP 2024), San Francisco, CA, USA, 2024.

@inproceedings{GerlachSP24,
TITLE = {Efficient and Generic Microarchitectural Hash-Function Recovery},
AUTHOR = {Gerlach, Lukas and Schwarz, Simon and Faro{\ss}, Nicolas and Schwarz, Michael},
LANGUAGE = {eng},
ISBN = {979-8-3503-3130-1},
DOI = {10.1109/SP54263.2024.00028},
PUBLISHER = {IEEE},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
BOOKTITLE = {45th IEEE Symposium on Security and Privacy (SP 2024)},
PAGES = {3661--3678},
ADDRESS = {San Francisco, CA, USA},
}

Endnote

%0 Conference Proceedings
%A Gerlach, Lukas
%A Schwarz, Simon
%A Faro&#223;, Nicolas
%A Schwarz, Michael
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Efficient and Generic Microarchitectural Hash-Function Recovery : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-886F-9
%R 10.1109/SP54263.2024.00028
%D 2024
%B 45th IEEE Symposium on Security and Privacy
%Z date of event: 2024-05-20 - 2024-05-24
%C San Francisco, CA, USA
%B 45th IEEE Symposium on Security and Privacy
%P 3661 - 3678
%I IEEE
%@ 979-8-3503-3130-1

Paper

RG1

H. Leidinger and C. Weidenbach

“Non-Ground Congruence Closure,” 2024. [Online]. Available: https://arxiv.org/abs/2412.10066.

Abstract

Congruence closure on ground equations is a well-established, efficient
algorithm for deciding ground equalities. It computes an explicit
representation of the ground equivalence classes on the basis of a set of
ground input equations. Then equalities are decided by membership. We
generalize the ground congruence closure algorithm to non-ground equations. The
algorithm also computes an explicit representation of all non-ground
equivalence classes. It is terminating due to an a priori bound on the term
size. By experiments we compare our new algorithm with ground congruence
closure.

BibTeX

@online{Leidinger2412.10066,
TITLE = {Non-Ground Congruence Closure},
AUTHOR = {Leidinger, Hendrik and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2412.10066},
EPRINT = {2412.10066},
EPRINTTYPE = {arXiv},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
ABSTRACT = {Congruence closure on ground equations is a well-established, efficient<br>algorithm for deciding ground equalities. It computes an explicit<br>representation of the ground equivalence classes on the basis of a set of<br>ground input equations. Then equalities are decided by membership. We<br>generalize the ground congruence closure algorithm to non-ground equations. The<br>algorithm also computes an explicit representation of all non-ground<br>equivalence classes. It is terminating due to an a priori bound on the term<br>size. By experiments we compare our new algorithm with ground congruence<br>closure.<br>},
}

Endnote

%0 Report
%A Leidinger, Hendrik
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Non-Ground Congruence Closure : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-8A35-7
%U https://arxiv.org/abs/2412.10066
%D 2024
%X   Congruence closure on ground equations is a well-established, efficient<br>algorithm for deciding ground equalities. It computes an explicit<br>representation of the ground equivalence classes on the basis of a set of<br>ground input equations. Then equalities are decided by membership. We<br>generalize the ground congruence closure algorithm to non-ground equations. The<br>algorithm also computes an explicit representation of all non-ground<br>equivalence classes. It is terminating due to an a priori bound on the term<br>size. By experiments we compare our new algorithm with ground congruence<br>closure.<br>
%K Computer Science, Logic in Computer Science, cs.LO

Article

RG1

A. Plank, S. Möhle, and M. Seidl

“Counting QBF Solutions at Level Two,” Constraints, vol. 29, 2024.

@article{Moehle24,
TITLE = {Counting {QBF} Solutions at Level Two},
AUTHOR = {Plank, Andreas and M{\"o}hle, Sibylle and Seidl, Martina},
LANGUAGE = {eng},
ISSN = {1383-7133},
DOI = {10.1007/s10601-024-09369-4},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
JOURNAL = {Constraints},
VOLUME = {29},
PAGES = {22--39},
}

Endnote

%0 Journal Article
%A Plank, Andreas
%A M&#246;hle, Sibylle
%A Seidl, Martina
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Counting QBF Solutions at Level Two : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000F-BC36-1
%R 10.1007/s10601-024-09369-4
%7 2024-08-08
%D 2024
%J Constraints
%V 29
%& 22
%P 22 - 39
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/d62iE

Article

RG1

G. Sutcliffe and M. Desharnais

“The CADE-29 Automated Theorem Proving System Competition – CASC-29,” AI Communications, vol. 37, no. 4, 2024.

@article{Sutcliffe24,
TITLE = {The {CADE}-29 Automated Theorem Proving System Competition -- {CASC}-29},
AUTHOR = {Sutcliffe, Geoff and Desharnais, Martin},
LANGUAGE = {eng},
ISSN = {0921-7126},
DOI = {10.3233/AIC-230325},
PUBLISHER = {IOS},
ADDRESS = {Amsterdam, Netherlands},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
JOURNAL = {AI Communications},
VOLUME = {37},
NUMBER = {4},
PAGES = {485--503},
}

Endnote

%0 Journal Article
%A Sutcliffe, Geoff
%A Desharnais, Martin
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T The CADE-29 Automated Theorem Proving System Competition &#8211; CASC-29  : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-2CFB-3
%R 10.3233/AIC-230325
%7 2024-09-18
%D 2024
%J AI Communications
%V 37
%N 4
%& 485
%P 485 - 503
%I IOS
%C Amsterdam, Netherlands
%@ false

Conference paper

RG1

U. Waldmann

“On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus,” in Automated Reasoning (IJCAR 2024), Nancy, France, 2024.

@inproceedings{Waldmann_IJCAR2024,
TITLE = {On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus},
AUTHOR = {Waldmann, Uwe},
LANGUAGE = {eng},
ISBN = {978-3-031-63497-0},
DOI = {10.1007/978-3-031-63498-7_15},
PUBLISHER = {Springer},
YEAR = {2024},
MARGINALMARK = {$\bullet$},
DATE = {2024},
BOOKTITLE = {Automated Reasoning (IJCAR 2024)},
EDITOR = {Benzm{\"u}ller, Christoph and Heule, Marijn J. H. and Schmidt, Renate A.},
PAGES = {244--261},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14739},
ADDRESS = {Nancy, France},
}

Endnote

%0 Conference Proceedings
%A Waldmann, Uwe
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-2E45-E
%R 10.1007/978-3-031-63498-7_15
%D 2024
%B 12th International Joint Conference on Automated Reasoning
%Z date of event: 2024-07-03 - 2024-07-06
%C Nancy, France
%B Automated Reasoning
%E Benzm&#252;ller, Christoph; Heule, Marijn J. H.; Schmidt, Renate A.
%P 244 - 261
%I Springer
%@ 978-3-031-63497-0
%B Lecture Notes in Artificial Intelligence
%N 14739
%U https://rdcu.be/d0hDL