publications

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. AFP

   The Sumcheck Protocol

   Azucena Garvı́a Bosshard, Christoph Sprenger, and Jonathan Bootle

   Arch. Formal Proofs, 2024

   Bib HTML

   @article{DBLP:journals/afp/BosshardSB24,
     author = {Garv{\'{\i}}a Bosshard, Azucena and Sprenger, Christoph and Bootle, Jonathan},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/afp/BosshardSB24.bib},
     date-added = {2024-03-11 12:46:27 +0100},
     date-modified = {2024-06-14 18:00:34 +0200},
     journal = {Arch. Formal Proofs},
     timestamp = {Tue, 20 Feb 2024 15:24:42 +0100},
     title = {The Sumcheck Protocol},
     volume = {2024},
     year = {2024},
   }

3. 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}
   }

4. AFP

   IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols

   Tobias Klenze, and Christoph Sprenger

   Arch. Formal Proofs, 2022

   Bib HTML

   @article{DBLP:journals/afp/Klenze022,
     author = {Klenze, Tobias and Sprenger, Christoph},
     journal = {Arch. Formal Proofs},
     title = {IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols},
     year = {2022},
   }

5. 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}
   }

6. 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}
   }

7. JCS

   Abstractions for security protocol verification

   Thanh Binh Nguyen, Christoph Sprenger, and Cas Cremers

   J. Comput. Secur., 2018

   Bib HTML PDF

   @article{DBLP:journals/jcs/NguyenSC18,
     author = {Nguyen, Thanh Binh and Sprenger, Christoph and Cremers, Cas},
     doi = {10.3233/JCS-15769},
     journal = {J. Comput. Secur.},
     number = {4},
     pages = {459--508},
     title = {Abstractions for security protocol verification},
     url = {https://doi.org/10.3233/JCS-15769},
     volume = {26},
     year = {2018},
     bdsk-url-1 = {https://doi.org/10.3233/JCS-15769}
   }

8. AFP

   Refining Authenticated Key Agreement with Strong Adversaries

   Joseph Lallemand, and Christoph Sprenger

   Arch. Formal Proofs, 2017

   Bib HTML

   @article{DBLP:journals/afp/LallemandS17,
     author = {Lallemand, Joseph and Sprenger, Christoph},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     journal = {Arch. Formal Proofs},
     title = {Refining Authenticated Key Agreement with Strong Adversaries},
     year = {2017},
   }

9. AFP

   Developing Security Protocols by Refinement

   Christoph Sprenger, and Ivano Somaini

   Arch. Formal Proofs, 2017

   Bib HTML

   @article{DBLP:journals/afp/SprengerS17,
     author = {Sprenger, Christoph and Somaini, Ivano},
     journal = {Arch. Formal Proofs},
     title = {Developing Security Protocols by Refinement},
     year = {2017},
   }

10. AFP

    Consensus Refined

    Ognjen Maric, and Christoph Sprenger

    Arch. Formal Proofs, 2015

    Bib HTML

    @article{DBLP:journals/afp/MaricS15,
      author = {Maric, Ognjen and Sprenger, Christoph},
      journal = {Arch. Formal Proofs},
      title = {Consensus Refined},
      volume = {2015},
      year = {2015},
    }

11. Inf. Comput.

    Compositional verification of sequential programs with procedures

    Dilian Gurov, Marieke Huisman, and Christoph Sprenger

    Inf. Comput., 2008

    Bib HTML PDF

    @article{DBLP:journals/iandc/GurovHS08,
      author = {Gurov, Dilian and Huisman, Marieke and Sprenger, Christoph},
      doi = {10.1016/j.ic.2008.03.003},
      journal = {Inf. Comput.},
      number = {7},
      pages = {840--868},
      title = {Compositional verification of sequential programs with procedures},
      url = {https://doi.org/10.1016/j.ic.2008.03.003},
      volume = {206},
      year = {2008},
      bdsk-url-1 = {https://doi.org/10.1016/j.ic.2008.03.003}
    }

12. On global induction mechanisms in a \(\mathrmμ\)-calculus with explicit approximations

    Christoph Sprenger, and Mads Dam

    RAIRO Theor. Informatics Appl., 2003

    Bib HTML PDF

    @article{DBLP:journals/ita/SprengerD03,
      author = {Sprenger, Christoph and Dam, Mads},
      doi = {10.1051/ita:2003024},
      journal = {{RAIRO} Theor. Informatics Appl.},
      number = {4},
      pages = {365--391},
      title = {On global induction mechanisms in a {\(\mathrm{\mu}\)}-calculus with explicit approximations},
      url = {https://doi.org/10.1051/ita:2003024},
      volume = {37},
      year = {2003},
      bdsk-url-1 = {https://doi.org/10.1051/ita:2003024}
    }

13. SCIDDLE: A tool for large scale distributed computing

    Peter Arbenz, Christoph Sprenger, Hans Peter Lüthi, and Stefan Vogel

    Concurr. Pract. Exp., 1995

    Bib HTML

    @article{DBLP:journals/concurrency/ArbenzSLV95,
      author = {Arbenz, Peter and Sprenger, Christoph and L{\"{u}}thi, Hans Peter and Vogel, Stefan},
      doi = {10.1002/cpe.4330070203},
      journal = {Concurr. Pract. Exp.},
      number = {2},
      pages = {121--146},
      title = {{SCIDDLE:} {A} tool for large scale distributed computing},
      url = {https://doi.org/10.1002/cpe.4330070203},
      volume = {7},
      year = {1995},
      bdsk-url-1 = {https://doi.org/10.1002/cpe.4330070203}
    }

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. CSF 2024

   Formal Verification of the Sumcheck Protocol

   Azucena Garvı́a Bosshard, Jonathan Bootle, and Christoph Sprenger

   In 37th IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, Netherlands, July 8-12, 2024, 2024

   arXiv Bib HTML PDF

   @inproceedings{DBLP:conf/csfw/BosshardBS24,
     author = {Bosshard, Azucena Garv{\'{\i}}a and Bootle, Jonathan and Sprenger, Christoph},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/csfw/BosshardBS24.bib},
     booktitle = {37th {IEEE} Computer Security Foundations Symposium, {CSF} 2024, Enschede, Netherlands, July 8-12, 2024},
     date-added = {2025-03-14 19:52:45 +0100},
     date-modified = {2025-03-14 19:52:45 +0100},
     doi = {10.1109/CSF61375.2024.00014},
     keywords = {interactive proofs},
     pages = {605--619},
     publisher = {{IEEE}},
     timestamp = {Sun, 06 Oct 2024 20:59:00 +0200},
     title = {Formal Verification of the Sumcheck Protocol},
     url = {https://doi.org/10.1109/CSF61375.2024.00014},
     year = {2024},
     bdsk-url-1 = {https://doi.org/10.1109/CSF61375.2024.00014}
   }

3. 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}
   }

4. CSF 2022

   N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures

   Thilo Weghorn, Si Liu, Christoph Sprenger, Adrian Perrig, and David A. Basin

   In 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022, 2022

   Bib HTML PDF

   @inproceedings{DBLP:conf/csfw/WeghornLSPB22,
     author = {Weghorn, Thilo and Liu, Si and Sprenger, Christoph and Perrig, Adrian and Basin, David A.},
     biburl = {https://dblp.org/rec/conf/csfw/WeghornLSPB22.bib},
     booktitle = {35th {IEEE} Computer Security Foundations Symposium, {CSF} 2022, Haifa, Israel, August 7-10, 2022},
     doi = {10.1109/CSF54842.2022.9919646},
     pages = {147--162},
     publisher = {{IEEE}},
     title = {N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures},
     url = {https://doi.org/10.1109/CSF54842.2022.9919646},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.1109/CSF54842.2022.9919646}
   }

5. CSF 2021

   Formal Verification of Secure Forwarding Protocols

   Tobias Klenze, Christoph Sprenger, and David A. Basin

   In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, 2021

   Bib HTML PDF

   @inproceedings{DBLP:conf/csfw/Klenze0B21,
     author = {Klenze, Tobias and Sprenger, Christoph and Basin, David A.},
     booktitle = {34th {IEEE} Computer Security Foundations Symposium, {CSF} 2021, Dubrovnik, Croatia, June 21-25, 2021},
     date-added = {2024-05-29 09:06:05 +0200},
     date-modified = {2024-05-29 09:06:05 +0200},
     doi = {10.1109/CSF51468.2021.00018},
     pages = {1--16},
     publisher = {{IEEE}},
     title = {Formal Verification of Secure Forwarding Protocols},
     url = {https://doi.org/10.1109/CSF51468.2021.00018},
     year = {2021},
     bdsk-url-1 = {https://doi.org/10.1109/CSF51468.2021.00018}
   }

6. EuroS&P 2020

   SoK: Delegation and Revocation, the Missing Links in the Web’s Chain of Trust

   Laurent Chuat, AbdelRahman Abdou, Ralf Sasse, Christoph Sprenger, David A. Basin, and Adrian Perrig

   In IEEE European Symposium on Security and Privacy, EuroS&P 2020, Genoa, Italy, September 7-11, 2020, 2020

   arXiv Bib HTML PDF

   @inproceedings{DBLP:conf/eurosp/ChuatAS0BP20,
     author = {Chuat, Laurent and Abdou, AbdelRahman and Sasse, Ralf and Sprenger, Christoph and Basin, David A. and Perrig, Adrian},
     booktitle = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2020, Genoa, Italy, September 7-11, 2020},
     doi = {10.1109/EuroSP48549.2020.00046},
     pages = {624--638},
     publisher = {{IEEE}},
     title = {SoK: Delegation and Revocation, the Missing Links in the Web's Chain of Trust},
     url = {https://doi.org/10.1109/EuroSP48549.2020.00046},
     year = {2020},
     bdsk-url-1 = {https://doi.org/10.1109/EuroSP48549.2020.00046}
   }

7. USENIX Sec. 2020

   EPIC: Every Packet Is Checked in the Data Plane of a Path-Aware Internet

   Markus Legner, Tobias Klenze, Marc Wyss, Christoph Sprenger, and Adrian Perrig

   In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, 2020

   Bib HTML

   @inproceedings{DBLP:conf/uss/LegnerKW0P20,
     author = {Legner, Markus and Klenze, Tobias and Wyss, Marc and Sprenger, Christoph and Perrig, Adrian},
     booktitle = {29th {USENIX} Security Symposium, {USENIX} Security 2020, August 12-14, 2020},
     editor = {Capkun, Srdjan and Roesner, Franziska},
     pages = {541--558},
     publisher = {{USENIX} Association},
     title = {{EPIC:} Every Packet Is Checked in the Data Plane of a Path-Aware Internet},
     url = {https://www.usenix.org/conference/usenixsecurity20/presentation/legner},
     year = {2020},
     bdsk-url-1 = {https://www.usenix.org/conference/usenixsecurity20/presentation/legner}
   }

8. CAV 2017

   Cutoff Bounds for Consensus Algorithms

   Ognjen Maric, Christoph Sprenger, and David A. Basin

   In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, 2017

   Bib HTML PDF

   @inproceedings{DBLP:conf/cav/MaricSB17,
     author = {Maric, Ognjen and Sprenger, Christoph and Basin, David A.},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
     doi = {10.1007/978-3-319-63390-9\_12},
     editor = {Majumdar, Rupak and Kuncak, Viktor},
     pages = {217--237},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     title = {Cutoff Bounds for Consensus Algorithms},
     url = {https://doi.org/10.1007/978-3-319-63390-9\_12},
     volume = {10427},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-63390-9%5C_12}
   }

9. EuroS&P 2017

   Refining Authenticated Key Agreement with Strong Adversaries

   Joseph Lallemand, David A. Basin, and Christoph Sprenger

   In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26-28, 2017, 2017

   Bib HTML PDF Code

   @inproceedings{DBLP:conf/eurosp/LallemandBS17,
     author = {Lallemand, Joseph and Basin, David A. and Sprenger, Christoph},
     booktitle = {2017 {IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2017, Paris, France, April 26-28, 2017},
     doi = {10.1109/EuroSP.2017.22},
     pages = {92--107},
     publisher = {{IEEE}},
     title = {Refining Authenticated Key Agreement with Strong Adversaries},
     url = {https://doi.org/10.1109/EuroSP.2017.22},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1109/EuroSP.2017.22}
   }

10. DSN 2015

    Consensus Refined

    Ognjen Maric, Christoph Sprenger, and David A. Basin

    In 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2015, Rio de Janeiro, Brazil, June 22-25, 2015, 2015

    Bib HTML PDF Code

    @inproceedings{DBLP:conf/dsn/MaricSB15,
      author = {Maric, Ognjen and Sprenger, Christoph and Basin, David A.},
      booktitle = {45th Annual {IEEE/IFIP} International Conference on Dependable Systems and Networks, {DSN} 2015, Rio de Janeiro, Brazil, June 22-25, 2015},
      doi = {10.1109/DSN.2015.38},
      pages = {391--402},
      publisher = {{IEEE} Computer Society},
      title = {Consensus Refined},
      url = {https://doi.org/10.1109/DSN.2015.38},
      year = {2015},
      bdsk-url-1 = {https://doi.org/10.1109/DSN.2015.38}
    }

11. POST 2015

    Abstractions for Security Protocol Verification

    Thanh Binh Nguyen, and Christoph Sprenger

    In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, 2015

    Bib HTML PDF

    @inproceedings{DBLP:conf/post/0003S15,
      author = {Nguyen, Thanh Binh and Sprenger, Christoph},
      booktitle = {Principles of Security and Trust - 4th International Conference, {POST} 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015, Proceedings},
      doi = {10.1007/978-3-662-46666-7\_11},
      editor = {Focardi, Riccardo and Myers, Andrew C.},
      pages = {196--215},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Abstractions for Security Protocol Verification},
      url = {https://doi.org/10.1007/978-3-662-46666-7\_11},
      volume = {9036},
      year = {2015},
      bdsk-url-1 = {https://doi.org/10.1007/978-3-662-46666-7%5C_11}
    }

12. FM 2014

    Verification of a Transactional Memory Manager under Hardware Failures and Restarts

    Ognjen Maric, and Christoph Sprenger

    In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014

    Bib HTML PDF

    @inproceedings{DBLP:conf/fm/MaricS14,
      author = {Maric, Ognjen and Sprenger, Christoph},
      booktitle = {{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings},
      doi = {10.1007/978-3-319-06410-9\_31},
      editor = {Jones, Cliff B. and Pihlajasaari, Pekka and Sun, Jun},
      pages = {449--464},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Verification of a Transactional Memory Manager under Hardware Failures and Restarts},
      url = {https://doi.org/10.1007/978-3-319-06410-9\_31},
      volume = {8442},
      year = {2014},
      bdsk-url-1 = {https://doi.org/10.1007/978-3-319-06410-9%5C_31}
    }

13. POST 2013

    Sound Security Protocol Transformations

    Thanh Binh Nguyen, and Christoph Sprenger

    In Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, 2013

    Bib HTML PDF

    @inproceedings{DBLP:conf/post/NguyenS13,
      author = {Nguyen, Thanh Binh and Sprenger, Christoph},
      booktitle = {Principles of Security and Trust - Second International Conference, {POST} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
      doi = {10.1007/978-3-642-36830-1\_5},
      editor = {Basin, David A. and Mitchell, John C.},
      pages = {83--104},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Sound Security Protocol Transformations},
      url = {https://doi.org/10.1007/978-3-642-36830-1\_5},
      volume = {7796},
      year = {2013},
      bdsk-url-1 = {https://doi.org/10.1007/978-3-642-36830-1%5C_5}
    }

14. CSF 2012

    Refining Key Establishment

    Christoph Sprenger, and David A. Basin

    In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, 2012

    Bib HTML PDF

    @inproceedings{DBLP:conf/csfw/SprengerB12,
      author = {Sprenger, Christoph and Basin, David A.},
      booktitle = {25th {IEEE} Computer Security Foundations Symposium, {CSF} 2012, Cambridge, MA, USA, June 25-27, 2012},
      doi = {10.1109/CSF.2012.21},
      editor = {Chong, Stephen},
      pages = {230--246},
      publisher = {{IEEE} Computer Society},
      title = {Refining Key Establishment},
      url = {https://doi.org/10.1109/CSF.2012.21},
      year = {2012},
      bdsk-url-1 = {https://doi.org/10.1109/CSF.2012.21}
    }

15. CCS 2010

    Developing security protocols by refinement

    Christoph Sprenger, and David A. Basin

    In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010, 2010

    Bib HTML PDF

    @inproceedings{DBLP:conf/ccs/SprengerB10,
      author = {Sprenger, Christoph and Basin, David A.},
      booktitle = {Proceedings of the 17th {ACM} Conference on Computer and Communications Security, {CCS} 2010, Chicago, Illinois, USA, October 4-8, 2010},
      doi = {10.1145/1866307.1866349},
      editor = {Al{-}Shaer, Ehab and Keromytis, Angelos D. and Shmatikov, Vitaly},
      pages = {361--374},
      publisher = {{ACM}},
      title = {Developing security protocols by refinement},
      url = {https://doi.org/10.1145/1866307.1866349},
      year = {2010},
      bdsk-url-1 = {https://doi.org/10.1145/1866307.1866349}
    }

16. CSF 2008

    Cryptographically-Sound Protocol-Model Abstractions

    Christoph Sprenger, and David A. Basin

    In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008, 2008

    Bib HTML PDF

    @inproceedings{DBLP:conf/csfw/SprengerB08,
      author = {Sprenger, Christoph and Basin, David A.},
      biburl = {https://dblp.org/rec/conf/csfw/SprengerB08.bib},
      booktitle = {Proceedings of the 21st {IEEE} Computer Security Foundations Symposium, {CSF} 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008},
      doi = {10.1109/CSF.2008.19},
      pages = {115--129},
      publisher = {{IEEE} Computer Society},
      title = {Cryptographically-Sound Protocol-Model Abstractions},
      url = {https://doi.org/10.1109/CSF.2008.19},
      year = {2008},
      bdsk-url-1 = {https://doi.org/10.1109/CSF.2008.19}
    }

17. TPHOLs 2007

    A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols

    Christoph Sprenger, and David A. Basin

    In Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, 2007

    Bib HTML PDF

    @inproceedings{DBLP:conf/tphol/SprengerB07,
      author = {Sprenger, Christoph and Basin, David A.},
      booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
      doi = {10.1007/978-3-540-74591-4\_23},
      editor = {Schneider, Klaus and Brandt, Jens},
      pages = {302--318},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols},
      url = {https://doi.org/10.1007/978-3-540-74591-4\_23},
      volume = {4732},
      year = {2007},
      bdsk-url-1 = {https://doi.org/10.1007/978-3-540-74591-4%5C_23}
    }

18. CSFW 2006

    Cryptographically Sound Theorem Proving

    Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, and Michael Waidner

    In 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy, 2006

    Bib HTML PDF

    @inproceedings{DBLP:conf/csfw/SprengerBBPW06,
      author = {Sprenger, Christoph and Backes, Michael and Basin, David A. and Pfitzmann, Birgit and Waidner, Michael},
      booktitle = {19th {IEEE} Computer Security Foundations Workshop, {(CSFW-19} 2006), 5-7 July 2006, Venice, Italy},
      doi = {10.1109/CSFW.2006.10},
      pages = {153--166},
      publisher = {{IEEE} Computer Society},
      title = {Cryptographically Sound Theorem Proving},
      url = {https://doi.org/10.1109/CSFW.2006.10},
      year = {2006},
      bdsk-url-1 = {https://doi.org/10.1109/CSFW.2006.10}
    }

19. FASE 2004

    Checking Absence of Illicit Applet Interactions: A Case Study

    Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov

    In Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings, 2004

    Bib HTML PDF

    @inproceedings{DBLP:conf/fase/HuismanGSC04,
      author = {Huisman, Marieke and Gurov, Dilian and Sprenger, Christoph and Chugunov, Gennady},
      booktitle = {Fundamental Approaches to Software Engineering, 7th International Conference, {FASE} 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings},
      doi = {10.1007/978-3-540-24721-0\_6},
      editor = {Wermelinger, Michel and Margaria, Tiziana},
      pages = {84--98},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Checking Absence of Illicit Applet Interactions: {A} Case Study},
      url = {https://doi.org/10.1007/978-3-540-24721-0\_6},
      volume = {2984},
      year = {2004},
      bdsk-url-1 = {https://doi.org/10.1007/978-3-540-24721-0%5C_6}
    }

20. MEMOCODE 2004

    Compositional verification for secure loading of smart card applets

    Christoph Sprenger, Dilian Gurov, and Marieke Huisman

    In 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 23-25 June 2004, San Diego, California, USA, Proceedings, 2004

    Bib HTML PDF

      author = {Sprenger, Christoph and Gurov, Dilian and Huisman, Marieke},
      booktitle = {2nd {ACM} {\&} {IEEE} International Conference on Formal Methods and Models for Co-Design {(MEMOCODE} 2004), 23-25 June 2004, San Diego, California, USA, Proceedings},
      doi = {10.1109/MEMCOD.2004.1459857},
      pages = {211--222},
      publisher = {{IEEE} Computer Society},
      title = {Compositional verification for secure loading of smart card applets},
      url = {https://doi.org/10.1109/MEMCOD.2004.1459857},
      year = {2004},
      bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2004.1459857}
    }

21. 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}
    }

22. MEMOCODE 2003

    A Verification Methodology for Infinite-State Message Passing Systems

    Christoph Sprenger, and Krzysztof Worytkiewicz

    In 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings, 2003

    Bib HTML PDF

      author = {Sprenger, Christoph and Worytkiewicz, Krzysztof},
      booktitle = {1st {ACM} {\&} {IEEE} International Conference on Formal Methods and Models for Co-Design {(MEMOCODE} 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings},
      doi = {10.1109/MEMCOD.2003.1210110},
      pages = {255--264},
      publisher = {{IEEE} Computer Society},
      title = {A Verification Methodology for Infinite-State Message Passing Systems},
      url = {https://doi.org/10.1109/MEMCOD.2003.1210110},
      year = {2003},
      bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2003.1210110}
    }

23. FICS 2002

    A note on global induction in a mu-calculus with explicit approximations

    Christoph Sprenger, and Mads Dam

    In Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings, 2002

    Bib PDF

    @inproceedings{DBLP:conf/fics/SprengerD02,
      author = {Sprenger, Christoph and Dam, Mads},
      booktitle = {Fixed Points in Computer Science, {FICS} 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings},
      editor = {{\'{E}}sik, Zolt{\'{a}}n and Ing{\'{o}}lfsd{\'{o}}ttir, Anna},
      pages = {22--24},
      publisher = {University of Aarhus},
      series = {{BRICS} Notes Series},
      title = {A note on global induction in a mu-calculus with explicit approximations},
      volume = {{NS-02-2}},
      year = {2002}
    }

24. TACAS 1998

    A Verified Model Checker for the Modal \(\mathrmμ\)-calculus in Coq

    Christoph Sprenger

    In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, 1998

    Bib HTML PDF

    @inproceedings{DBLP:conf/tacas/Sprenger98,
      author = {Sprenger, Christoph},
      booktitle = {Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, {TACAS} '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings},
      doi = {10.1007/BFb0054171},
      editor = {Steffen, Bernhard},
      pages = {167--183},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {A Verified Model Checker for the Modal {\(\mathrm{\mu}\)}-calculus in Coq},
      url = {https://doi.org/10.1007/BFb0054171},
      volume = {1384},
      year = {1998},
      bdsk-url-1 = {https://doi.org/10.1007/BFb0054171}
    }

25. SCIDDLE: A Tool for Large Scale Cooperative Computing

    Peter Arbenz, Hans Peter Lüthi, Christoph Sprenger, and Stefan Vogel

    In High-Performance Computing and Networking, International Conference and Exhibition, HPCN Europe 1994, Munich, Germany, April 18-20, 1994, Proceedings, Volume II: Networking and Tools, 1994

    Bib HTML

    @inproceedings{DBLP:conf/hpcn/ArbenzLSV94,
      author = {Arbenz, Peter and L{\"{u}}thi, Hans Peter and Sprenger, Christoph and Vogel, Stefan},
      booktitle = {High-Performance Computing and Networking, International Conference and Exhibition, {HPCN} Europe 1994, Munich, Germany, April 18-20, 1994, Proceedings, Volume {II:} Networking and Tools},
      doi = {10.1007/3-540-57981-8\_138},
      editor = {Gentzsch, Wolfgang and Harms, Uwe},
      pages = {326--327},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {{SCIDDLE:} {A} Tool for Large Scale Cooperative Computing},
      url = {https://doi.org/10.1007/3-540-57981-8\_138},
      volume = {797},
      year = {1994},
      bdsk-url-1 = {https://doi.org/10.1007/3-540-57981-8%5C_138}
    }

Technical Reports

1. VerIso: Verifiable Isolation Guarantees for Database Transactions

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

   2025

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-2503-06284,
     archiveprefix = {arXiv},
     author = {Ghasemirad, Shabnam and Liu, Si and Sprenger, Christoph and Multazzu, Luca and Basin, David},
     doi = {10.48550/arXiv.2503.06284},
     eprint = {2503.06284},
     eprinttype = {arXiv},
     journal = {CoRR},
     primaryclass = {cs.DB},
     title = {{VerIso}: Verifiable Isolation Guarantees for Database Transactions},
     volume = {abs/2503.06284},
     year = {2025}
   }

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

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

   2024

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-2411-07049,
     archiveprefix = {arXiv},
     author = {Ghasemirad, Shabnam and Sprenger, Christoph and Liu, Si and Multazzu, Luca and Basin, David},
     doi = {10.48550/ARXIV.2411.07049},
     eprint = {2411.07049},
     eprinttype = {arXiv},
     journal = {CoRR},
     primaryclass = {cs.DB},
     title = {Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions},
     volume = {abs/2411.07049},
     year = {2024},
     bdsk-url-2 = {https://doi.org/10.48550/ARXIV.2411.07049}
   }

3. Formal Verification of the Sumcheck Protocol

   Azucena Garvı́a Bosshard, Jonathan Bootle, and Christoph Sprenger

   2024

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-2402-06093,
     author = {Bosshard, Azucena Garv{\'{\i}}a and Bootle, Jonathan and Sprenger, Christoph},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/corr/abs-2402-06093.bib},
     date-added = {2024-03-11 12:47:49 +0100},
     date-modified = {2024-03-11 12:47:49 +0100},
     doi = {10.48550/ARXIV.2402.06093},
     eprint = {2402.06093},
     eprinttype = {arXiv},
     journal = {CoRR},
     timestamp = {Fri, 16 Feb 2024 13:00:19 +0100},
     title = {Formal Verification of the Sumcheck Protocol},
     url = {https://doi.org/10.48550/arXiv.2402.06093},
     volume = {abs/2402.06093},
     year = {2024},
     bdsk-url-1 = {https://doi.org/10.48550/arXiv.2402.06093}
   }

4. Protocols to Code: Formal Verification of a Next-Generation Internet Router

   João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, and Adrian Perrig

   2024

   arXiv Bib

   @techreport{arXiv.2405.06074,
     author = {Pereira, João C. and Klenze, Tobias and Giampietro, Sofia and Limbeck, Markus and Spiliopoulos, Dionysios and Wolf, Felix A. and Eilers, Marco and Sprenger, Christoph and Basin, David and Müller, Peter and Perrig, Adrian},
     doi = {10.48550/arXiv.2405.06074},
     eprint = {2405.06074},
     eprinttype = {arXiv},
     journal = {CoRR},
     title = {Protocols to Code: Formal Verification of a Next-Generation Internet Router},
     url = {https://doi.org/10.48550/arXiv.2405.06074},
     volume = {abs/2405.06074},
     year = {2024},
     bdsk-url-1 = {https://doi.org/10.48550/arXiv.2405.06074}
   }

5. Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)

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

   2022

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-2212-04171,
     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},
     doi = {10.48550/arXiv.2212.04171},
     eprint = {2212.04171},
     eprinttype = {arXiv},
     journal = {CoRR},
     title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)},
     url = {https://doi.org/10.48550/arXiv.2212.04171},
     volume = {abs/2212.04171},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.48550/arXiv.2212.04171}
   }

6. 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

   2020

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-2010-04749,
     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.},
     eprint = {2010.04749},
     eprinttype = {arXiv},
     journal = {CoRR},
     title = {Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification},
     volume = {abs/2010.04749},
     year = {2020},
   }

7. Proxy Certificates: The Missing Link in the Web’s Chain of Trust

   Laurent Chuat, AbdelRahman Abdou, Ralf Sasse, Christoph Sprenger, David A. Basin, and Adrian Perrig

   2019

   arXiv Bib

   @techreport{DBLP:journals/corr/abs-1906-10775,
     author = {Chuat, Laurent and Abdou, AbdelRahman and Sasse, Ralf and Sprenger, Christoph and Basin, David A. and Perrig, Adrian},
     eprint = {1906.10775},
     eprinttype = {arXiv},
     journal = {CoRR},
     title = {Proxy Certificates: The Missing Link in the Web's Chain of Trust},
     volume = {abs/1906.10775},
     year = {2019},
   }

8. Cryptographically Sound Theorem Proving

   Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, and Michael Waidner

   2006

   IACR Cryptol. ePrint Arch.

   Bib HTML

   @techreport{DBLP:journals/iacr/SprengerBBPW06,
     author = {Sprenger, Christoph and Backes, Michael and Basin, David A. and Pfitzmann, Birgit and Waidner, Michael},
     journal = {{IACR} Cryptol. ePrint Arch.},
     note = {{IACR} Cryptol. ePrint Arch.},
     pages = {47},
     title = {Cryptographically Sound Theorem Proving},
     url = {http://eprint.iacr.org/2006/047},
     year = {2006},
     bdsk-url-1 = {http://eprint.iacr.org/2006/047}
   }

Theses

1. Deductive Local Model Checking – On the Verification of CTL* Properties of Infinite-State Reactive Systems

   Christoph Sprenger

   EPFL, Lausanne, Switzerland, 2000

   PhD thesis

   Bib PDF

   @phdthesis{Sprenger2000,
     author = {Sprenger, Christoph},
     note = {PhD thesis},
     school = {EPFL, Lausanne, Switzerland},
     title = {Deductive Local Model Checking -- On the Verification of CTL* Properties of Infinite-State Reactive Systems},
     year = {2000}
   }