What comes after PVS?

[John Rushby <rushby@csl.sri.com>]

Sign up for our tutorial at FME (part of FLoC) and learn about ICS,
SAL, and PVS 3,0
 http://floc02.diku.dk/FME/SOTA.html

Saturday is the deadline for early registration for all FLoC meetings
 http://floc02.diku.dk/

A more technical tutorial by Shankar, Harald Ruess, and Ashish Tiwari
describes the theory behind the ICS decision procedures
 http://floc02.diku.dk/CADE/Combined.html

You might also find it interesting to see what some of our industrial
partners are doing with this technology
  http://www.transeda.com/news/PressCov/SRI.html

But don't worry: it all remains free for academic research



Other PVS and SRI-related highlights at FLoC:

Shankar is the invited speaker for FME, LICS, and RTA
 http://floc02.diku.dk/bio/Shankar%3AFLoC%3A2002%3AFME+LICS+RTA.html

The paper by Shankar and Harald Ruess in the RTA proceedings (see
their home pages) describes the theoretical background to ICS

Tha CADE paper by Shankar and Jonathan Ford describes the formal
verification (in PVS) of the single-theory version of the technique
used in ICS

The LICS paper by Ashish Tiwari describes a polynomial time algorithm
for deciding confluence of ground term rewrite systems

The short LICS presentation by Jonathan Ford, Ian Mason, and Shankar
describes lessons learned from some formal developments in PVS

FME papers by Neil Henderson, and Stephen Paynter, by Vlad Rusu, and
by Michael Backes, Christian Jacobi, Birgit Pfitzmann, and a CAV paper
by Christian Jacobi all describe applications of PVS

And our colleague Mark Stickel of SRI's AI Center will receive the
2002 Herbrand Award at CADE


We hope to see many of you there,
John Rushby