CIS 842 Weekly Explorations

In addition to assigned exercises and reading, the course instructors will often identify material that is interesting and relevant for the course. The study of the material is not required, but we hope that students will take time to explore the material listed on this page.

Several general resources on formal methods, model-checking, and software model-checking are listed below.

As the course progresses, additional material relevant to the weekly lectures will be posted.

Online Documentation and Resources

Here are some other resources that you might enjoy exploring.

SLAM project
ESC/Java
Verisoft
Mocha
ETI Repository
iContract is a Java-based solution for dynamic checking of design contracts
iDoclet is a Javadoc-based documentation extractor that knows about iContract tags
JMSAssert is another Java-based design by contract system
The World Wide Web Virtual Library: Formal Methods

Week 1: Course Overview and Spin

Article on model checking properties of the Cray S1 supercomputer
Initial email on the comp.risks newsgroup on NASA Mars Pathfinder bug that spawned a lot of discussion.
Subsequent article on Robot Magazine article on NASA Mars Pathfinder bug
Article on Ariane 5 bug.
Article on Therac 25 problems.
comp.risks -- home page of newsgroup focused on computer-associated risks and safety critical computing.
Philip Koopman has done a lot of work on dependendable embedded software and he has some interesting links off of his home page (check out some of his courses).

Maintained by John Hatcliff [HOME]