OOPSLA

\documentclass[acmsmall,screen]{acmart}
\acmJournal{PACMPL}
\acmVolume{8} \acmNumber{OOPSLA} \acmArticle{333}
\acmYear{2026} \acmMonth{10}
\acmDOI{10.1145/XXXXXXX.XXXXXXX}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}

\newtheorem{theorem}{Theorem}

\begin{document}

\title{Sound Inference of Rust Lifetimes via\\
       Borrowed Reference Abstract Interpretation}

\author{First Last}
\affiliation{\institution{University of Example}\country{Country}}
\email{[email protected]}
\author{Jane Doe}
\affiliation{\institution{Example Research Labs}\country{Country}}
\email{[email protected]}
\renewcommand{\shortauthors}{Last and Doe}

\begin{abstract}
Rust's borrow checker infers lifetimes syntactically and sometimes
rejects sound programs. We present a semantic abstract interpretation
over a fragment of Rust that accepts strictly more programs while
remaining sound. Our implementation, ChronoRust, type-checks 92\% of
the \texttt{unsafe} blocks in 50 open-source crates as safe.
\end{abstract}

\begin{CCSXML}
<ccs2012><concept><concept_id>10011007.10011006.10011041</concept_id>
<concept_desc>Software and its engineering~Compilers</concept_desc></concept></ccs2012>
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~Compilers}
\keywords{Rust, ownership, abstract interpretation}
\maketitle

\section{Introduction}
Rust's borrow checker is famously strict. Workarounds involve
\texttt{unsafe}, which bypasses guarantees.

\section{Background}
Borrow checking, lifetime inference, ownership types.

\section{Design}
ChronoRust performs semantic abstract interpretation over an ownership
lattice richer than the syntactic lifetimes of stock Rust.

\section{Soundness}
\begin{theorem}
Programs accepted by ChronoRust enjoy the same memory-safety guarantees
as those accepted by stock Rust.
\end{theorem}

\section{Evaluation}
\begin{table}[t]
\centering
\begin{tabular}{lcc}
\toprule
Crate & Stock rejections & \textbf{ChronoRust accepts} \\
\midrule
serde  & 14 & \textbf{12} \\
tokio  & 23 & \textbf{19} \\
rayon  & 11 & \textbf{11} \\
\bottomrule
\end{tabular}
\end{table}

\section{Conclusion}
Semantic analysis can strictly improve borrow-checking coverage while
preserving safety.

\bibliographystyle{ACM-Reference-Format}
\bibliography{refs}
\end{document}