This course is scheduled for the Spring semester 2004 as a graduate seminar course. It's a natural follow-up to CS-845: Formal Specification and Verification of Software Systems. It can also be opened to undergraduates who perfomed well in CS-745.
The objective for this course is to go beyond sequential imperative programs specified in terms of pre/post-conditions. In particular, we are interested in reasoning about concurrent and distributed systems specified in temporal logic. These classes of programs involve specific aspects such as concurrency, communication, nondeterminism, etc., and are more complex than sequential programs in various respects, such as interaction and composition. As a result, the specification and verification problem becomes much trickier.
As long as we are working on those aspects of specification and verification that I am interested in, I'm rather flexible regarding what the course is really about. In particular, the emphasis can be on specification or on verification, on case studies or on theory, on tools or on good old hand-written mathematics. Different students can even focus on different aspects, as it happened last time I taught the course.
Last time, we used TLA+ as our main logical framework to specify and verify several algorithms. Although TLA proofs are not supported by any (simple, i.e., not Isabelle/TLA) tool, TLA+ modules are supported by some tools, most notably a parser/semantic checker (SANY), a pretty-printer (TLATEX) and a model-checker/simulator (TLC).
Between challenging hand-written proof, we had some fun playing with those tools. In particular, TLC is great at finding bugs before wasting our time trying to prove something that cannot possibly be proved. See the report on TLC use that I wrote for TLC's developers.
CS-986 is offered again next Spring, TR 2:10 - 3:30. Students who are considering taking this course should contact me now, so that we can talk about their interests and I can begin to set up the course.
>
Last modified: Mon Nov 17 15:24:17 EST 2003