Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
DOI10.1016/j.tcs.2024.114876MaRDI QIDQ6639734
Simon Foster, J. C. P. Woodcock, Kangfeng Ye
Publication date: 18 November 2024
Published in: Theoretical Computer Science (Search for Journal in Brave)
classificationformal semanticstheorem provingautomated reasoningformal verificationprobability distributionsroboticsmachine learningfixed-point theoremsprobabilistic modelsIsabelle/HOLquantitative verificationprobabilistic programsUTPpredicative programming
Reasoning under uncertainty in the context of artificial intelligence (68T37) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A probability perspective
- Probabilistic communicating processes
- Semantics with applications: an appetizer.
- Proofs of randomized algorithms in Coq
- A probabilistic PDL
- Semantics of probabilistic programs
- Bisimulation through probabilistic testing
- Constructive versions of Tarski's fixed point theorems
- Probabilistic models for the guarded command language
- Composition and behaviors of probabilistic I/O automata
- On the hardness of analyzing probabilistic programs
- Specifications, programs, and total correctness
- Reactive, generative, and stratified models of probabilistic processes
- Probabilistic semantics for RoboChart. A weakest completion approach
- An assertion-based program logic for probabilistic programs
- Refinement-oriented probability for CSP
- Reasoning about probabilistic sequential programs
- Probabilistic guarded commands mechanized in HOL
- On the calculus of relations.
- A lattice-theoretical fixpoint theorem and its applications
- Automated reasoning for probabilistic sequential programs with theorem proving
- Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
- Probabilistic Termination
- On the Hardness of Almost–Sure Termination
- VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
- Two Notes on Notation
- Unifying Heterogeneous State-Spaces with Lenses
- Programs are predicates
- Predicative programming Part I
- Predicative programming Part II
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Abstraction, Refinement and Proof for Probabilistic Systems
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Semantics of Probabilistic Programming: A Gentle Introduction
- Termination Analysis of Probabilistic Programs with Martingales
- EasyCrypt: A Tutorial
- Formal certification of code-based cryptographic proofs
- Mathematics of Program Construction
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- FDR3 — A Modern Refinement Checker for CSP
- An axiomatic basis for computer programming
- Term Rewriting and Applications
- Communicating Sequential Processes. The First 25 Years
- Theoretical Aspects of Computing - ICTAC 2004
- Integrated Formal Methods
- VPHL: a verified partial-correctness logic for probabilistic programs
- New approaches for almost-sure termination of probabilistic programs
This page was built for publication: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
