Bernhard Kragl

I am an applied scientist at Amazon Web Services (AWS). Before joining Amazon, I obtained a PhD in computer science from the Institute of Science and Technology Austria (IST Austria). My advisor was Thomas A. Henzinger. I hold a bachelor and master degree in computer science, both from the Technical University of Vienna.

Contact

Email:

<last_name> b @ <employer> .com

Research Interests

Formal Verification, Programming Languages, Distributed Systems, Logic, Automated Reasoning

Publications

• DBLP
• Google Scholar
• ORCID

• Validating a High-Performance Cloud Object Store with Lightweight Formal Methods
  Vimuth Fernando, Rajeev Joshi, Bernhard Kragl, Julien Mascart, Matthew Russo, Sarek Skotåm, Colin Walker, Jake Wires
  SOSP 2026 (32nd ACM Symposium on Operating Systems Principles)
  [pdf] [doi]
• High Fidelity Models for Large Scale Stateful Services (Operational Systems)
  Nouraldin Jaber, Dongyun Jin, Bernhard Kragl, Enrico Magnago, Gustavo Petri, Thorsten Tarrach, Serdar Tasiran
  OSDI 2026 (20th USENIX Symposium on Operating Systems Design and Implementation)
  [pdf] [website]
• Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
  James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield
  SOSP 2021 (28th ACM Symposium on Operating Systems Principles)
  🏆 Best Paper Award
  [pdf] [doi] [website] [blog]
• The Civl Verifier
  Bernhard Kragl, Shaz Qadeer
  FMCAD 2021 (Formal Methods in Computer-Aided Design)
  [pdf] [doi] [slides] [video]
• Refinement for Structured Concurrent Programs
  Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger
  CAV 2020 (32nd International Conference on Computer Aided Verification)
  [pdf] [doi] [slides] [video]
• Inductive Sequentialization of Asynchronous Programs
  Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer
  PLDI 2020 (41st ACM SIGPLAN Conference on Programming Language Design and Implementation)
  [pdf] [doi] [artifact] [slides] [video]
• Monitoring Event Frequencies
  Thomas Ferrère, Thomas A. Henzinger, Bernhard Kragl
  CSL 2020 (28th EACSL Annual Conference on Computer Science Logic)
  [pdf] [pdf-extended] [doi] [arXiv] [slides]
• Synchronizing the Asynchronous
  Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger
  CONCUR 2018 (29th International Conference on Concurrency Theory)
  [pdf] [doi] [slides]
• Layered Concurrent Programs
  Bernhard Kragl, Shaz Qadeer
  CAV 2018 (30th International Conference on Computer Aided Verification)
  [pdf] [doi] [slides]
• Faster Algorithms for Weighted Recursive State Machines
  Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, Andreas Pavlogiannis
  ESOP 2017 (26th European Symposium on Programming)
  [pdf] [pdf-extended] [doi] [arXiv] [slides]
• Extensional Crisis and Proving Identity
  Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov
  ATVA 2014 (12th International Symposium on Automated Technology for Verification and Analysis)
  [pdf] [doi] [slides]
• Tree Interpolation in Vampire
  Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl
  LPAR 2013 (19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning)
  [pdf] [doi] [slides]

PhD Thesis

• Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization
  🏆 Young Expert Award @ Austrian Computer Science Day 2021
  [pdf] [doi]

Software

• Shuttle: a library for testing concurrent Rust code
  I co-maintain Shuttle and apply it to real-world storage systems.
• Civl: a refinement-based verifier for concurrent programs built on top of Boogie
  I co-maintain Civl and develop new techniques to simplify the verification of distributed systems.
• Vampire: a world-leading first-order theorem prover
  I implemented the extensionality resolution inference rule for efficient reasoning with extensionality axioms, and contributed to the tree interpolation module of Vampire.