The Organizing Committee of FM2009 invited proposals for half or whole day tutorials the wide area of formal methods, in particular: novel applications of existing tools and techniques, advanced topics in formal methods research, and uses of formal methods in emerging fields. From the submitted proposals, seven were initially selected. Two of these have gained sufficient support in early registration, and will take place preceding the Symposium, on 2 and 3 November 2009.
General inquiries regarding the tutorials can be made to the Organizing Committee, email@example.com.
Tutors Ganesh Gopalakrishnan and Robert M. KirbyIn this hands-on tutorial, we present a rapidly emerging approach to formally verify concurrent programs using Dynamic Verification. Given a concurrent message-passing or shared memory program, a dynamic verification system instruments the program to trap the API calls, and orchestrates relevant interleavings, while concretely running the program. Our research is unique in realizing this approach for three different APIs, namely: (i) the widely used message passing API called MPI, (ii) the widely used shared memory threading API called Pthreads, and (iii) the emerging multi-core communications API called MCAPI. We will explain the principles behind the dynamic partial order reduction algorithm used in these tools, pointing out their similarities and differences. We provide a bootable LiveDVD (for you to keep) which allows you to experiment with actual C programs making MPI and thread calls. We also provide Eclipse based graphical user interface that permits an interesting array of execution control and viewing facilities. Contrasts with similar tools (e.g., Verisoft, CHESS, and the Java Path Finder) will be provided.
Half-day tutorial on Tuesday morning November 3, 2009, Main Building room HG 8.61.
Tutors Ion Petre and Ralph-Johan BackThis one-day tutorial provides an introduction to computational systems biology, starting with a crash course on molecular biology for computer scientist and continuing with discrete, continuous and stochastic modeling techniques, as well as formal methods-based approaches. A demonstration is included on Copasi (Complex Pathway Simulator), a useful tool for modeling and simulating sysbio projects. The well-known heat shock response, that the tutors and their research groups have been working on already for some years, will serve as a running example connecting the various topics.
Full-day tutorial on Monday November 2, 2009, Auditorium room CZ12b.