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

This page gives access to information about the Formal Methods Seminar (Com S 610 RL) as taught (in Fall 2001) by Robyn Lutz and Gary T. Leavens for the Department of Computer Science at Iowa State University.

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
Other papers may be added if time permits.  Participants are also welcome to suggest papers.


Last update $Date: 2007/08/10 23:10:51 $
This page maintained by:
Gary T. Leavens

229 Atanasoff Hall
Department of Computer Science, Iowa State University
Ames, Iowa 50011-1040 USA