Bounded model checking for probabilistic programs

DOI10.1007/978-3-319-46520-3_5zbMath1398.68343arXiv1605.04477OpenAlexW2395880299MaRDI QIDQ1990501

Nils Jansen, Lukas Westhofen, Benjamin Lucien Kaminski, Christian Dehnert, Joost-Pieter Katoen

Publication date: 25 October 2018

Full work available at URL: https://arxiv.org/abs/1605.04477

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (4)

Latticed \(k\)-induction with an application to probabilistic programs ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

This page was built for publication: Bounded model checking for probabilistic programs