3 Search Results for "Sälzer, Marco"

Document
DOI: 10.4230/LIPIcs.ITP.2025.1
A Certified Proof Checker for Deep Neural Network Verification in Imandra

Authors: Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra - an industrial functional programming language and an interactive theorem prover (ITP) - that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.
Cite as

Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desmartin_et_al:LIPIcs.ITP.2025.1,
  author =	{Desmartin, Remi and Isac, Omri and Passmore, Grant and Komendantskaya, Ekaterina and Stark, Kathrin and Katz, Guy},
  title =	{{A Certified Proof Checker for Deep Neural Network Verification in Imandra}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.1},
  URN =		{urn:nbn:de:0030-drops-246000},
  doi =		{10.4230/LIPIcs.ITP.2025.1},
  annote =	{Keywords: Neural Network Verification, Farkas Lemma, Proof Certification}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.TIME.2023.19
Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract)

Authors: Marco Sälzer and Silvia Beddar-Wiesing

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
We present a first notion of a time-aware robustness property for Temporal Graph Neural Networks (TGNN), a recently popular framework for computing functions over continuous- or discrete-time graphs, motivated by recent work on time-aware attacks on TGNN used for link prediction tasks. Furthermore, we discuss promising verification approaches for the presented or similar safety properties and possible next steps in this direction of research.
Cite as

Marco Sälzer and Silvia Beddar-Wiesing. Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 19:1-19:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{salzer_et_al:LIPIcs.TIME.2023.19,
  author =	{S\"{a}lzer, Marco and Beddar-Wiesing, Silvia},
  title =	{{Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{19:1--19:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.19},
  URN =		{urn:nbn:de:0030-drops-191094},
  doi =		{10.4230/LIPIcs.TIME.2023.19},
  annote =	{Keywords: graph neural networks, temporal, verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.24
Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures

Authors: Florian Bruse, Marco Sälzer, and Martin Lange

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The modal μ-calculus can only express bisimulation-invariant properties. It is a simple consequence of Kleene’s Fixpoint Theorem that on structures with finite bisimulation quotients, the fixpoint iteration of any formula converges after finitely many steps. We show that the converse does not hold: we construct a word with an infinite bisimulation quotient that is locally regular so that the iteration for any fixpoint formula of the modal μ-calculus on it converges after finitely many steps. This entails decidability of μ-calculus model-checking over this word. We also show that the reason for the discrepancy between infinite bisimulation quotients and trans-finite fixpoint convergence lies in the fact that the μ-calculus can only express regular properties.
Cite as

Florian Bruse, Marco Sälzer, and Martin Lange. Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.MFCS.2021.24,
  author =	{Bruse, Florian and S\"{a}lzer, Marco and Lange, Martin},
  title =	{{Finite Convergence of \mu-Calculus Fixpoints on Genuinely Infinite Structures}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.24},
  URN =		{urn:nbn:de:0030-drops-144643},
  doi =		{10.4230/LIPIcs.MFCS.2021.24},
  annote =	{Keywords: temporal logic, fixpoint iteration, bisimulation}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023
  • 1 2021

  • Refine by Author
  • 2 Sälzer, Marco
  • 1 Beddar-Wiesing, Silvia
  • 1 Bruse, Florian
  • 1 Desmartin, Remi
  • 1 Isac, Omri
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Computing methodologies → Neural networks
  • 2 Theory of computation → Logic and verification
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Formal software verification
  • 1 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 1 Farkas Lemma
  • 1 Neural Network Verification
  • 1 Proof Certification
  • 1 bisimulation
  • 1 fixpoint iteration
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact