@inproceedings{lean4,
  author    = {Leonardo de Moura and Sebastian Ullrich},
  title     = {The {Lean} 4 Theorem Prover and Programming Language},
  booktitle = {Automated Deduction -- CADE 28},
  series    = {LNCS},
  volume    = {12699},
  pages     = {625--635},
  publisher = {Springer},
  year      = {2021}
}

@misc{clangir,
  author       = {{The LLVM Project}},
  title        = {{ClangIR}: a high-level {MLIR} dialect for {C} and {C++}},
  howpublished = {\url{https://llvm.github.io/clangir/}; upstream llvm-project commit 4955d32b used here},
  year         = {2026}
}

@inproceedings{soot,
  author    = {Raja Vall{\'e}e-Rai and Phong Co and Etienne Gagnon and Laurie Hendren and Patrick Lam and Vijay Sundaresan},
  title     = {Soot -- a {Java} Bytecode Optimization Framework},
  booktitle = {Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (CASCON)},
  year      = {1999}
}

@misc{gnucobol,
  author       = {{GnuCOBOL contributors}},
  title        = {{GnuCOBOL} 3.2},
  howpublished = {\url{https://gnucobol.sourceforge.io/}},
  year         = {2023}
}

@misc{carddemo,
  author       = {{Amazon Web Services}},
  title        = {{CardDemo}: a mainframe credit-card application for migration tools},
  howpublished = {\url{https://github.com/aws-samples/aws-mainframe-modernization-carddemo}, commit 59cc6c2f},
  year         = {2025}
}

@misc{carddemo64,
  author       = {son-risa},
  title        = {{CBACT04C} ({INTCALC}): the last account's interest is written as a transaction but never added to the account},
  howpublished = {CardDemo issue \#64, \url{https://github.com/aws-samples/aws-mainframe-modernization-carddemo/issues/64}},
  year         = {2026},
  note         = {Opened 2026-10-03}
}

@misc{carddemo54,
  author       = {Michael Tautschnig},
  title        = {Bound externally-controlled reference-modification lengths and subscripts},
  howpublished = {CardDemo pull request \#54, \url{https://github.com/aws-samples/aws-mainframe-modernization-carddemo/pull/54}},
  year         = {2026},
  note         = {Opened 2026-06-17}
}

@article{aeneas,
  author  = {Son Ho and Jonathan Protzenko},
  title   = {Aeneas: {Rust} Verification by Functional Translation},
  journal = {Proceedings of the ACM on Programming Languages},
  volume  = {6},
  number  = {ICFP},
  year    = {2022},
  pages = {711--741}
}

@inproceedings{charon,
  author    = {Son Ho and Guillaume Boisseau and Lucas Franceschino and Yoann Prak and Aymeric Fromherz and Jonathan Protzenko},
  title     = {Charon: An Analysis Framework for {Rust}},
  booktitle = {Computer Aided Verification (CAV)},
  series    = {LNCS},
  pages     = {377--391},
  publisher = {Springer},
  year      = {2025},
  doi       = {10.1007/978-3-031-98685-7_18}
}

@misc{circe,
  author       = {Petr Bauch},
  title        = {circe: {Lean}-based verification tool for {C++}},
  howpublished = {\url{https://github.com/petr-bauch/circe}, public since 2026-09-21},
  year         = {2026}
}

@misc{veircir,
  author       = {{opencompl}},
  title        = {{VeIR} pull request \#1346: cir: add the {CIR} integer and core dialect},
  howpublished = {\url{https://github.com/opencompl/veir/pull/1346}, merged 2026-09-02},
  year         = {2026}
}

@misc{cir2c,
  author       = {{Anonymous}},
  title        = {Unlocking {C++} for {C} verifiers using {ClangIR} (accompanying artifact)},
  howpublished = {Zenodo, \url{https://doi.org/10.5281/zenodo.21042196}; \url{https://github.com/ftsrg/cir2c}},
  year         = {2026}
}

@misc{brick,
  author       = {{SkyLabs AI}},
  title        = {{BRiCk} and brick-libcpp: separation-logic specifications of {C++} and its standard library in {Rocq}},
  howpublished = {\url{https://github.com/SkyLabsAI/BRiCk} and \url{https://github.com/SkyLabsAI/brick-libcpp}},
  year         = {2025}
}

@inproceedings{leanmlir,
  author    = {Siddharth Bhat and Alex Keizer and Chris Hughes and Andr{\'e}s Goens and Tobias Grosser},
  title     = {Verifying Peephole Rewriting in {SSA} Compiler {IRs}},
  booktitle = {Interactive Theorem Proving (ITP)},
  series    = {LIPIcs},
  year      = {2024},
  volume = {309},
  articleno = {9}
}

@article{esbmccpp,
  author    = {Xianzhiyu Li and Kunjian Song and Mikhail R. Gadelha and Franz Brau{\ss}e and Rafael S. Menezes and Konstantin Korovin and Lucas C. Cordeiro},
  title     = {{ESBMC} v7.6: Enhanced Model Checking of {C++} Programs with Clang {AST}},
  journal   = {Science of Computer Programming},
  volume    = {246},
  pages     = {103336},
  year      = {2025},
  doi       = {10.1016/j.scico.2025.103336}
}

@misc{claws,
  author       = {Phillip Pape},
  title        = {claws: Laws for {C++}},
  howpublished = {\url{https://github.com/paperview/claws}, created 2026-10-23},
  year         = {2026}
}

@inproceedings{bytebackfm,
  author    = {Marco Paganoni and Carlo A. Furia},
  title     = {Verifying Functional Correctness Properties at the Level of {Java} Bytecode},
  booktitle = {Formal Methods (FM)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2023}
}

@inproceedings{bytebackifm,
  author    = {Marco Paganoni and Carlo A. Furia},
  title     = {Reasoning About Exceptional Behavior at the Level of {Java} Bytecode},
  booktitle = {Integrated Formal Methods (iFM)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2023}
}

@inproceedings{bytebackfase,
  author    = {Marco Paganoni and Carlo A. Furia},
  title     = {Reasoning about Substitutability at the Level of {JVM} Bytecode},
  booktitle = {Fundamental Approaches to Software Engineering (FASE)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2025}
}

@inproceedings{kjava,
  author    = {Denis Bogd{\u{a}}na{\c{s}} and Grigore Ro{\c{s}}u},
  title     = {{K-Java}: A Complete Semantics of {Java}},
  booktitle = {Principles of Programming Languages (POPL)},
  publisher = {ACM},
  year      = {2015}
}

@inproceedings{acl2m6,
  author    = {Hanbing Liu and J Strother Moore},
  title     = {Executable {JVM} Model for Analytical Reasoning: A Study},
  booktitle = {Workshop on Interpreters, Virtual Machines and Emulators (IVME)},
  publisher = {ACM},
  year      = {2003}
}

@inproceedings{jinjainit,
  author    = {Susannah Mansky and Elsa L. Gunter},
  title     = {Dynamic Class Initialization Semantics: A {Jinja} Extension},
  booktitle = {Certified Programs and Proofs (CPP)},
  publisher = {ACM},
  year      = {2019}
}

@inproceedings{keystrings,
  author    = {Richard Bubel and Reiner H{\"a}hnle and Ulrich Geilmann},
  title     = {A Formalisation of {Java} Strings for Program Specification and Verification},
  booktitle = {Software Engineering and Formal Methods (SEFM)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2011}
}

@inproceedings{jayhorn,
  author    = {Temesghen Kahsai and Philipp R{\"u}mmer and Huascar Sanchez and Martin Sch{\"a}f},
  title     = {{JayHorn}: A Framework for Verifying {Java} Programs},
  booktitle = {Computer Aided Verification (CAV)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2016}
}

@inproceedings{esbmcjimple,
  author    = {Rafael Menezes and Daniel Moura and Helena Cavalcante and Rosiane de Freitas and Lucas C. Cordeiro},
  title     = {{ESBMC-Jimple}: Verifying {Kotlin} Programs via {Jimple} Intermediate Representation},
  booktitle = {International Symposium on Software Testing and Analysis (ISSTA), tool demonstrations},
  publisher = {ACM},
  year      = {2022}
}

@misc{ironproof,
  author       = {Dominik Blain},
  title        = {{IRONPROOF}: {COBOL}-to-{Python} Transpilation with {SMT}-Based Equivalence Checking},
  howpublished = {arXiv:2610.11073},
  year         = {2026}
}

@misc{cobolequiv,
  author       = {Abdulaziz Abdujalilov},
  title        = {cobol-equiv: differential testing harness and a {Python} runtime for {COBOL} numeric semantics},
  howpublished = {\url{https://github.com/abdulazizbalu/cobol-equiv}, created 2026-10-13},
  year         = {2026}
}

@inproceedings{fieldramalingam,
  author    = {John Field and G. Ramalingam},
  title     = {Identifying Procedural Structure in {Cobol} Programs},
  booktitle = {Workshop on Program Analysis for Software Tools and Engineering (PASTE)},
  publisher = {ACM},
  year      = {1999}
}

@misc{amexmigration,
  author       = {Andras Ferenczi and Jordan Docherty and Mariya Bessonov and Matthew Findlay and Krishna Lingamneni},
  title        = {Agentic Method for Deterministic Validation of Legacy Code Migration},
  howpublished = {arXiv:2607.28271},
  year         = {2026}
}

@inproceedings{ibmcobjava,
  author    = {Atul Kumar and Diptikalyan Saha and Toshiaki Yasue and Kohichi Ono and Saravanan Krishnan and Sandeep Hans and Fumiko Satoh and Gerald Mitchell and Sachin Kumar},
  title     = {Automated Validation of {COBOL} to {Java} Transformation},
  booktitle = {39th IEEE/ACM International Conference on Automated Software Engineering (ASE)},
  pages     = {2415--2418},
  publisher = {ACM},
  year      = {2024},
  doi       = {10.1145/3691620.3695365}
}

@misc{thales,
  author       = {Jesse Alama},
  title        = {Thales and {Tarski}: a proof tool for {TypeScript} and a {JavaScript} semantics in {Lean} 4},
  howpublished = {\url{https://github.com/lakatos-ts/thales}},
  year         = {2026}
}

@misc{lemmascript,
  author       = {{Midspiral}},
  title        = {{LemmaScript}: a verification toolchain for {TypeScript}},
  howpublished = {\url{https://github.com/midspiral/LemmaScript}},
  year         = {2026}
}

@misc{floatmodel,
  author       = {{Lean FRO}},
  title        = {Lean pull request \#14079: \texttt{Float.Model}},
  howpublished = {\url{https://github.com/leanprover/lean4/pull/14079}, merged 2026-06-17},
  year         = {2026}
}

@misc{floatlib,
  author       = {Robert Joseph George and Will Adkisson and Anima Anandkumar},
  title        = {{FloatLib}: Verified Floating-Point Arithmetic in {Lean}},
  howpublished = {arXiv:2609.19352},
  year         = {2026}
}

@inproceedings{jscert,
  author    = {Martin Bodin and Arthur Chargu{\'e}raud and Daniele Filaretti and Philippa Gardner and Sergio Maffeis and Daiva Naud{\v{z}}i{\=u}nien{\.e} and Alan Schmitt and Gareth Smith},
  title     = {A Trusted Mechanised {JavaScript} Specification},
  booktitle = {Principles of Programming Languages (POPL)},
  publisher = {ACM},
  year      = {2014}
}

@inproceedings{kjs,
  author    = {Daejun Park and Andrei {\c{S}}tef{\u{a}}nescu and Grigore Ro{\c{s}}u},
  title     = {{KJS}: A Complete Formal Semantics of {JavaScript}},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {ACM},
  year      = {2015}
}

@inproceedings{gillian,
  author    = {Jos{\'e} Fragoso Santos and Petar Maksimovi{\'c} and Sacha-{\'E}lie Ayoun and Philippa Gardner},
  title     = {Gillian, Part {I}: A Multi-Language Platform for Symbolic Execution},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {ACM},
  year      = {2020}
}

@inproceedings{javertclick,
  author    = {Gabriela Sampaio and Jos{\'e} Fragoso Santos and Petar Maksimovi{\'c} and Philippa Gardner},
  title     = {A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
  series    = {LIPIcs},
  year      = {2020}
}

@inproceedings{esverify,
  author    = {Christopher Schuster and Sohum Banerjea and Cormac Flanagan},
  title     = {esverify: Verifying Dynamically-Typed Higher-Order Functional Programs by {SMT} Solving},
  booktitle = {Implementation and Application of Functional Languages (IFL)},
  publisher = {ACM},
  year      = {2018}
}

@inproceedings{mold,
  author    = {Cosmin Radoi and Stephen J. Fink and Rodric Rabbah and Manu Sridharan},
  title     = {Translating Imperative Code to {MapReduce}},
  booktitle = {Object-Oriented Programming, Systems, Languages \& Applications (OOPSLA)},
  publisher = {ACM},
  year      = {2014}
}

@misc{hax,
  author       = {{Cryspen}},
  title        = {hax: a {Rust} verification tool chain},
  howpublished = {\url{https://github.com/pereq-dev/hax} (formerly cryspen/hax)},
  year         = {2026}
}

@misc{sawffs,
  author       = {{Galois}},
  title        = {{SAW} tutorial: cross-language proofs of find-first-set in {C} and {Java}},
  howpublished = {\url{https://github.com/GaloisInc/saw-script}, first version 2013-06-07},
  year         = {2013}
}

@inproceedings{saw,
  author    = {Robert Dockins and Adam Foltzer and Joe Hendrix and Brian Huffman and Dylan McNamee and Aaron Tomb},
  title     = {Constructing Semantic Models of Programs with the Software Analysis Workbench},
  booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2016}
}

@inproceedings{keq,
  author    = {Theodoros Kasampalis and Daejun Park and Zhengyao Lin and Vikram S. Adve and Grigore Ro{\c{s}}u},
  title     = {Language-Parametric Compiler Validation with Application to {LLVM}},
  booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
  publisher = {ACM},
  year      = {2021}
}

@article{ciobaca,
  author  = {{\c{S}}tefan Ciob{\^a}c{\u{a}} and Dorel Lucanu and Vlad Rusu and Grigore Ro{\c{s}}u},
  title   = {A Language-Independent Proof System for Full Program Equivalence},
  journal = {Formal Aspects of Computing},
  volume  = {28},
  year    = {2016},
  number = {3},
  pages = {469--497}
}

@inproceedings{sewell,
  author    = {Thomas Sewell and Magnus O. Myreen and Gerwin Klein},
  title     = {Translation Validation for a Verified {OS} Kernel},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {ACM},
  year      = {2013}
}

@inproceedings{libm,
  author    = {Mark S. Baranowski and Zvonimir Rakamari{\'c} and Ganesh Gopalakrishnan},
  title     = {Equivalence Checking of a libm Port},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  series    = {LNCS},
  pages     = {239--256},
  publisher = {Springer},
  year      = {2025},
  doi       = {10.1007/978-3-031-90653-4_12}
}

@misc{leanplverify,
  author       = {Anand Kumar Keshavan},
  title        = {lean-pl-verify: formal verification of {Rust} and {TypeScript} programs in {Lean} 4},
  howpublished = {\url{https://github.com/akkeshavan/lean-pl-verify}, created 2026-05-28},
  year         = {2026}
}

@misc{rem2,
  author       = {Matthew Britton and Sasha Pak and Alex Potanin},
  title        = {Refactoring and Equivalence in {Rust}: Expanding the {REM} Toolchain with a Novel Approach to Automated Equivalence Proofs},
  howpublished = {arXiv:2601.19207},
  year         = {2026}
}

@misc{refinemonadic,
  author       = {Peter Lammich},
  title        = {Refinement for Monadic Programs},
  howpublished = {Archive of Formal Proofs, \url{https://www.isa-afp.org/entries/Refine_Monadic.html}},
  year         = {2012}
}

@misc{l4v,
  author       = {{seL4 project}},
  title        = {l4v: {seL4} proofs, \texttt{lib/CorresWhile.thy}},
  howpublished = {\url{https://github.com/seL4/l4v}},
  year         = {2026}
}

@article{compcert,
  author  = {Xavier Leroy},
  title   = {A Formally Verified Compiler Back-end},
  journal = {Journal of Automated Reasoning},
  volume  = {43},
  number  = {4},
  pages   = {363--446},
  year    = {2009}
}

@misc{aqueduct,
  author       = {Zhe Ye and Udaya Ghai and Zhizhen Qin and Dawn Song and Soonho Kong},
  title        = {Agentic Verified Optimization of Real-World Software},
  howpublished = {arXiv:2610.30188},
  year         = {2026}
}

@misc{anthropictheorem,
  author       = {Keane Lucas and Aengus Lynch and Luna Tong and Luke Champine and Zygi Straznickas and Dino Distefano and Harshikaa Agrawal and Evyatar {Ben Asher} and Ava Howell and Sami Jawhar and Chris Rohlf and Nickolai Zeldovich and Nicholas Carlini and Rajashree Agrawal and Jason Gross},
  title        = {{LLMs} are making formal software verification feasible at a much larger scale},
  howpublished = {Anthropic research post with Theorem, \url{https://www.anthropic.com/research/formal-verification}},
  year         = {2026},
  note         = {Published 2026-10-22}
}

@misc{partialcontracts,
  author       = {Yiannis Charalambous and Rafael Menezes and Youcheng Sun and Lucas C. Cordeiro},
  title        = {Partial Contracts Suffice: Sound, {LLM}-Inferred Regression Verification},
  howpublished = {arXiv:2607.10291},
  year         = {2026}
}

@misc{trivet,
  author       = {Chunhao Liao and Hongxu Xu and Xintong Zhou and Yizhou Zhang and Chengnian Sun},
  title        = {{LLVM} Translation Validation Automated with Large Language Models and {Lean}},
  howpublished = {arXiv:2609.19583},
  year         = {2026}
}

@misc{ccv,
  author       = {Haokun Li and Zhongyi Wang and Guanyan Li and Xiao Yi and Shengchao Qin and Jianwei Yin and Mingshuai Chen},
  title        = {Automatically Building Machine-Checked Assurance Cases from {C} Codebases to Requirements},
  howpublished = {arXiv:2609.40119},
  year         = {2026}
}

@misc{verdict,
  author       = {Tengjie Lin and Zhongyi Wang and Haokun Li and Jianwei Yin and Mingshuai Chen},
  title        = {{VERDICT}: Multi-Agent Parallel Modular Verification},
  howpublished = {arXiv:2610.29147},
  year         = {2026}
}

@inproceedings{autospec,
  author    = {Cheng Wen and Jialun Cao and Jie Su and Zhiwu Xu and Shengchao Qin and Mengda He and Haokun Li and Shing-Chi Cheung and Cong Tian},
  title     = {Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification},
  booktitle = {Computer Aided Verification (CAV)},
  series    = {LNCS},
  pages     = {302--328},
  publisher = {Springer},
  year      = {2024},
  doi       = {10.1007/978-3-031-65630-9_16}
}

@inproceedings{alphaverus,
  author    = {Pranjal Aggarwal and Bryan Parno and Sean Welleck},
  title     = {{AlphaVerus}: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement},
  booktitle = {Proceedings of the 42nd International Conference on Machine Learning (ICML)},
  series    = {PMLR},
  volume    = {267},
  pages     = {587--615},
  year      = {2025}
}

@article{autoverus,
  author    = {Chenyuan Yang and Xuheng Li and Md Rakib Hossain Misu and Jianan Yao and Weidong Cui and Yeyun Gong and Chris Hawblitzel and Shuvendu Lahiri and Jacob R. Lorch and Shuai Lu and Fan Yang and Ziqiao Zhou and Shan Lu},
  title     = {{AutoVerus}: Automated Proof Generation for {Rust} Code},
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {9},
  number    = {OOPSLA2},
  pages     = {3454--3482},
  year      = {2025},
  doi       = {10.1145/3763174}
}

@inproceedings{lemur,
  author    = {Haoze Wu and Clark Barrett and Nina Narodytska},
  title     = {Lemur: Integrating Large Language Models in Automated Program Verification},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year      = {2024}
}

@inproceedings{clover,
  author    = {Chuyue Sun and Ying Sheng and Oded Padon and Clark Barrett},
  title     = {Clover: Closed-Loop Verifiable Code Generation},
  booktitle = {AI Verification (SAIV 2024)},
  series    = {LNCS},
  volume    = {14846},
  pages     = {134--155},
  publisher = {Springer},
  year      = {2024},
  doi       = {10.1007/978-3-031-65112-0_7}
}

@inproceedings{leinowustholz,
  author    = {K. Rustan M. Leino and Valentin W{\"u}stholz},
  title     = {Fine-Grained Caching of Verification Results},
  booktitle = {Computer Aided Verification (CAV)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2015}
}

@inproceedings{dac,
  author    = {Shuvendu K. Lahiri and Kenneth L. McMillan and Rahul Sharma and Chris Hawblitzel},
  title     = {Differential Assertion Checking},
  booktitle = {Foundations of Software Engineering (ESEC/FSE)},
  publisher = {ACM},
  year      = {2013}
}

@inproceedings{infer,
  author    = {Cristiano Calcagno and Dino Distefano and J{\'e}r{\'e}my Dubreil and Dominik Gabi and Pieter Hooimeijer and Martino Luca and Peter O'Hearn and Irene Papakonstantinou and Jim Purbrick and Dulma Rodriguez},
  title     = {Moving Fast with Software Verification},
  booktitle = {NASA Formal Methods (NFM)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2015}
}

@inproceedings{alive2,
  author    = {Nuno P. Lopes and Juneyoung Lee and Chung-Kil Hur and Zhengyang Liu and John Regehr},
  title     = {{Alive2}: Bounded Translation Validation for {LLVM}},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {ACM},
  year      = {2021}
}

@inproceedings{houdini,
  author    = {Cormac Flanagan and K. Rustan M. Leino},
  title     = {Houdini, an Annotation Assistant for {ESC/Java}},
  booktitle = {Formal Methods Europe (FME)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2001}
}

@article{daikon,
  author  = {Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and Chen Xiao},
  title   = {The {Daikon} System for Dynamic Detection of Likely Invariants},
  journal = {Science of Computer Programming},
  volume  = {69},
  year    = {2007},
  number = {1--3},
  pages = {35--45}
}

@inproceedings{pie,
  author    = {Saswat Padhi and Rahul Sharma and Todd Millstein},
  title     = {Data-Driven Precondition Inference with Learned Features},
  booktitle = {Programming Language Design and Implementation (PLDI)},
  publisher = {ACM},
  year      = {2016}
}

@inproceedings{godlinstrichman,
  author    = {Benny Godlin and Ofer Strichman},
  title     = {Regression Verification},
  booktitle = {Design Automation Conference (DAC)},
  publisher = {ACM},
  year      = {2009}
}

@inproceedings{reve,
  author    = {Dennis Felsing and Sarah Grebing and Vladimir Klebanov and Philipp R{\"u}mmer and Mattias Ulbrich},
  title     = {Automating Regression Verification},
  booktitle = {Automated Software Engineering (ASE)},
  publisher = {ACM},
  year      = {2014}
}

@inproceedings{symdiff,
  author    = {Shuvendu K. Lahiri and Chris Hawblitzel and Ming Kawaguchi and Henrique Reb{\^e}lo},
  title     = {{SymDiff}: A Language-Agnostic Semantic Diff Tool for Imperative Programs},
  booktitle = {Computer Aided Verification (CAV)},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2012}
}

@misc{codemender,
  author       = {{Google DeepMind}},
  title        = {Introducing {CodeMender}: an {AI} agent for code security},
  howpublished = {Blog post, \url{https://deepmind.google/blog/introducing-codemender-an-ai-agent-for-code-security/}},
  year         = {2025},
  note         = {Published 2025-10-06}
}

@misc{autoform,
  author       = {mbhatt1},
  title        = {autoform: autoformalized {Lean} 4 for an arbitrary codebase via a formal interpreter},
  howpublished = {\url{https://github.com/mbhatt1/autoform}, created 2026-08-20},
  year         = {2026}
}

@misc{jverify,
  author       = {{Strata}},
  title        = {{JVerify}: program verification for {Java}},
  howpublished = {\url{https://github.com/strata-org/jverify}},
  year         = {2025}
}

@misc{algorithmscpp,
  author       = {{The Algorithms}},
  title        = {{TheAlgorithms/C-Plus-Plus}},
  howpublished = {\url{https://github.com/TheAlgorithms/C-Plus-Plus}, commit fdcc29b},
  year         = {2026}
}

@misc{algorithmsts,
  author       = {{The Algorithms}},
  title        = {{TheAlgorithms/TypeScript}},
  howpublished = {\url{https://github.com/TheAlgorithms/TypeScript}, commit 19b4ced},
  year         = {2024}
}

@misc{estoolkit,
  author       = {{Toss}},
  title        = {es-toolkit v1.52.0},
  howpublished = {\url{https://github.com/toss/es-toolkit}, commit 32f4c8f},
  year         = {2026}
}

@misc{jsmn,
  author       = {Serge Zaitsev},
  title        = {jsmn: a minimalistic {JSON} parser in {C}},
  howpublished = {\url{https://github.com/zserge/jsmn}},
  year         = {2026}
}

@misc{tinyregex,
  author       = {kokke},
  title        = {tiny-regex-c},
  howpublished = {\url{https://github.com/kokke/tiny-regex-c}},
  year         = {2026}
}

@misc{cjson,
  author       = {Dave Gamble and {cJSON contributors}},
  title        = {{cJSON}: ultralightweight {JSON} parser in {ANSI C}},
  howpublished = {\url{https://github.com/DaveGamble/cJSON}},
  year         = {2026}
}

@misc{lang3,
  author       = {{The Apache Software Foundation}},
  title        = {Apache Commons Lang 3.14.0},
  howpublished = {\url{https://commons.apache.org/proper/commons-lang/}},
  year         = {2023}
}

@article{bali,
  author    = {David von Oheimb},
  title     = {Hoare Logic for {Java} in {Isabelle/HOL}},
  journal   = {Concurrency and Computation: Practice and Experience},
  year      = {2001},
  doi       = {10.1002/cpe.598},
  volume = {13},
  number = {13},
  pages = {1173--1214}
}

@inproceedings{mobius,
  author    = {Benjamin Gr{\'e}goire and Jorge Luis Sacchini},
  title     = {Combining a Verification Condition Generator for a Bytecode Language with Static Analyses},
  booktitle = {Trustworthy Global Computing (TGC 2007)},
  series    = {LNCS},
  volume    = {4912},
  publisher = {Springer},
  year      = {2008},
  doi       = {10.1007/978-3-540-78663-4_4}
}

@article{loom,
  author    = {Vladimir Gladshtein and George P{\^\i}rlea and Qiyuan Zhao and Vitaly Kurin and Ilya Sergey},
  title     = {Foundational Multi-Modal Program Verifiers},
  journal   = {Proceedings of the ACM on Programming Languages},
  volume    = {10},
  number    = {POPL},
  pages     = {2233--2264},
  year      = {2026},
  doi       = {10.1145/3776719}
}

@techreport{baumann,
  author      = {Peter Baumann and J{\"u}rg F{\"a}ssler and Markus Kiser and Zafer {\"O}zt{\"u}rk},
  title       = {Beauty and the Beast or A Formal Semantic Description of the Control Constructs of {Cobol} and its
                 Implementation},
  institution = {Universit{\"a}t Z{\"u}rich},
  number      = {IFI-93.39},
  year        = {1993}
}

@misc{heimdall,
  author       = {V. A. Dasu and M. Santra and M. R. U. Rashid and A. Kumar and S. Tizpaz-Niari and G. Tan},
  title        = {Heimdall: Formally Verified Automated Migration of Legacy {eBPF} Programs to {Rust}},
  howpublished = {arXiv:2605.25411v2},
  year         = {2026}
}
@misc{browne,
  author       = {A. Browne and E. Lee and C. Salvi},
  title        = {Proving {LLM}-Generated {GPU} Kernels Correct and Safe: Floating-Point Verification in {Lean} and {VerCors}},
  howpublished = {arXiv:2610.24548},
  year         = {2026}
}
@misc{equivm,
  author       = {E. Lazaropoulos and Z. Paraskevopoulou},
  title        = {Foundational Refinement Proofs for {EVM} Bytecode, at the Price of Tokens},
  howpublished = {arXiv:2607.26306v2},
  year         = {2026}
}
@misc{vert,
  author       = {A. Z. H. Yang and Y. Takashima and B. Paulsen and J. Dodds and D. Kroening},
  title        = {{VERT}: Verified Equivalent {Rust} Transpilation with Large Language Models as Few-Shot Learners},
  howpublished = {arXiv:2404.18852v2},
  year         = {2024}
}
@inproceedings{llmlift,
  author       = {S. Bhatia and J. Qiu and N. Hasabnis and S. A. Seshia and A. Cheung},
  title        = {Verified Code Transpilation with {LLMs}},
  booktitle    = {Advances in Neural Information Processing Systems 37 (NeurIPS 2024)},
  year         = {2024}
}
@misc{amexwitness,
  author       = {A. L. Ferenczi and M. Bessonov and A. Ponnudurai and C. R. Mamillapalli and K. K. Maddula and K. K. Lingamneni},
  title        = {Certifying Repeatable Entry-Replay Witnesses for {COBOL}-to-{Java} Migration},
  howpublished = {arXiv:2610.27272},
  year         = {2026}
}
@misc{carddemo32,
  author       = {DukeDeSouth},
  title        = {Fix arithmetic and control flow bugs in batch programs},
  howpublished = {CardDemo pull request \#32, \url{https://github.com/aws-samples/aws-mainframe-modernization-carddemo/pull/32}},
  year         = {2026},
  note         = {Opened 2026-02-24}
}
@inproceedings{pan2024lost,
  author       = {R. Pan and A. R. Ibrahimzada and R. Krishna and D. Sankar and L. P. Wassi and M. Merler and B. Sobolev and R. Pavuluri and S. Sinha and R. Jabbarvand},
  title        = {Lost in Translation: A Study of Bugs Introduced by Large Language Models while Translating Code},
  booktitle    = {Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE)},
  year         = {2024},
  doi          = {10.1145/3597503.3639226}
}
@misc{eniser2024,
  author       = {H. F. Eniser and H. Zhang and C. David and M. Wang and M. Christakis and B. Paulsen and J. Dodds and D. Kroening},
  title        = {Towards Translating Real-World Code with {LLMs}: A Study of Translating to {Rust}},
  howpublished = {arXiv:2405.11514},
  year         = {2024}
}
@misc{chang2025,
  author       = {H. Chang and G. Meng and S. Xiao and K. Chen and Y. Li and K. Sun},
  title        = {When Code Crosses Borders: A Security-Centric Study of {LLM}-based Code Translation},
  howpublished = {arXiv:2509.06504v2},
  year         = {2025}
}
@misc{du2026,
  author       = {Y. Du and Y. Zhang and M. Li},
  title        = {Hallucinations of Large Language Models in Cross-Language Code Translation: Phenomena and Mitigation},
  howpublished = {arXiv:2610.27868},
  year         = {2026}
}
@inproceedings{wang2012ub,
  author       = {X. Wang and H. Chen and A. Cheung and Z. Jia and N. Zeldovich and M. F. Kaashoek},
  title        = {Undefined Behavior: What Happened to My Code?},
  booktitle    = {Proceedings of the Asia-Pacific Workshop on Systems (APSys)},
  year         = {2012},
  doi          = {10.1145/2349896.2349905}
}
@inproceedings{stack2013,
  author       = {X. Wang and N. Zeldovich and M. F. Kaashoek and A. Solar-Lezama},
  title        = {Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior},
  booktitle    = {Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP)},
  year         = {2013},
  doi          = {10.1145/2517349.2522728}
}
@inproceedings{kcc,
  author       = {C. Hathhorn and C. Ellison and G. Ro{\c{s}}u},
  title        = {Defining the Undefinedness of {C}},
  booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
  year         = {2015},
  doi          = {10.1145/2737924.2737979}
}
@misc{theoremossverify,
  author       = {{Theorem Labs, PBC}},
  title        = {{OSS Verify}: proofs and theorem statements about {OSS-Fuzz} fuzz targets, release 2026.10.0},
  howpublished = {\url{https://github.com/theorem-labs/oss-verify-proofs}},
  year         = {2026},
  note         = {Tag v2026.10.0 (commit 8f5f467); read at commit 98e995d, 2026-10-23}
}
@misc{cjson919,
  author       = {imaami},
  title        = {v1.7.19 added Undefined Behavior to \texttt{cJSON\_SetValuestring()}},
  howpublished = {cJSON issue \#919, \url{https://github.com/DaveGamble/cJSON/issues/919}},
  year         = {2024},
  note         = {Opened 2024-12-25; see also pull request \#924 and issue \#1106}
}
@misc{cve202616554,
  author       = {{CERT Polska} and Michal Majchrowicz and Marcin Wyczechowski},
  title        = {{CVE-2026-16554}: {cJSON} \texttt{print\_string\_ptr()} 32-bit \texttt{size\_t} wraparound},
  howpublished = {\url{https://cert.pl/en/posts/2026/07/CVE-2026-16554/}},
  year         = {2026},
  note         = {Published 2026-07-27}
}
@inproceedings{s2n2018,
  author       = {A. Chudnov and N. Collins and B. Cook and J. Dodds and B. Huffman and C. MacC{\'a}rthaigh and S. Magill and E. Mertens and E. Mullen and S. Tasiran and A. Tomb and E. Westbrook},
  title        = {Continuous Formal Verification of {Amazon} s2n},
  booktitle    = {Computer Aided Verification (CAV)},
  year         = {2018},
  doi          = {10.1007/978-3-319-96142-2_26}
}
@inproceedings{chong2020,
  author       = {N. Chong and B. Cook and K. Kallas and K. Khazem and F. R. Monteiro and D. Schwartz-Narbonne and S. Tasiran and M. Tautschnig and M. R. Tuttle},
  title        = {Code-Level Model Checking in the Software Development Workflow},
  booktitle    = {Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)},
  year         = {2020},
  doi          = {10.1145/3377813.3381347}
}
@inproceedings{diffkemp,
  author       = {V. Mal{\'i}k and T. Vojnar},
  title        = {Automatically Checking Semantic Equivalence between Versions of Large-Scale {C} Projects},
  booktitle    = {IEEE Conference on Software Testing, Verification and Validation (ICST)},
  year         = {2021},
  doi          = {10.1109/ICST49551.2021.00045}
}
@inproceedings{sarker2026,
  author       = {L. Sarker and A. Satter and T. Bultan},
  title        = {Quantitative Symbolic Patch Impact Analysis},
  booktitle    = {NASA Formal Methods (NFM 2026)},
  series       = {LNCS},
  pages        = {367--390},
  publisher    = {Springer},
  year         = {2026},
  doi          = {10.1007/978-3-032-28079-4_17}
}
@article{autorocq,
  author       = {H. Tu and H. Zhao and Y. Song and M. Zafar and R. Meng and A. Roychoudhury},
  title        = {Agentic Verification of Software Systems},
  journal      = {Proceedings of the ACM on Software Engineering},
  volume       = {3},
  number       = {FSE},
  articleno    = {FSE157},
  year         = {2026},
  doi          = {10.1145/3808164}
}
@inproceedings{klees2018,
  author       = {G. Klees and A. Ruef and B. Cooper and S. Wei and M. Hicks},
  title        = {Evaluating Fuzz Testing},
  booktitle    = {Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS)},
  year         = {2018},
  doi          = {10.1145/3243734.3243804}
}
@article{registeredreports,
  author       = {N. A. Ernst and M. T. Baldassarre},
  title        = {Registered Reports in Software Engineering},
  journal      = {Empirical Software Engineering},
  volume       = {28},
  number       = {2},
  articleno    = {55},
  year         = {2023},
  doi          = {10.1007/s10664-022-10277-5}
}

@misc{fvtechreport,
  author = {Tejasvi Singh Tomar},
  title = {Proof-Carrying Modernization: Artifact and Technical Report},
  howpublished = {Zenodo},
  year = {2026},
  doi = {10.5281/zenodo.23996137}
}