Specification and Verification Tools Seminar

Specification and Verification Tools Seminar (Fall 2008) Resources

This page provides various links to interesting systems for the Specification and Verification Tools Seminar.

Some tools related to requirements analysis.

• SCR
• RSML
• Statemate

Some tools related to (OO) domain analysis. (See also the model checking and proof checking tools below.)

• Alloy
• LSL
• Z

Some tools that start at the analysis level and can refine all the way down to the code level

• Event-B
• B Tool

Some tools related to software archicture.

• ArchJava

Some tools related to coding/APIs.

• Spec#
• UPPAAL
• Spark/Ada
• JStar
• Eiffel
• Larch/C++

Model checking tools.

• SMV
• Bandera
• JavaPathfinder
• SPIN
• FDR

Proof checking and proof assistant tools.

• PVS
• HOL and Isabelle/HOL
• Coq
• ACL2

Last modified Wednesday, September 3, 2008.