History Types and Verification: Monday April 12, 2004

Computer Science Seminar Series Presents

Title: History Types and Verification

Speaker:
      Dr Christian Skalka
      Department of Computer Science
      University of Vermont
      Burlington, VT 05405
      skalka-UYko1UTVIqz2fBVCVOL8/[email protected]

Date:       Monday, April 12th, 2004
Time:       11:15 a.m - 12:05 p.m
Location:   110 Kalkin

Abstract:

Safe program execution is crucial for modern information systems,
but is difficult to attain in practice.  Both faulty logic, due to programmer
errors, and access control violations, due to intentional attacks, can lead
to unsafe program executions.  Programming language-based tools and
techniques can increase safety by verifying at both compile- and run-time
that programs possess certain safety properties.

This presentation describes a new foundation for static verification
of program properties, built on a novel process for automatically
extracting event histories of program executions, and for specifying
and automatically verifying properties of these histories.  Our approach
combines a type and effect theory with model checking techniques,
which is expressive enough for application to a range of static analyses;
in particular, we will discuss language-based access control as an
application focus.

This is joint work with Scott Smith, Johns Hopkins University.

URL: http://www.cs.uvm.edu/seminars/seminar_series.shtml