% generated by paper/tools/bib.py from thesis/literature.bib

@inproceedings{apinis12,
  author    = {Kalmer Apinis and Helmut Seidl and Vesal Vojdani},
  title     = {Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis},
  booktitle = {Programming Languages and Systems ({APLAS} 2012)},
  series    = {LNCS},
  volume    = {7705},
  pages     = {157--172},
  publisher = {Springer},
  year      = {2012},
  doi       = {10.1007/978-3-642-35182-2_12}
}

@article{ballarin14,
  author  = {Clemens Ballarin},
  title   = {Locales: A Module System for Mathematical Theories},
  journal = {Journal of Automated Reasoning},
  volume  = {52},
  number  = {2},
  pages   = {123--153},
  year    = {2014},
  doi     = {10.1007/s10817-013-9284-7}
}

@inproceedings{blazy13,
  author = {Sandrine Blazy and Vincent Laporte and André Maroneze and David Pichardie},
  title = {Formal Verification of a {C} Value Analysis Based on Abstract Interpretation},
  booktitle = {Static Analysis},
  year = {2013},
  pages = {324--344},
  doi = {10.1007/978-3-642-38856-9_18}
}

@article{breitner10afp,
  author = {Joachim Breitner},
  title = {{Shivers'} Control Flow Analysis},
  journal = {Archive of Formal Proofs},
  year = {2010},
  month = nov,
  url = {https://isa-afp.org/entries/Shivers-CFA.html},
  urldate = {2026-09-22}
}

@article{cachera05,
  author  = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu},
  title   = {Extracting a Data Flow Analyser in Constructive Logic},
  journal = {Theoretical Computer Science},
  volume  = {342},
  number  = {1},
  pages   = {56--78},
  year    = {2005},
  doi     = {10.1016/j.tcs.2005.06.004}
}

@inproceedings{cachera10,
  author    = {David Cachera and David Pichardie},
  title     = {A Certified Denotational Abstract Interpreter},
  booktitle = {Interactive Theorem Proving ({ITP} 2010)},
  series    = {LNCS},
  pages     = {9--24},
  publisher = {Springer},
  year      = {2010},
  doi       = {10.1007/978-3-642-14052-5_3}
}

@inproceedings{dabrowski09,
  author    = {Frédéric Dabrowski and David Pichardie},
  title     = {A Certified Data Race Analysis for a {Java}-like Language},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2009)},
  series    = {LNCS},
  pages     = {212--227},
  year      = {2009},
  doi       = {10.1007/978-3-642-03359-9_16}
}

@article{devilhena20,
  author  = {Paulo Emílio de Vilhena and François Pottier and Jacques-Henri Jourdan},
  title   = {Spy Game: Verifying a Local Generic Solver in {Iris}},
  journal = {Proceedings of the ACM on Programming Languages},
  volume  = {4},
  number  = {POPL},
  pages   = {33:1--33:28},
  year    = {2020},
  doi     = {10.1145/3371101}
}

@inproceedings{franceschino21,
  author    = {Lucas Franceschino and David Pichardie and Jean-Pierre Talpin},
  title     = {Verified Functional Programming of an Abstract Interpreter},
  booktitle = {Static Analysis ({SAS} 2021)},
  series    = {LNCS},
  pages     = {124--143},
  publisher = {Springer},
  year      = {2021},
  doi       = {10.1007/978-3-030-88806-0_6},
  note      = {Hosted browser version: \url{https://w95psp.github.io/verified-abstract-interpreter}}
}

@misc{goblint1161,
  author = {Michael Schwarz},
  title = {Congruences: Make {\%} Sound by Restricting Cases Where We Return a Constant},
  year = {2023},
  url = {https://github.com/goblint/analyzer/pull/1161},
  note = {Pull request 1161},
  urldate = {2026-09-21}
}

@inproceedings{haftmann10,
  author    = {Florian Haftmann and Tobias Nipkow},
  title     = {Code Generation via Higher-Order Rewrite Systems},
  booktitle = {Functional and Logic Programming ({FLOPS} 2010)},
  series    = {LNCS},
  volume    = {6009},
  pages     = {103--117},
  publisher = {Springer},
  year      = {2010},
  doi       = {10.1007/978-3-642-12251-4_9}
}

@inproceedings{hofmann10,
  author    = {Martin Hofmann and Aleksandr Karbyshev and Helmut Seidl},
  title     = {Verifying a Local Generic Solver in {Coq}},
  booktitle = {Static Analysis ({SAS} 2010)},
  series    = {LNCS},
  pages     = {340--355},
  publisher = {Springer},
  year      = {2010},
  doi       = {10.1007/978-3-642-15769-1_21}
}

@inproceedings{huffman13,
  author    = {Brian Huffman and Ondřej Kunčar},
  title     = {Lifting and Transfer: A Modular Design for Quotients in {Isabelle/HOL}},
  booktitle = {Certified Programs and Proofs ({CPP} 2013)},
  series    = {LNCS},
  pages     = {131--146},
  publisher = {Springer},
  year      = {2013},
  doi       = {10.1007/978-3-319-03545-1_9}
}

@inproceedings{jeannet04,
  author    = {Bertrand Jeannet and Wendelin Serwe},
  title     = {Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs},
  booktitle = {Algebraic Methodology and Software Technology ({AMAST} 2004)},
  series    = {Lecture Notes in Computer Science},
  volume    = {3116},
  pages     = {258--273},
  publisher = {Springer},
  year      = {2004},
  doi       = {10.1007/978-3-540-27815-3_22}
}

@inproceedings{jourdan15,
  author    = {Jacques-Henri Jourdan and Vincent Laporte and Sandrine Blazy and Xavier Leroy and David Pichardie},
  title     = {A Formally-Verified {C} Static Analyzer},
  booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
  pages     = {247--259},
  publisher = {ACM},
  year      = {2015},
  doi       = {10.1145/2676726.2676966}
}

@inproceedings{knoop92,
  author    = {Jens Knoop and Bernhard Steffen},
  title     = {The Interprocedural Coincidence Theorem},
  booktitle = {Compiler Construction ({CC} '92)},
  series    = {LNCS},
  volume    = {641},
  pages     = {125--140},
  publisher = {Springer},
  year      = {1992},
  doi       = {10.1007/3-540-55984-1_13}
}

@article{lammich07afp,
  author = {Peter Lammich and Markus Müller-Olm},
  title = {Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors},
  journal = {Archive of Formal Proofs},
  year = {2007},
  month = dec,
  url = {https://isa-afp.org/entries/Program-Conflict-Analysis.html},
  urldate = {2026-09-22}
}

@mastersthesis{lerchner26thesis,
  author = {Manuel Lerchner},
  title  = {{Voblint}: Towards a Verified {Goblint}-Style Analysis Pipeline in {Isabelle/HOL}},
  school = {Technical University of Munich},
  year   = {2026},
  note   = {Draft},
  url    = {https://manuellerchner.github.io/Voblint-Verification-Master-Thesis/thesis.pdf}
}

@article{leroy09,
  author  = {Xavier Leroy},
  title   = {Formal Verification of a Realistic Compiler},
  journal = {Communications of the ACM},
  volume  = {52},
  number  = {7},
  pages   = {107--115},
  year    = {2009},
  doi     = {10.1145/1538788.1538814}
}

@article{michelland24,
  author = {Sébastien Michelland and Yannick Zakowski and Laure Gonnord},
  title = {Abstract Interpreters: A Monadic Approach to Modular Verification},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {ICFP},
  year = {2024},
  doi = {10.1145/3674646}
}

@inproceedings{might09,
  author    = {Matthew Might and Panagiotis Manolios},
  title     = {A Posteriori Soundness for Non-deterministic Abstract Interpretations},
  booktitle = {Verification, Model Checking, and Abstract Interpretation ({VMCAI} 2009)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5403},
  pages     = {260--274},
  publisher = {Springer},
  year      = {2009},
  doi       = {10.1007/978-3-540-93900-9_22}
}

@misc{monniaux24,
  author       = {David Monniaux},
  title        = {Flavors of Abstract Interpretation},
  howpublished = {Invited tutorial, European Joint Conferences on Theory and Practice of Software ({ETAPS} 2024), Luxembourg},
  month        = apr,
  year         = {2024},
  note         = {Lecture slides, HAL hal-04750222},
  url          = {https://hal.science/hal-04750222}
}

@inproceedings{nipkow12,
  author    = {Tobias Nipkow},
  title     = {Abstract Interpretation of Annotated Commands},
  booktitle = {Interactive Theorem Proving ({ITP} 2012)},
  series    = {LNCS},
  pages     = {116--132},
  publisher = {Springer},
  year      = {2012},
  doi       = {10.1007/978-3-642-32347-8_9}
}

@book{nipkow14,
  author    = {Tobias Nipkow and Gerwin Klein},
  title     = {Concrete Semantics with {Isabelle/HOL}},
  publisher = {Springer},
  year      = {2014},
  doi       = {10.1007/978-3-319-10542-0}
}

@inproceedings{reps95,
  author    = {Thomas Reps and Susan Horwitz and Mooly Sagiv},
  title     = {Precise Interprocedural Dataflow Analysis via Graph Reachability},
  booktitle = {Proceedings of the 22nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL})},
  pages     = {49--61},
  publisher = {ACM},
  year      = {1995},
  doi       = {10.1145/199448.199462}
}

@article{rival07,
  author = {Xavier Rival and Laurent Mauborgne},
  title = {The Trace Partitioning Abstract Domain},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {29},
  number = {5},
  year = {2007},
  doi = {10.1145/1275497.1275501}
}

@inproceedings{schwarz21,
  author = {Michael Schwarz and Simmo Saan and Helmut Seidl and Kalmer Apinis and Julian Erhard and Vesal Vojdani},
  title = {Improving Thread-Modular Abstract Interpretation},
  booktitle = {Static Analysis},
  pages = {359--383},
  series = {LNCS},
  volume = {12913},
  year = {2021},
  doi = {10.1007/978-3-030-88806-0_18}
}

@inproceedings{schwarz23,
  author    = {Michael Schwarz and Simmo Saan and Helmut Seidl and Julian Erhard and Vesal Vojdani},
  title     = {Clustered Relational Thread-Modular Abstract Interpretation with Local Traces},
  booktitle = {Programming Languages and Systems (ESOP 2023)},
  pages     = {28--58},
  series    = {LNCS},
  volume    = {13990},
  year      = {2023},
  doi       = {10.1007/978-3-031-30044-8_2}
}

@article{seidl03,
  author  = {Helmut Seidl and Varmo Vene and Markus M{\"u}ller-Olm},
  title   = {Global Invariants for Analysing Multi-threaded Applications},
  journal = {Proceedings of the Estonian Academy of Sciences. Physics. Mathematics},
  volume  = {52},
  number  = {4},
  pages   = {413--436},
  year    = {2003},
  doi     = {10.3176/phys.math.2003.4.05}
}

@inproceedings{seidl26,
  author = {Helmut Seidl and Vesal Vojdani and Julian Erhard and Michael Schwarz},
  title = {Mixed Flow-Sensitive Static Analysis: Engineering Modularity},
  booktitle = {FM 2026: Formal Methods},
  year = {2026},
  pages = {446--470},
  doi = {10.1007/978-3-032-26220-2_22}
}

@incollection{sharir81,
  author    = {Micha Sharir and Amir Pnueli},
  title     = {Two Approaches to Interprocedural Data Flow Analysis},
  booktitle = {Program Flow Analysis: Theory and Applications},
  editor    = {Steven S. Muchnick and Neil D. Jones},
  chapter   = {7},
  publisher = {Prentice-Hall},
  year      = {1981}
}

@inproceedings{stade24,
  author = {Yannick Stade and Sarah Tilscher and Helmut Seidl},
  title = {The Top-Down Solver Verified: Building Confidence in Static Analyzers},
  booktitle = {Computer Aided Verification},
  year = {2024},
  pages = {303--324},
  doi = {10.1007/978-3-031-65627-9_15},
  note = {Formalization: Archive of Formal Proofs entry Top\_Down\_Solver, \url{https://isa-afp.org/entries/Top_Down_Solver.html}}
}

@inproceedings{tilscher26,
  author    = {Sarah Tilscher and Alexandra Gra{\ss} and Helmut Seidl},
  title     = {Verifying a Solver for Mixed Flow-Sensitive Analyses},
  booktitle = {{NASA} Formal Methods ({NFM} 2026)},
  series    = {LNCS},
  pages     = {48--69},
  publisher = {Springer},
  year      = {2026},
  doi       = {10.1007/978-3-032-28079-4_3}
}

@misc{tilscher26artifact,
  author = {Sarah Tilscher and Alexandra Gra{\ss} and Helmut Seidl},
  title = {Verifying a Solver for Mixed Flow-Sensitive Analyses (Artifact)},
  year = {2026},
  publisher = {Zenodo},
  doi = {10.5281/zenodo.19259984}
}

@article{tilscher26jar,
  author  = {Sarah Tilscher and Alexandra Gra{\ss} and Helmut Seidl and Yannick Stade},
  title   = {Proving Total Correctness of Top-Down Solvers with Widening and Narrowing},
  journal = {Journal of Automated Reasoning},
  volume  = {70},
  number  = {2},
  note    = {Article 15},
  year    = {2026},
  doi     = {10.1007/s10817-026-09756-x}
}

@inproceedings{vanhorn10,
  author    = {David Van Horn and Matthew Might},
  title     = {Abstracting Abstract Machines},
  booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP})},
  pages     = {51--62},
  publisher = {ACM},
  year      = {2010},
  doi       = {10.1145/1863543.1863553}
}

@misc{voblint,
  author    = {Manuel Lerchner},
  title     = {{Voblint}: A Verified {Goblint}-Style Static Analysis Pipeline in {Isabelle/HOL}},
  year      = {2026},
  publisher = {Zenodo},
  doi       = {10.5281/zenodo.23260696}
}

@inproceedings{vojdani16,
  author    = {Vesal Vojdani and Kalmer Apinis and Vootele Rõtov and Helmut Seidl and Varmo Vene and Ralf Vogler},
  title     = {Static Race Detection for Device Drivers: The {Goblint} Approach},
  booktitle = {Proceedings of the 31st {IEEE/ACM} International Conference on Automated Software Engineering ({ASE})},
  pages     = {391--402},
  publisher = {ACM},
  year      = {2016},
  doi       = {10.1145/2970276.2970337}
}

@article{wasserrab09afp,
  author = {Daniel Wasserrab},
  title = {Backing up Slicing: Verifying the Interprocedural Two-Phase {Horwitz-Reps-Binkley} Slicer},
  journal = {Archive of Formal Proofs},
  year = {2009},
  month = nov,
  url = {https://isa-afp.org/entries/HRB-Slicing.html},
  urldate = {2026-09-22}
}