Christoph Sprenger

Journals

1. VLDB 2025

   VerIso: Verifiable Isolation Guarantees for Database Transactions

   Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Si Liu, Luca Multazzua, and David Basin

   Proc. VLDB Endow., 2025

   To appear.

   arXiv Bib HTML

   @article{GhasemiradLiuSprenger+-VLDB25,
     author = {Ghasemirad, Shabnam and Liu, Si and Sprenger, Christoph and Liu, Si and Multazzua, Luca and Basin, David},
     journal = {Proc. {VLDB} Endow.},
     keywords = {distributed database systems, transaction processing, consistency models},
     title = {{VerIso}: Verifiable Isolation Guarantees for Database Transactions },
     url = {https://doi.org/10.14778/3718057.3718065},
     volume = {18},
     year = {2025},
     note = {{To} appear.}
   }

2. JCS

   IsaNet: A framework for verifying secure data plane protocols

   Tobias Klenze, Christoph Sprenger, and David A. Basin

   J. Comput. Secur., 2023

   Bib HTML PDF Code

   @article{DBLP:journals/jcs/KlenzeSB23,
     author = {Klenze, Tobias and Sprenger, Christoph and Basin, David A.},
     doi = {10.3233/JCS-220021},
     journal = {J. Comput. Secur.},
     number = {3},
     pages = {217--259},
     title = {IsaNet: {A} framework for verifying secure data plane protocols},
     url = {https://doi.org/10.3233/JCS-220021},
     volume = {31},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.3233/JCS-220021}
   }

3. OOPSLA

   Igloo: soundly linking compositional refinement and separation logic for distributed system verification

   Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David A. Basin

   Proc. ACM Program. Lang., 2020

   arXiv Bib HTML PDF

   @article{DBLP:journals/pacmpl/0001KEW0CB20,
     author = {Sprenger, Christoph and Klenze, Tobias and Eilers, Marco and Wolf, Felix A. and M{\"{u}}ller, Peter and Clochard, Martin and Basin, David A.},
     doi = {10.1145/3428220},
     journal = {Proc. {ACM} Program. Lang.},
     number = {{OOPSLA}},
     pages = {152:1--152:31},
     title = {Igloo: soundly linking compositional refinement and separation logic for distributed system verification},
     url = {https://doi.org/10.1145/3428220},
     volume = {4},
     year = {2020},
     bdsk-url-1 = {https://doi.org/10.1145/3428220}
   }

4. JCS

   Refining security protocols

   Christoph Sprenger, and David A. Basin

   J. Comput. Secur., 2018

   Bib HTML PDF Code

   @article{DBLP:journals/jcs/SprengerB18,
     author = {Sprenger, Christoph and Basin, David A.},
     doi = {10.3233/JCS-16814},
     journal = {J. Comput. Secur.},
     number = {1},
     pages = {71--120},
     title = {Refining security protocols},
     url = {https://doi.org/10.3233/JCS-16814},
     volume = {26},
     year = {2018},
     bdsk-url-1 = {https://doi.org/10.3233/JCS-16814}
   }

Conferences

1. TACAS 2025

   Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions

   Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, and David Basin

   In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2025, 2025

   To appear.

   arXiv Bib

   @inproceedings{GhasemiradSprengerLiu+-TACAS25,
     author = {Ghasemirad, Shabnam and Sprenger, Christoph and Liu, Si and Multazzu, Luca and Basin, David},
     title = {Pushing the Limit: Verified Performance-Optimal Causally-Consistent
                       Database Transactions},
     booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                       - 31st International Conference, {TACAS} 2025, Held as Part of the
                       European Joint Conferences on Theory and Practice of Software, {ETAPS}
                       2025},
     series = {Lecture Notes in Computer Science},
     publisher = {Springer},
     year = {2025},
     note = {{To} appear.}
   }

2. S&P 2023

   Sound Verification of Security Protocols: From Design to Interoperable Implementations

   Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, and Peter Müller

   In 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, May 21-25, 2023, 2023

   arXiv Bib HTML PDF

   @inproceedings{DBLP:conf/sp/ArquintWLSSWBM23,
     author = {Arquint, Linard and Wolf, Felix A. and Lallemand, Joseph and Sasse, Ralf and Sprenger, Christoph and Wiesner, Sven N. and Basin, David A. and M{\"{u}}ller, Peter},
     booktitle = {44th {IEEE} Symposium on Security and Privacy, {SP} 2023, San Francisco, CA, USA, May 21-25, 2023},
     doi = {10.1109/SP46215.2023.10179325},
     pages = {1077--1093},
     publisher = {{IEEE}},
     title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations},
     url = {https://doi.org/10.1109/SP46215.2023.10179325},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.1109/SP46215.2023.10179325}
   }

3. FoSSaCS 2003

   On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the \(\mathrmμ\)-Calculus

   Christoph Sprenger, and Mads Dam

   In Foundations of Software Science and Computational Structures, (FoSSaCS 2003), 2003

   Bib HTML PDF

   @inproceedings{DBLP:conf/fossacs/SprengerD03,
     author = {Sprenger, Christoph and Dam, Mads},
     booktitle = {Foundations of Software Science and Computational Structures, ({FoSSaCS} 2003)},
     doi = {10.1007/3-540-36576-1\_27},
     editor = {Gordon, Andrew D.},
     pages = {425--440},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     title = {On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the {\(\mathrm{\mu}\)}-Calculus},
     url = {https://doi.org/10.1007/3-540-36576-1\_27},
     volume = {2620},
     year = {2003},
     bdsk-url-1 = {https://doi.org/10.1007/3-540-36576-1%5C_27}
   }