\documentclass[a4paper,10pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[textwidth=145mm,textheight=224mm]{geometry}
\usepackage{microtype,amsmath,amssymb,amsthm,stmaryrd}
\usepackage{xcolor,graphicx,booktabs,multirow,tikz}
\usetikzlibrary{arrows.meta,positioning,fit,calc,backgrounds}
\usepackage{hyperref}
\usepackage[nameinlink]{cleveref}
\newtheorem{theorem}{Theorem}
\setlength{\emergencystretch}{1.5em}
\input{macros}
\input{generated/stats}
\title{Voblint: End-to-End Soundness of a Context-Sensitive Goblint-Style Analyzer in Isabelle/HOL}
\author{Manuel Lerchner\\Technical University of Munich, Germany\\\texttt{manuel.lerchner@tum.de}}
\date{Preprint}
\hypersetup{pdftitle={Voblint: End-to-End Soundness of a Context-Sensitive Goblint-Style Analyzer in Isabelle/HOL},pdfauthor={Manuel Lerchner}}
\bibliographystyle{plainurl}
\begin{document}
\maketitle
\input{sections/abstract}
\noindent\textbf{Keywords:} abstract interpretation, interprocedural analysis, calling contexts, side-effecting constraint systems, verified static analysis, Isabelle/HOL.
\par\smallskip
\noindent\textbf{Related version:} Master's thesis~\cite{lerchner26thesis}.\par
\noindent\textbf{Software:} Isabelle/HOL formalization and analyzer~\cite{voblint}, \url{https://doi.org/10.5281/zenodo.23260696}.\par
\noindent\textcopyright\ Manuel Lerchner. Licensed under CC BY 4.0.


\input{sections/introduction}
\input{sections/overview}
\input{sections/traces}
\input{sections/equations}
\input{sections/theorem}
\input{sections/mechanization}
\input{sections/evaluation}
\input{sections/related}
\input{sections/conclusion}

\input{sections/statements}

% Read by tools/pages.py: the last page counted against the page limit.
\label{paper:body-end}
\bibliography{generated/references}

\end{document}