\newif\ifresearchfull
\newif\iftalksinvitedonly
\newif\ifshowstudentsupervision
\newif\ifshowprivatefields

\researchfulltrue
\talksinvitedonlytrue
\showstudentsupervisiontrue
\showprivatefieldstrue\documentclass[a4paper,11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[a4paper,left=1.8cm,right=1.8cm,top=1.5cm,bottom=1.6cm]{geometry}
\usepackage{enumitem}
\usepackage[hidelinks]{hyperref}
\usepackage[dvipsnames]{xcolor}
\usepackage[p,osf,swashQ]{cochineal}
\usepackage[medium,bold]{cabin}
\usepackage[varqu,varl,scale=0.9]{zi4}
\usepackage[backend=biber, maxbibnames=99]{biblatex}

\DeclareSortingTemplate{ydmnt}{
  \sort{\field{presort}}
  \sort{\field{sortkey}}
  \sort[direction=descending]{\field{year}}
  \sort[direction=descending]{\field{month}}
  \sort{
    \field{sortname}
    \field{author}
    \field{editor}
    \field{translator}
  }
  \sort{\field{sorttitle}}
  \sort{\field{title}}
}
\ExecuteBibliographyOptions{sorting=ydmnt}

\usepackage{xpatch}% or use http://tex.stackexchange.com/a/40705

\DeclareFieldFormat{eventtitleaddon}{\textbf{#1}}
\DeclareFieldFormat[article]{number}{\textbf{#1}}
\DeclareFieldFormat[article]{journal}{\textbf{#1}}
\DeclareFieldFormat[article]{journaltitle}{\textbf{#1}}
\DeclareFieldFormat{labelnumberwidth}{#1.}

\makeatletter
\newbibmacro*{name:bold}[2]{%
  \edef\blx@tmp@name{\expandonce#1, \expandonce#2}%
  \def\do##1{\ifdefstring{\blx@tmp@name}{##1}{\bfseries\listbreak}{}}%
  \dolistloop{\boldnames}}
\newcommand*{\boldnames}{}
\makeatother

\xpretobibmacro{name:family}{\begingroup\usebibmacro{name:bold}{#1}{#2}}{}{}
\xpretobibmacro{name:given-family}{\begingroup\usebibmacro{name:bold}{#1}{#2}}{}{}
\xpretobibmacro{name:family-given}{\begingroup\usebibmacro{name:bold}{#1}{#2}}{}{}
\xpretobibmacro{name:delim}{\begingroup\normalfont}{}{}

\xapptobibmacro{name:family}{\endgroup}{}{}
\xapptobibmacro{name:given-family}{\endgroup}{}{}
\xapptobibmacro{name:family-given}{\endgroup}{}{}
\xapptobibmacro{name:delim}{\endgroup}{}{}

% List your own name variants that are to be highlighted
\forcsvlist{\listadd\boldnames}
{ {Teuber, Samuel}, {Samuel Teuber} }

\definecolor{CVHeading}{HTML}{145A5A}
\definecolor{CVRule}{HTML}{5B8C85}

\begin{filecontents*}[overwrite]{cv-journals.bib}

@article{daggitt2026compositionalneuralcyberphysicalverificationinteractive,
      title={Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice}, 
      author={Matthew L. Daggitt and Ekaterina Komendantskaya and Alistair Sirman and Alessandro Bruni and Samuel Teuber and Josh Smart and Grant Passmore},
      eprint={2605.02790},
      archivePrefix={arXiv},
      primaryClass={cs.PL},
      url={https://arxiv.org/abs/2605.02790}, 
      journal      = {Proc. {ACM} Program. Lang.},
      number       = {ICFP},
      year={2026},
  month = {aug},
}

@article{teuber2025heterogeneousdynamiclogicprovability,
  author    = {Teuber, Samuel and
               Ulbrich, Mattias and
               Platzer, Andr{\'{e}} and
               Beckert, Bernhard},
  title     = {Heterogeneous Dynamic Logic: Provability Modulo Program Theories},
  journal      = {Proc. {ACM} Program. Lang.},
  number       = {PLDI},
  year         = {2026},
  month = {jun},
  doi       = {10.1145/3808295},
  editor    = {Manu Sridharan},
  eprinttype    = {arXiv},
  eprint       = {2507.08581}
}

\end{filecontents*}

\begin{filecontents*}[overwrite]{cv-conferences.bib}

@INPROCEEDINGS{TeuberAngelsAndDemons2025,
  author       = {Samuel Teuber and
                  Debasmita Lohar and
                  Bernhard Beckert},
  title        = {Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite
                  Precision},
  booktitle       = {25th Conference on Formal Methods in Computer-Aided
                  Design},
  eventtitleaddon = {{FMCAD}~2025},
  venue           = {Menlo Park, CA, USA},
  eventdate       = {2025-10-06/2025-10-10},
  year         = {2025},
  month = {sep},
  opturl       = {https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_12},
  doi          = {10.34727/2025/isbn.978-3-85448-084-6_12},
}


@INPROCEEDINGS{PrebetHighwayCarControl2025,
  author       = {Enguerrand Prebet and
                  Samuel Teuber and
                  Andr{\'{e}} Platzer},
  editor       = {Michael Leuschel and
                  Fuyuki Ishikawa},
  title        = {Verification of Autonomous Neural Car Control with KeYmaera {X}},
  booktitle       = {11th International Conference on Rigorous State-Based Methods},
  eventtitleaddon = {{ABZ}~2025},
  venue           = {D{\"{u}}sseldorf, Germany},
  eventdate       = {2025-06-10/2025-06-13},
  series       = {LNCS},
  volume       = {15728},
  pages        = {288--307},
  publisher    = {Springer},
  year         = {2025},
  month = {jun},
  opturl       = {https://doi.org/10.1007/978-3-031-94533-5_17},
  doi          = {10.1007/978-3-031-94533-5_17},
}


@INPROCEEDINGS{VeryDiff,
  author       = {Samuel Teuber and
                  Philipp Kern and
                  Marvin Janzen and
                  Bernhard Beckert},
  editor       = {Arie Gurfinkel and
                  Marijn Heule},
  title        = {Revisiting Differential Verification: Equivalence Verification with
                  Confidence},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  eventtitleaddon    = {{TACAS}~2025},
  venue           = {Hamilton, ON, Canada},
  eventdate       = {2025-05-03/2025-05-08},
  series       = {LNCS},
  volume       = {15697},
  pages        = {257--278},
  publisher    = {Springer},
  year         = {2025},
  month = {may},
  doi          = {10.1007/978-3-031-90653-4_13},
}





@inproceedings{TeuberVerSAILLE2024,
  author       = {Samuel Teuber and
                  Stefan Mitsch and
                  Andr{\'{e}} Platzer},
  editor       = {Amir Globersons and
                  Lester Mackey and
                  Danielle Belgrave and
                  Angela Fan and
                  Ulrich Paquet and
                  Jakub M. Tomczak and
                  Cheng Zhang},
  title        = {Provably Safe Neural Network Controllers via Differential Dynamic
                  Logic},
  booktitle    = {Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems},
  eventtitleaddon = {{NeurIPS}~2024},
  venue           = {Vancouver, BC, Canada},
  eventdate       = {2024-12-10/2024-12-15},
  year         = {2024},
  month = {dec},
  opturl       = {http://papers.nips.cc/paper_files/paper/2024/hash/031b5fd7d847f69ed33378a9a1117b4b-Abstract-Conference.html},
  timestamp    = {Thu, 13 Feb 2025 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/nips/TeuberMP24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}



@inproceedings{Beckert24,
  title           = {Towards Combining the Cognitive Abilities of Large
                     Language Models with the Rigor of Deductive Progam
                     Verification},
  author          = {Bernhard Beckert and
                     Jonas Klamroth and
                     Wolfram Pfeifer and
                     Patrick R{\"{o}}per and
                     Samuel Teuber},
  year            = {2024},
  month = {oct},
  booktitle       = {12th International Symposium on Leveraging Applications
                     of Formal Methods, Verification and Validation.
                     Software Engineering Methodologies, Part {IV}},
  eventtitleaddon = {{ISoLA}~2024},
  venue           = {Crete, Greece},
  eventdate       = {2024-10-27/2024-10-31},
  editor          = {Tiziana Margaria and
                     Bernhard Steffen},
  series          = {LNCS},
  volume          = {15222},
  pages           = {242--257},
  publisher       = {Springer},
  doi             = {10.1007/978-3-031-75387-9_15}
}


@inproceedings{TeuberAAAI24,
  author       = {Samuel Teuber and
                  Bernhard Beckert},
  editor       = {Michael J. Wooldridge and
                  Jennifer G. Dy and
                  Sriraam Natarajan},
  title        = {An Information-Flow Perspective on Algorithmic Fairness},
  booktitle       = {Thirty-Eighth {AAAI} Conference on Artificial Intelligence},
  eventtitleaddon = {{AAAI}~2024},
  venue           = {Vancouver, BC, Canada},
  eventdate       = {2024-02-20/2024-02-27},
  pages        = {15337--15345},
  publisher    = {{AAAI} Press},
  year         = {2024},
  month = {feb},
   opturl       = {https://doi.org/10.1609/aaai.v38i14.29458},
  doi          = {10.1609/AAAI.V38I14.29458},
  timestamp    = {Mon, 03 Mar 2025 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/aaai/TeuberB24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}



@inproceedings{LanzingerSAC24,
  author       = {Florian Lanzinger and
                  Christian Martin and
                  Frederik Reiche and
                  Samuel Teuber and
                  Robert Heinrich and
                  Alexander Weigl},
  editor       = {Jiman Hong and
                  Juw Won Park},
  title        = {Quantifying Software Correctness by Combining Architecture Modeling
                  and Formal Program Analysis},
  booktitle    = {39th {ACM/SIGAPP} Symposium on Applied Computing},
  eventtitleaddon = {{SAC}~2024},
  venue           = {Avila, Spain},
  eventdate       = {2024-04-08/2024-04-12},
  pages        = {1702--1711},
  publisher    = {{ACM}},
  year         = {2024},
   opturl       = {https://doi.org/10.1145/3605098.3636008},
  doi          = {10.1145/3605098.3636008},
  timestamp    = {Sun, 19 Jan 2025 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/sac/LanzingerMRTHW24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org},
  month = {apr}
}

@INPROCEEDINGS{TeuberICTAI21,
  author={Teuber, Samuel and Kleine Büning, Marko and Kern, Philipp and Sinz, Carsten},
  booktitle={IEEE 33rd International Conference on Tools with Artificial Intelligence},
  eventtitleaddon = {{ICTAI}~2021},
  venue           = {virtual},
  eventdate       = {2021-11-01/2021-11-03},
  title={Geometric Path Enumeration for Equivalence Verification of Neural Networks}, 
  year={2021},
  month = {nov},
  volume={},
  number={},
  pages={200-208},
  doi={10.1109/ICTAI52525.2021.00035}
}


@InProceedings{TeuberQEST21,
  author={Teuber, Samuel and Weigl, Alexander},
  editor={Abate, Alessandro and Marin, Andrea},
  title={Quantifying Software Reliability via Model-Counting},
  booktitle={Quantitative Evaluation of Systems},
  eventtitleaddon = {{QEST}~2021},
  venue           = {virtual},
  eventdate       = {2021-08-23/2021-08-27},
  year={2021},
  publisher={Springer},
  address={Cham},
  pages={59--79},
  isbn={978-3-030-85172-9},
  month = {aug}
}


\end{filecontents*}

\begin{filecontents*}[overwrite]{cv-workshops.bib}

@INPROCEEDINGS{TeuberNSE2025,
  title           = {Next Steps in LLM-Supported Java Verification},
  author          = {Samuel Teuber and
                     Bernhard Beckert},
  year            = {2025},
  booktitle       = {1st {IEEE/ACM} International Workshop on Neuro-Symbolic
                     Software Engineering},
  eventtitleaddon = {{NSE@ICSE}~2025},
  venue           = {Ottawa, ON, Canada},
  eventdate       = {2025-05-03},
  pages           = {1--4},
  publisher       = {{IEEE}},
  doi             = {10.1109/NSE66660.2025.00007},
  month = {may}
}


@inproceedings{TeuberEWAF23,
  author       = {Samuel Teuber and
                  Bernhard Beckert},
  editor       = {Jos{\'{e}} M. {\'{A}}lvarez and
                  Alessandro Fabris and
                  Christoph Heitz and
                  Corinna Hertweck and
                  Michele Loi and
                  Meike Zehlike},
  title        = {Formally Verified Algorithmic Fairness Using Information-Flow Tools},
  booktitle    = {2nd European Workshop on Algorithmic Fairness},
  eventtitleaddon = {{EWAF}~2023},
  venue        = {Winterthur, Switzerland},
  eventdate    = {2023-06-07/2023-06-09},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {3442},
  publisher    = {CEUR-WS.org},
  year         = {2023},
  month = {jun},
   opturl       = {https://ceur-ws.org/Vol-3442/paper-21.pdf},
  timestamp    = {Fri, 03 May 2024 17:18:29 +0200},
  biburl       = {https://dblp.org/rec/conf/ewaf/TeuberB23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}



\end{filecontents*}

\begin{filecontents*}[overwrite]{cv-preprints.bib}



@article{DBLP:journals/corr/abs-2606-21282,
  author       = {Anagha Athavale and
                  Samuel Teuber and
                  Matteo Maffei and
                  Ezio Bartocci and
                  Dejan Nickovic and
                  Georg Weissenbacher},
  title        = {Differential Zonotopes for Verifying Global Robustness of DNNs},
  journal      = {CoRR},
  volume       = {abs/2606.21282},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2606.21282},
  doi          = {10.48550/ARXIV.2606.21282},
  eprinttype   = {arXiv},
  eprint       = {2606.21282},
  timestamp    = {Wed, 08 Jul 2026 21:21:07 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2606-21282.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}





@article{DBLP:journals/corr/abs-2605-23096,
  author       = {Philipp Kern and
                  Lorenzo Rovida and
                  Samuel Teuber and
                  Edoardo Manino and
                  Carsten Sinz and
                  Alberto Leporati},
  title        = {Encrypted Neural Networks without Overflows},
  journal      = {CoRR},
  volume       = {abs/2605.23096},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2605.23096},
  doi          = {10.48550/ARXIV.2605.23096},
  eprinttype   = {arXiv},
  eprint       = {2605.23096},
  timestamp    = {Fri, 12 Jun 2026 15:09:30 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2605-23096.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

\end{filecontents*}

\begin{filecontents*}[overwrite]{cv-software.bib}

@software{samuel_teuber_2025_14627125,
  author       = {Samuel Teuber and
                  Kern, Philipp and
                  Janzen, Marvin and
                  Beckert, Bernhard},
  title        = {VeryDiff},
  month = {jan},
  year         = 2025,
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.14627125},
  url          = {https://doi.org/10.5281/zenodo.14627125}
}

@software{samuel_teuber_2024_13922169,
  author       = {Samuel Teuber and
                  Mitsch, Stefan and
                  Platzer, André},
  title        = {NCubeV},
  month = {oct},
  year         = 2024,
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.13922169},
  url          = {https://doi.org/10.5281/zenodo.13922169},
}


@software{teuber_2024_13922177,
  author       = {Teuber, Samuel and
                  Kern, Philipp},
  title        = {samysweb/nnequiv: v1.1},
  month = {oct},
  year         = 2024,
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.13922177},
  url          = {https://doi.org/10.5281/zenodo.13922177}
}

@software{TeuberWeigl2021_1000134169,
    author       = {Teuber, Samuel and Weigl, Alexander},
    year         = {2021},
    title        = {counterSharp},
    doi          = {10.5445/IR/1000134169}
}

\end{filecontents*}

\begin{filecontents*}[overwrite]{cv-theses.bib}

@mastersthesis{TeuberMA,
    title={Transfer of Safety Guarantees from Differential Dynamic Logic Proofs to Neural Network-based Controller Systems},
    author={Teuber, Samuel},
    year={2022},
    school={Karlsruhe Institute of Technology},
    type={Master's Thesis},
    note={Awarded with the "Best Master's Thesis Award" of the Faculty of Informatics, KIT, 2022}
}

@mastersthesis{TeuberBA,
    title={Solving difficult SMT instances using abstractions and incremental SMT solving},
    author={Teuber, Samuel},
    year={2020},
    school={Karlsruhe Institute of Technology},
    type={Bachelor's Thesis}
}

\end{filecontents*}

\newcommand{\CVSection}[1]{\vspace{0.85em}\noindent{\large\bfseries\sffamily\color{CVHeading}\textsc{#1}}\par\vspace{0.15em}{\color{CVRule}\hrule}\vspace{0.35em}}
\newcommand{\CVSubsection}[1]{\vspace{0.35em}\noindent{\bfseries\sffamily #1}\par\vspace{0.2em}}
\setlist[itemize]{leftmargin=1.2em,itemsep=0.22em,topsep=0.2em,parsep=0pt,label={\color{CVRule}$\diamond$}}
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.15em}

\begin{document}
{\LARGE\bfseries\sffamily Samuel Teuber}\\[-0.1em]
%
\href{mailto:teuber@kit.edu}%
teuber@kit.edu%
%
%
\hspace{0.8em}{\color{CVRule}$\diamond$}\hspace{0.8em}%
\url{ www.teuber.dev }%
%
\ifshowprivatefields%
%
\fi

\vspace{0.2em}
\noindent
\begin{minipage}[t]{0.49\textwidth}\vspace*{0pt}

  \textbf{Office Address}\\[-0.1em]
Am Fasanengarten 5, 76131 Karlsruhe, Germany
\par\vspace{0.3em}

\ifshowprivatefields

\fi
\end{minipage}%
\hfill%
\begin{minipage}[t]{0.49\textwidth}\vspace*{0pt}
\begin{tabular}{@{}p{0.38\linewidth}p{0.58\linewidth}@{}}



  \textbf{Languages:} & German (native), English (fluent), French (basic)\\

\end{tabular}
\end{minipage}

\CVSection{Research Interests}
\ifresearchfull
My research develops logical foundations and practical tools for the verification of AI-based heterogeneous systems, that is, systems combining software, AI, and physical components. Concrete applications include the formal verification of neural network control systems and the verification of algorithmic fairness.
\else
\begin{itemize}[leftmargin=*]
\item Formal verification of neural network control systems
\item Algorithmic fairness and information-flow perspectives
\item Deductive verification with theorem provers
\end{itemize}
\fi

\CVSection{Education}
\begin{itemize}[leftmargin=*]
\item \textbf{ 2022-present }: \textbf{ PhD Candidate in Computer Science } --- Karlsruhe Institute of Technology\\
\emph{Thesis:} Provable Correctness of AI-based Heterogeneous Systems ---
Completion planned by Feb. 2027
\item \textbf{ 2022 }: \textbf{ Master's Thesis via interACT } --- Logical Systems Lab, Carnegie Mellon University\\
\emph{Thesis:} Transfer of Safety Guarantees from Differential Dynamic Logic Proofs to Neural Network-based Controller Systems ---
Awarded with KIT Informatic's Best Thesis Award\\
\emph{Referees:} Prof. André Platzer (CMU); Prof. Carsten Sinz (KIT)
\item \textbf{ 2020-2022 }: \textbf{ M.Sc. in Computer Science } --- Karlsruhe Institute of Technology\\
\emph{Subject:} Computer Science\\
\emph{Grade:} 1.0 (very good; with distinction)
\item \textbf{ 2017-2018 }: \textbf{ ERASMUS Exchange } --- ENSIMAG, Grenoble\\
\emph{Subject:} Ingénierie des Systèmes d’Information
\item \textbf{ 2015-2020 }: \textbf{ B.Sc. in Computer Science } --- Karlsruhe Institute of Technology\\
\emph{Subject:} Computer Science\\
\emph{Grade:} 1.5 (very good)\\
\emph{Thesis:} Solving difficult SMT instances using abstractions and incremental SMT solving\\
\emph{Referees:} Prof. Carsten Sinz (KIT)
\item \textbf{ 2015 }: \textbf{ A Levels (Abitur) } --- Oskar-von-Miller-Gymnasium, München\\
\emph{Grade:} 1.2 (very good)
\end{itemize}

\CVSection{Experience}
\begin{itemize}[leftmargin=*]\item \textbf{ 2022-present }: Researcher, KASTEL Beckert, KIT\item \textbf{ 2020-2021 }: Student Assistant for Software Safety Quantification Research, ITI Beckert, KIT\item \textbf{ 2019-2021 }: Student Teaching Assistant for "Programmierparadigmen", IPD Snelting, KIT\item \textbf{ 2018 }: CERN Openlab Summer Student, EP-SFT, CERN\item \textbf{ 2015-2016 }: Student Assistant, IT-Centre for the humanities, LMU
\end{itemize}

\CVSection{Awards and Honors}
\begin{itemize}[leftmargin=*]\item \textbf{ 2023 }: Best Master's Thesis Award 2022/2023 by the KIT Informatics Department\item \textbf{ 2018 }: One of the competition winners during the CERN Openlab lightning talks 2018\item \textbf{ 2016 }: Abitur prize of the German Physics Association (DPG)
\end{itemize}

\CVSection{Funding \& Scholarships}
\begin{itemize}[leftmargin=*]\item \textbf{ 2017-2022 }: Scholarship holder at Cusanuswerk e.V.
\end{itemize}

\CVSection{Publications}
\CVSubsection{Refereed Journal Publications}
\begin{refsection}[cv-journals.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSubsection{Refereed Conference Publications}
\begin{refsection}[cv-conferences.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSubsection{Refereed Workshop Publications}
\begin{refsection}[cv-workshops.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSubsection{Preprints}
\begin{refsection}[cv-preprints.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSubsection{Software}
\begin{refsection}[cv-software.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSubsection{Theses}
\begin{refsection}[cv-theses.bib]
\nocite{*}
\printbibliography[heading=none]
\end{refsection}

\CVSection{ Talks }
\CVSubsection{Invited Talks}
\begin{itemize}[leftmargin=*]
\item \textbf{ 2026}:\textbf{ Guaranteed Safe AI Seminars } --- Horizon Omega (online)
\item \textbf{ 2025}:\textbf{ Of Good Demons and Bad Angels: Guaranteeing Safe Neural Control under Finite Precision } --- ANSR Reading Group, Berkeley, California, US (Online)
\item \textbf{ 2025}:\textbf{ Of Good Demons and Bad Angels: Guaranteeing Safe Neural Control under Finite Precision } --- Arcak Group (Berkeley, California, US)
\item \textbf{ 2025}:\textbf{ Provable Guarantees for Neural Networks } --- Meel Group (Online)
\item \textbf{ 2024}:\textbf{ Provably Safe Neural Network Controllers via Differential Dynamic Logic } --- Laboratory for Foundations of Computer Science Seminar (Edinburgh, UK)
\end{itemize}

\CVSubsection{Contributed Talks}
\begin{itemize}[leftmargin=*]
\item \textbf{ 2026}:\textbf{ Heterogeneous Dynamic Logic: Provability Modulo Program Theories } --- Formal Reasoning for Compositional Systems Engineering (FLoC, Lisbon, Portugal)
\item \textbf{ 2026}:\textbf{ Differential Verification of Neural Networks: Theory and Applications } --- Workshop on Program Equivalence and Relational Reasoning (FLoC, Lisbon, Portugal)
\item \textbf{ 2026}:\textbf{ Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision } --- Symposium on AI Verification (FLoC, Lisbon, Portugal)
\item \textbf{ 2025}:\textbf{ Replication of the Landscape for LLM-generated Formal Specifications for C Programs } --- Contract Languages Seminar (Online)
\item \textbf{ 2025}:\textbf{ Dynamic Logic à la Locale } --- KeY Symposium (Manigod, France)
\item \textbf{ 2025}:\textbf{ Towards LLM-support for Deductive Verification of Java Programs } --- Workshop on Theorem Proving and Machine Learning in the age of LLMs (Edinburgh, UK)
\item \textbf{ 2024}:\textbf{ Heterogeneous Dynamic Logic } --- KeY Symposium (Bad Herrenalb, Germany)
\item \textbf{ 2024}:\textbf{ Provably Safe Neural Network Controllers via Differential Dynamic Logic } --- Symposium on AI Verification (Montreal, Canada)
\item \textbf{ 2023}:\textbf{ An Information-Flow Perspective on Algorithmic Fairness } --- KeY Symposium (Bergen, Norway)
\end{itemize}


\CVSection{Teaching Experience}
\begin{itemize}[leftmargin=*]
\item \textbf{ Summer 2026 }: Formal Systems II: Theory (Guest Lecture: Heterogeneous Dynamic Logic)
\item \textbf{ November 2025 }: Verification and Validation of Autonomous Systems with Neural Network Components at Heriot-Watt University, Edinburgh (Guest Lecture \& Lab on VerSAILLE)
\item \textbf{ Winter 2025/26 }: Formal Systems (Teaching assistant \& lecturer for first order logic)
\item \textbf{ Summer 2025 }: Seminar "Fairness and Non-Discrimination from the viewpoint of Computer Science and Philosophy" (Organizer \& Student advisor)
\item \textbf{ Summer 2025 }: Seminar "LLMs in Formal Verification" (Student advisor)
\item \textbf{ Summer 2025 }: Lecture "Formal Systems II: Applications" (2 Guest Lectures: Neural Network Verification together with Philipp Kern)
\item \textbf{ Winter 2024/25 }: Seminar "Neural Networks in Formal Verification" (Co-Organizer \& Student advisor)
\item \textbf{ Winter 2024/25 }: Formal Systems (Teaching assistant)
\item \textbf{ October 2024 }: Verification and Validation of Autonomous Systems with Neural Network Components at Heriot-Watt University, Edinburgh (Guest Lecture \& Lab on VerSAILLE)
\item \textbf{ Winter 2023/24 }: Formal Systems (Teaching assistant)
\item \textbf{ Summer 2023 }: Seminar "Fairness and Non-Discrimination from the Perspective of Ethics and Computer Science" (Co-Organizer)
\item \textbf{ Summer 2023 }: Proseminar "Differentiable Programming" (Co-Organizer \& Student advisor)
\item \textbf{ Winter 2022/23 }: Formal Systems (Teaching assistant)
\item \textbf{ Winter 2020/21 }: Programming Paradigms (Student teaching assistant)
\item \textbf{ Winter 2019/20 }: Programming Paradigms (Student teaching assistant)
\end{itemize}

\ifshowstudentsupervision
\CVSubsection{Student Supervision}
\begin{itemize}[leftmargin=*]
\item \textbf{ Summer 2026 }:  Bachelor's Thesis --- Modelling and Verification of Multi-Obstacle Systems in Heterogeneous Dynamic Logic
\item \textbf{ Summer 2026 }:  Bachelor's Thesis --- Bernstein Polynomial Set Representations for Optimizable Neural Network Verification
\item \textbf{ 2025/26 }:  1 year research internship --- Synthesis of Auxiliary Specifications via Large Language Models
\item \textbf{ Winter 2025/26 }:  Bachelor's Thesis --- Differential Verification of Non-ReLU Neural Networks
\item \textbf{ Winter 2025/26 }:  Bachelor's Thesis --- LP-free Neuron Splitting for Neural Network Equivalence Verification
\item \textbf{ Winter 2025/26 }:  Bachelor's Thesis --- Differential Verification for Computational Graphs
\item \textbf{ Winter 2025/26 }:  HiWi --- Reengineering NCubeV's Backends
\item \textbf{ Summer 2025 }:  Research Lab --- Experimental Evaluation of Tools and LLMs for Generating Loop Invariants
\item \textbf{ 2024/25 }:  1 year research internship --- Efficient NN Verification via LP-based Conflict Learning
\item \textbf{ Summer 2024 }:  Bachelor's Thesis --- Improving Zonotope-Based Neural Network Verification via Gradient-Based Optimization
\item \textbf{ Summer 2024 }:  Bachelor's Thesis --- Conflict Analysis for Simplex-Based Neural Network Verification via Farkas Vectors
\item \textbf{ Summer 2024 }:  Research Lab --- Generation of loop specifications using large language models
\item \textbf{ Summer 2024 }:  Research Lab --- Generation of submethod specifications using large language models(german)
\item \textbf{ Summer 2023 }:  Bachelor's Thesis --- Abstraction-refinement based Equivalence Verification of Convolutional Neural Networks
\item \textbf{ Summer 2023 }:  Bachelor's Thesis --- Dimensionality Reduction for Neural Network Verification
\item \textbf{ Summer 2023 }:  Research Lab --- Large Language Models for the synthesis of JML-Specifications
\end{itemize}
\fi

\CVSection{Professional Service}
\begin{itemize}[leftmargin=*]
\item \textbf{ Conference Reviews }: NeurIPS (2026); NeurIPS (2025); AAAI (2025); ICML (2025); AISTATS (2025); AAAI SRRAI Track (2024); NeurIPS (2024)
\item \textbf{ Subreviews }: FM (2026,2024); POPL (2025); LICS (2025); ICTAC (2024); iFM (2023); LICS (2023)
\item \textbf{ Journal Reviews }: Science of Computer Programming (2024/2025)
\end{itemize}


\CVSection{References}
Available upon request

\end{document}
