Model checking concurrent programs with nondeterminism and randomization

DOI10.4230/LIPICS.FSTTCS.2010.364MaRDI QIDQ2908866zbMATH OpenOpenAlexFDO

Authors Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Publication date 29 August 2012

Full work available at URL http://subs.emis.de/LIPIcs/frontdoor_b84b.html

zbMATH Keywords

model-checkingprobabilistic programlocally Markovian schedulerview consistent scheduler

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model checking concurrent programs
• On verifying that a concurrent program satisfies a nondeterministic specification
• Model checking of probabilistic and nondeterministic systems
• Computer Aided Verification
• The fixed-parameter tractability of model checking concurrent systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Modular verification of concurrent programs via sequential model checking
• Model checking of concurrent algorithms: from Java to C

Cited in

(6)

• Schedulers are no prophets
• scientific article; zbMATH DE number 1884415 (Why is no real title available?)
• Concurrent Probabilistic Programs, Or: How to Schedule If You Must
• Modular verification of protocol equivalence in the presence of randomness
• On verifying that a concurrent program satisfies a nondeterministic specification
• Partial-observation stochastic games, how to win when belief fails

This page was built for publication: Model checking concurrent programs with nondeterminism and randomization

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