Generating counterexamples for quantitative safety specifications in probabilistic B

DOI10.1016/J.JLAP.2011.06.001zbMATH Open1269.68047OpenAlexW2126704329WikidataQ124807099 ScholiaQ124807099MaRDI QIDQ652160FDOQ652160

Ukachukwu Ndukwu

Publication date: 19 December 2011

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2011.06.001

Recommendations

• Counterexamples in Probabilistic Model Checking
• High-level counterexamples for probabilistic automata
• Bounded model checking for probabilistic programs
• Verification of Probabilistic Programs
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods

zbMATH Keywords

expectationscounterexamplesfailuresprobabilistic Bquantitative safety

Mathematics Subject Classification ID

Theory of programming languages (68N15) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in artificial intelligence (68T27)

Cites Work

• Finding the k Shortest Paths
• Borel determinacy
• A logic for reasoning about time and reliability
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• The B-Book
• Title not available (Why is that?)
• Abstraction, Refinement and Proof for Probabilistic Systems
• Optimal control of diffusion processes with reflection
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Stochastic Model Checking
• Counterexamples in Probabilistic Model Checking
• Formal Modeling and Analysis of Timed Systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• PRISM
• Rodin
• ProB
• CESAR

This page was built for publication: Generating counterexamples for quantitative safety specifications in probabilistic B

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q652160)