Formal Methods Seminar (Com S 610 RL, Fall 2001)

Meetings will be held on Wednesdays from 1:10-2 PM, in 217 Atanasoff Hall. The first meeting will be September, 12 2001.  If you plan to attend, please send email to Robyn Lutz (rlutz@cs-DOT-iastate-DOT-edu).

You can sign up for 1 credit if you like by registering for course 610 RL. If you wish to register for this seminar, the registration number is 2724 092.  (This works to enroll with AccessPlus or touch-tone registration through August 31.) Students who are registered for credit will be expected to present a paper by leading the discussion on it.  Students registered for credit will also be expected to be active in reading papers and participating in discussions. (Grading is S/F only, of course.)

You can also attend without registering if you wish.

A tentative list of papers for the seminar is as follows:

1. Edmund M. Clarke and Jeannette M. Wing, et al.. Formal Methods: State of the Art and Future Directions.ACM Computing Surveys, 28(4):626-643, Dec. 1996. http://www.acm.org/pubs/citations/journals/surveys/1996-28-4/p626-clarke/
2. Nancy G. Leveson.  Software Safety in Embedded Computer Systems. Comm. ACM, 34(2):3-46, Feb. 1991.
3. Nancy G. Leveson.  Intent Specifications: An Approach to Building Human-Centered Specifications.  IEEE Trans. on Software Engin. 26(1):15-35, Jan. 2000. http://sunnyday.mit.edu/papers.html
4. John C. Knight, Kimberly S. Hanks, and Sean R. Travis. Tool Support for Production Use of Formal Techniques. International Symposium on Software Reliability Engineering, Hong Kong, November, 2001. http://www.cs.virginia.edu/~jck/publications/issre.2001.fm.pdf
5. John Rushby. Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. IEEE Trans. on Software Engin. 25(5):651-660, Sept.-Oct. 1999.
6. Dimitri Naydich and David Guaspari. Timing Analysis by Model Checking.  The Fifth NASA Langley Formal Methods Workshop, Virginia, June, 2000.  http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/cpp07.pdf
7. K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, Jon L. White. Formal Analysis of the Remote Agent - Before and After Flight.  The Fifth NASA Langley Formal Methods Workshop, Virginia, June, 2000.  http://ase.arc.nasa.gov/havelund/Publications/rax.ps
8. David Coppit, Kevin J. Sullivan, and Joanne Bechta Dugan.  Formal Semantics of Models for Computational Engineering: A Case Study on Dynamic Fault Trees.  In Proc. 11th International Symposium on Software Reliabilty Engineering, ISSRE 2000, pages 270-282, Oct. 2000. http://www.coppit.org/soft_eng/papers/FormalSemanticsOfModelsForCompEng.pdf
9. John Rushby.  Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.  In D. Dams, R. Gerth, S. Leue and M. Massink (eds.), From Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops. Volume 1680 of Lecture Notes in Computer Science. Springer-Verlag, 1999. http://www.csl.sri.com/papers/s/p/spin99/spin99.ps.gz