Christoph Matheja

Andrey Rivkin

Proceedings of the Joint Proceedings of the Workshops at the 46th International Conference on Application and Theory of Petri Nets and Concurrency: Petri Nets and Software Engineering (PNSE'25), Algorithms & Theories for the Analysis of Event Data (ATAED'25), and Petri Net Games, Examples and Quizzes for Education, Contest and Fun (PeNGE'25) co-located with PETRI NETS 2025, June 23, 2025

2024

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report).

[BibT_eX]

[DOI]

Tobias Winkler

CoRR, 2024

Data Petri Nets meet Probabilistic Programming (Extended version).

[BibT_eX]

[DOI]

CoRR, 2024

A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL.

[BibT_eX]

[DOI]

Proceedings of the Bridging the Gap Between AI and Reality, 2024

LogPPL: A Tool for Probabilistic Process Mining.

[BibT_eX]

[DOI]

Proceedings of the Doctoral Consortium and Demo Track 2024 at the International Conference on Process Mining 2024 co-located with the 6th International Conference on Process Mining (ICPM 2024), 2024

What Should Be Observed for Optimal Reward in POMDPs?

[BibT_eX]

[DOI]

Alyzia-Maria Konsta

Alberto Lluch-Lafuente

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Data Petri Nets Meet Probabilistic Programming.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management - 22nd International Conference, 2024

J-P: MDP. FP. PP - Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs.

[BibT_eX]

[DOI]

Tobias Winkler

Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024

2023

A Deductive Verification Infrastructure for Probabilistic Programs.

[BibT_eX]

[DOI]

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 (artefact).

[BibT_eX]

[DOI]

Dataset, September, 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

Expected Runtime Analyis by Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Probabilistic Programming, 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]