Publications - Current Year

“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},
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},
}

%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ørner, Nikolaj; Heule, Martin; Voronkov, Andrei
%P 198 - 221
%I EasyChair
%B EasyChair Proceedings in Computing
%N 100
%@ false

“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},
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},
}

%0 Conference Proceedings
%A Bromberger, Martin
%A Krasnopol, Florent
%A Mö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ü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

“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},
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},
}

%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

“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 Luders, Christoph and Radulescu, Ovidiu and Rahkooy, Hamid and Seiss, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1536-0040},
DOI = {10.1137/22M1543963},
PUBLISHER = {SIAM},
ADDRESS = {Philadelphia, PA},
YEAR = {2024},
DATE = {2024},
JOURNAL = {SIAM journal on Applied Dynamical Systems},
VOLUME = {23},
NUMBER = {1},
PAGES = {256--296},
}

%0 Journal Article
%A Desoeuvres, Aurelien
%A Iosif, Alexandru
%A Luders, Christoph
%A Radulescu, Ovidiu
%A Rahkooy, Hamid
%A Seiss, 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

“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},
DATE = {2024},
JOURNAL = {SIAM Journal on Applied Dynamical Systems},
VOLUME = {23},
NUMBER = {1},
PAGES = {813--854},
}

%0 Journal Article
%A Desoeuvres, Aurélien
%A Iosif, Alexandru
%A Lüders, Christoph
%A Radulescu, Ovidiu
%A Rahkooy, Hamid
%A Seiß, 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

“Counting QBF Solutions at Level Two,” Constraints, 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},
JOURNAL = {Constraints},
}

%0 Journal Article
%A Plank, Andreas
%A Mö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
%D 2024
%J Constraints
%I Springer
%C New York, NY
%@ false

“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},
DATE = {2024},
JOURNAL = {AI Communications},
VOLUME = {37},
NUMBER = {4},
PAGES = {485--503},
}

%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 – 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

“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},
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},
}

%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ü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