Model Checking Reading Club/Suggestions for Papers (2009-2010)

Please add your suggestions for articles you would like to discuss in the Reading Club!

---

• Pnueli: Using Abstraction to Verify Arbitrary Temporal Properties. APSEC 2008. Faranak Heidarian

• μ-calculus. Faranak Heidarian. (Perhaps invite Angelika or some μCRL expert for about two lectures.)

• Cellular automata. Faranak Heidarian

• something about games, proposed by David Jansen Frits proposes as a concrete article: Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime: Efficient On-the-Fly Algorithms for the Analysis of Timed Games. CONCUR 2005: 66-80

• cost (rather specialistic) David Jansen

• Model checking discounted temporal properties by Luca de Alfaro, ..., Mariëlle Stoelinga. Theoretical Computer Science, 2005. David Jansen

• recently several papers have appeared (or are being submitted) that discuss links between Bayesian statistics and probabilistic model checking, for instance by Langmead and by Clarke et al. This appears to be exciting research and should particularly be interesting for MBSD since it is on the borderline of expertise of two groups. I miss the necessary background on Bayesian statistics though. So I'd be interested to study some basic papers/textbooks on Bayesian statistics, followed by a study of these papers. Frits Vaandrager

• at FM'09 there was a very interesting keynote by Rajamani. In particular I was intrigued by his report on the Yogi tool that combines verification with testing, and the Merlin tool that uses Bayesian inference for bug finding. Frits Vaandrager

• Compositional Real-Time Scheduling Framework with periodic Model by Shin and Lee. Frits Vaandrager

• Automata learning. To be read in 2010. Frits Vaandrager

• Abstract interpretation Jan Tretmans According to Faranak, it's not too closely related to Pnueli's article mentioned above.
• Applying model checking in biology (Joost-Pieter gave a recent sales talk on applying model checking to any kind of system except computer science) Julien Schmaltz
• Termination analysis. Freek Verbeek.

• Predictability analysis. Work done by Reinhard Wilhelm, Saarbrücken, and Lothar Thiele (Pareto analysis for worst-case execution time) Georgeta Igna.

---

Decision: Faranak will pick an article on abstraction; this will be discussed during the next two sessions. We feel that after one session, there may be still open questions that can best be postponed to another session. Later, Frits is ready to present about timed games and David about DCTL.