Brontekst bekijken van 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. [[Gebruiker:Faranak Heidarian|Faranak Heidarian]]

* &mu;-calculus. [[Gebruiker:Faranak Heidarian|Faranak Heidarian]]. (Perhaps invite Angelika or some &mu;CRL expert for about two lectures.)

* Cellular automata. [[Gebruiker:Faranak Heidarian|Faranak Heidarian]]

* something about games, proposed by [[Gebruiker:David Jansen|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) [[Gebruiker:David Jansen|David Jansen]]

* Model checking discounted temporal properties by Luca de Alfaro, ..., Mariëlle Stoelinga. Theoretical Computer Science, 2005. [[Gebruiker:David Jansen|David Jansen]]

* recently several papers have appeared (or are being submitted) that discuss links between Bayesian statistics and probabilistic model checking, for instance by [http://csb2009.org/pdf/068Langmead.pdf 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. [[Gebruiker:Frits Vaandrager|Frits Vaandrager]]

* at FM'09 there was a very interesting keynote by Rajamani.  In particular I was intrigued by his report on the [http://www.springerlink.com/content/l8743ut1m443qu15/ Yogi] tool that combines verification with testing, and the [http://portal.acm.org/citation.cfm?doid=1542476.1542485 Merlin tool] that uses Bayesian inference for bug finding. [[Gebruiker:Frits Vaandrager|Frits Vaandrager]]

* [http://portal.acm.org/citation.cfm?id=1347383 Compositional Real-Time Scheduling Framework with periodic Model] by Shin and Lee. [[Gebruiker:Frits Vaandrager|Frits Vaandrager]]

* Automata learning. To be read in 2010. [[Gebruiker:Frits Vaandrager|Frits Vaandrager]]

* Abstract interpretation [[Gebruiker:Jan Tretmans|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) [[Gebruiker:Julien Schmaltz|Julien Schmaltz]]
* Termination analysis. [[Gebruiker:Freek Verbeek|Freek Verbeek]].

* Predictability analysis. Work done by Reinhard Wilhelm, Saarbrücken, and Lothar Thiele (Pareto analysis for worst-case execution time) [[Gebruiker:Georgeta Igna|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.