Christoph Matheja

Proc. ACM Program. Lang., October, 2023

A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation.

[BibT_eX]

[DOI]

Dataset, July, 2023

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Jens Pagel

Florian Zuleger

ACM Trans. Comput. Log., January, 2023

A Calculus for Amortized Expected Runtimes.

[BibT_eX]

[DOI]

Lena Verscht

Proc. ACM Program. Lang., January, 2023

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.

[BibT_eX]

[DOI]

Mingshuai Chen

Sebastian Junges

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022

Foundations for Entailment Checking in Quantitative Separation Logic (extended version).

[BibT_eX]

[DOI]

CoRR, 2022

The Prusti Project: Formal Verification for Rust.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

Foundations for Entailment Checking in Quantitative Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2022

2021

Modular specification and verification of closures in Rust.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

A pre-expectation calculus for probabilistic sensitivity.

[BibT_eX]

[DOI]

Alejandro Aguirre

Gilles Barthe

Justin Hsu

Proc. ACM Program. Lang., 2021

Flexible Refinement Proofs in Separation Logic.

[BibT_eX]

[DOI]

Aurel Bílý

Peter Müller

CoRR, 2021

Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars.

[BibT_eX]

[DOI]

Proceedings of the Graph Transformation - 14th International Conference, 2021

Latticed k-Induction with an Application to Probabilistic Programs.

[BibT_eX]

[DOI]

Mingshuai Chen

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Automated reasoning and randomization in separation logic.

[BibT_eX]

[DOI]

PhD thesis, 2020

How do programmers use unsafe rust?

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Relatively Complete Verification of Probabilistic Programs.

[BibT_eX]

[DOI]

CoRR, 2020

Complete Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Jens Pagel

Florian Zuleger

CoRR, 2020

PrIC3: Property Directed Reachability for MDPs.

[BibT_eX]

[DOI]

Sebastian Junges

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.

[BibT_eX]

[DOI]

Thomas Noll

Proc. ACM Program. Lang., 2019

Kantorovich Continuity of Probabilistic Programs.

[BibT_eX]

[DOI]

Alejandro Aguirre

Gilles Barthe

Justin Hsu

CoRR, 2019

On the hardness of analyzing probabilistic programs.

[BibT_eX]

[DOI]

Acta Informatica, 2019

SL-COMP: Competition of Solvers for Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Effective Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Jens Katelaan

Florian Zuleger

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018

Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.

[BibT_eX]

[DOI]

Federico Olmedo

J. ACM, 2018

Quantitative Separation Logic.

[BibT_eX]

[DOI]

Thomas Noll

CoRR, 2018

Rule-Based Conditioning of Probabilistic Data.

[BibT_eX]

[DOI]

Maurice van Keulen

Proceedings of the Scalable Uncertainty Management - 12th International Conference, 2018

Graph-Based Shape Analysis Beyond Context-Freeness.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Heap Abstraction Beyond Context-Freeness.

[BibT_eX]

[DOI]

CoRR, 2017

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

2016

Inferring Covariances for Probabilistic Programs.

[BibT_eX]

[DOI]

Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016

Reasoning about Recursive Probabilistic Programs.

[BibT_eX]

[DOI]

Federico Olmedo

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs.

[BibT_eX]

[DOI]

Federico Olmedo

Proceedings of the Programming Languages and Systems, 2016

2015

Tree-Like Grammars and Separation Logic.

[BibT_eX]

[DOI]