!
FLUENT Verification ProjectRegular Team Meeting
Attending: Chris W, Riley, Tom, Hao, Mohammad, Zhen
Agenda
- Chris M is on travel
- Mohammad: got code for counterexample generation implemented in PRISM “to some degree”, sent by Dave Parker. Have implemented one case of bounded until but not all of them. Implemented for both CTMC and DTMC (some cases overlap). CTL formulas overlap for some cases. Reading about model checking algorithms. Next step: study CTMC counterexample generation algorithm.
- Chris W: working on ASYNC abstract. Still trying to develop a minimal working example showing a decoding subciruit, PRISM model, property specification, and design application.
- Zhen: working on bug fixes. Possibly taking an undergrad assistant to work on chemical reaction network models.
- Riley: got a feel for the layout of STORM code and “found a couple of places to get my foot in the door”, making good progress there. Trying to parse properties into [tex]$\psi = \Phi U^I\Psi$[/tex].
