!
FLUENT Verification ProjectRegular Teleconference
Attending: Hao, Riley, Zhen, Chris W, Porter, Mohammad, Lukas, Nisa, Tom, Payton, Laureano
Agenda
- Hao and Mohammad -- has been changing the code base entirely so that we can expand counterexample graph not from patterns but from transitions. New version doesn't work for PRISM models yet but is working for some abstract models. Discussion on importance sampling and stochastic simulation -- IS needs to be specialized to a particular type of property. Some discussion on Gillespie's algorithm and relationship between biochemical systems and CTMC models.
- Laureano -- update on IC3, better understanding of the basic structure.
- Nisa -- working on documenting code, cleaning up folder and file organization.
- Chris W & Tom -- developing a simple model of a faulty asynchronous data interface in PRISM, will use it along with Hao/Mohammad's counterexample model to explore IS options. Will post some papers on IS in CTMC.
- Zhen & Riley -- Update on Hazard Analysis iBiosim & STAMINA paper. Having some crashes due to insufficient memory.
- Lukas -- still working on paper; Riley will be second author.
- Porter -- working on various details.
#
meetings