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

• 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

• CIVL: a refinement-based verifier for concurrent programs built on top of Boogie
  I am the main maintainer 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.