Cover Image

Caesar: A Deductive Verifier for Probabilistic Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Schröer, Philipp, Batz, Kevin, Dural, Umut Yiğit, Haase, Darion, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
by: Schröer, Philipp, et al.
Published: (2025)

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
by: Haase, Darion, et al.
Published: (2026)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

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)
by: Batz, Kevin, et al.
Published: (2024)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
by: Schröer, Philipp, et al.
Published: (2026)

Unknown Biases and Timing Constraints in Timed Automata
by: Haase, Darion, et al.
Published: (2024)

Quantifier Elimination and Craig Interpolation, Quantitatively
by: Batz, Kevin, et al.
Published: (2025)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
by: Yang, Xiaoxiao, et al.
Published: (2017)

Data Petri Nets meet Probabilistic Programming (Extended version)
by: Kuhn, Martin, et al.
Published: (2024)

Verifying Sampling Algorithms via Distributional Invariants
by: Zilken, Daniel, et al.
Published: (2025)

Model Checking Temporal Properties of Recursive Probabilistic Programs
by: Winkler, Tobias, et al.
Published: (2021)

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
by: Acevedo, Emmanuel Suárez, et al.
Published: (2026)

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
by: Young, David, et al.
Published: (2024)

Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
by: Zhang, Linpeng, et al.
Published: (2024)

Newtonian Program Analysis of Probabilistic Programs
by: Wang, Di, et al.
Published: (2023)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

Multi-Language Probabilistic Programming
by: Stites, Sam, et al.
Published: (2025)

Real-Time Probabilistic Programming
by: Hummelgren, Lars, et al.
Published: (2023)

Dependent Session Types for Verified Concurrent Programming
by: Fu, Qiancheng, et al.
Published: (2025)

Probabilistic Programs of Thought
by: Garg, Poorva, et al.
Published: (2026)

Compositional Reasoning for Probabilistic Automata with Uncertainty
by: Mertens, Hannah, et al.
Published: (2026)

Compositional Reasoning for Parametric Probabilistic Automata
by: Mertens, Hannah, et al.
Published: (2025)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
by: Agarwal, Shubham, et al.
Published: (2026)

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version)
by: Yan, Pengbo, et al.
Published: (2024)

Programming and Reasoning in Partially Observable Probabilistic Environments
by: Gürtler, Tobias, et al.
Published: (2025)

\texttt{ReMind}: Understanding Deductive Code Reasoning in LLMs
by: Gao, Jun, et al.
Published: (2025)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
by: Shen, Gan, et al.
Published: (2024)

Qafny: A Quantum-Program Verifier
by: Li, Liyi, et al.
Published: (2022)

Sound Interval-Based Synthesis for Probabilistic Programs
by: Espada, Guilherme, et al.
Published: (2025)

Data-Driven Invariant Learning for Probabilistic Programs
by: Bao, Jialu, et al.
Published: (2021)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
by: Pedersen, Jan, et al.
Published: (2025)

Refuting Equivalence in Probabilistic Programs with Conditioning
by: Chatterjee, Krishnendu, et al.
Published: (2025)

Equivalence and Similarity Refutation for Probabilistic Programs
by: Chatterjee, Krishnendu, et al.
Published: (2024)