Subject: 590L this quarter
From: Todd D Millstein (todd@cs.washington.edu)
Date: Mon Mar 27 2000 - 16:22:30 PST
There will be a 590L this quarter on software model checking. Model
checking is a technique that has been used very successfully for verifying
properties of hardware systems, and recently people have started to look
at how the technique could be applied to software. The approach has
several nice properties: it's completely automatic, it produces a
counterexample upon verification failure, and it allows property
specifications in fairly rich languages based on temporal logics.
We will start by briefly reviewing the traditional model checking
framework, and then we'll look at how this framework could be applied to
the static analysis of programs: dataflow analysis, static typechecking,
formal verification, and anything else we can think of.
We will be meeting on Mondays from 2:30-3:20pm, and we'll start next week.
It will take a few days for this class to be officially added to the
course schedule. At that point, we'll know what room we'll be in, and
people can then sign up for the class.
If you're interested, please subscribe to the 590L mailing list (e-mail
majordomo@cs with the body reading "subscribe cse590l"), because future
announcements will be sent there.
Todd
This archive was generated by hypermail 2b25 : Tue Oct 03 2000 - 15:21:27 PDT