Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
DOI10.1016/J.TCS.2024.114876MaRDI QIDQ6639734FDOQ6639734
Authors: Kangfeng Ye, Jim Woodcock, Simon Foster 
Publication date: 18 November 2024
Published in: Theoretical Computer Science (Search for Journal in Brave)
Recommendations
classificationmachine learningprobability distributionstheorem provingroboticsautomated reasoningformal semanticsformal verificationIsabelle/HOLfixed-point theoremsquantitative verificationprobabilistic modelsprobabilistic 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
- Title not available (Why is that?)
- EasyCrypt: a tutorial
- Formal certification of code-based cryptographic proofs
- Constructive versions of Tarski's fixed point theorems
- A lattice-theoretical fixpoint theorem and its applications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theoretical Aspects of Computing - ICTAC 2004
- Semantics with applications: an appetizer.
- Bisimulation through probabilistic testing
- Two Notes on Notation
- Title not available (Why is that?)
- Type classes and filters for mathematical analysis in Isabelle/HOL
- An axiomatic basis for computer programming
- Title not available (Why is that?)
- A probabilistic PDL
- Reactive, generative, and stratified models of probabilistic processes
- Abstraction, Refinement and Proof for Probabilistic Systems
- Semantics of probabilistic programs
- Proofs of randomized algorithms in Coq
- FDR3 -- a modern refinement checker for CSP
- Title not available (Why is that?)
- Reasoning about probabilistic sequential programs
- Probabilistic communicating processes
- An assertion-based program logic for probabilistic programs
- Refinement-oriented probability for CSP
- Probabilistic models for the guarded command language
- Probabilistic extensions of process algebras.
- Title not available (Why is that?)
- Predicative programming Part I
- Predicative programming Part II
- Composition and behaviors of probabilistic I/O automata
- Probabilistic guarded commands mechanized in HOL
- Programs are predicates
- Title not available (Why is that?)
- Mathematics of Program Construction
- A probability perspective
- VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
- Probabilistic termination: soundness, completeness, and compositionality
- Integrated Formal Methods
- On the hardness of analyzing probabilistic programs
- Weakest precondition reasoning for expected runtimes of randomized algorithms
- 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
- Term Rewriting and Applications
- Title not available (Why is that?)
- VPHL: a verified partial-correctness logic for probabilistic programs
- Unifying heterogeneous state-spaces with lenses
- Weakest precondition reasoning for expected run-times of probabilistic programs
- On the hardness of almost-sure termination
- Specifications, programs, and total correctness
- Communicating Sequential Processes. The First 25 Years
- New approaches for almost-sure termination of probabilistic programs
- Automated reasoning for probabilistic sequential programs with theorem proving
- Probabilistic semantics for RoboChart. A weakest completion approach
- On the calculus of relations.
This page was built for publication: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6639734)
