Output details

Bayesian statistical model checking with application to Stateflow/Simulink verification

<07> We present the first approach for verifying temporal logic properties of Stateflow/Simulink models, the de-facto standard for developing embedded systems. We introduce Bayesian sequential estimation and show that it enables orders of magnitude faster verification than other techniques. I was invited to present an earlier version of this work at the AVACS Spring School, Oldenburg (Germany), 15-19 March 2010. This paper led to a $1,300,000 (£815,000) grant from the US Office of Naval Research (PI Edmund M. Clarke – emc@cs.cmu.edu; award no. N000141010188). The paper is an invited submission to a journal special issue dedicated to probabilistic model checking.