[9-26]FDR3: current and recent developments in CSP model checking
文章來源： | 發布時間：2016-09-26 | 【打印】 【關閉】
Title: FDR3: current and recent developments in CSP model checking
Speaker: Prof. Bill Roscoe
Department of Computer Science, Oxford University
Time: 10:00am, Monday, Sept. 26, 2016
Venue: Room 334, Building 5, State Key Lab. of Computer Science, Institute of Software
I will review FDR3, the parallel implementation of the CSP refinement checker FDR, together with some of its approaches to the state explosion problem. These include symmetry reduction, partial order reduction as well as improvements to its support for semantic-preserving compression. I will also discuss a new approach to verification which I term "static model checking", using deadlock analysis as the motivating example. I will also review the industrial uses of FDR and discuss our plans for building new technology for supporting model-based embedded software development using technology similar to FDR.
