Title: Algorithmic Software Verification
Speaker: Rajeev Alur, University of Pennsylvania
Date: Monday, April 19, 2004 3:30-4:30pm
Location: DIMACS Center, CoRE Bldg, Room 431, Rutgers University, Busch Campus, Piscataway, NJ
Abstract:
Building tools that can certify correctness of software systems with respect to their specifications, or reveal inconsistencies, remains a grand challenge for computer science. In this talk, I will first survey the progress in formal methods for specification and verification from early days of manual proofs of sorting programs using loop invariants to today's highly optimized and automated tools for discovering bugs in network protocols and device drivers. Then, I will describe some of our current research directions. In particular, I will discuss a surprising recent theoretical result concerning algorithmic verification of context-free properties of recursive programs, and a new project for automatic synthesis of state-machine interfaces for Java classes.
See Webpage: http://www.cs.rutgers.edu/~muthu/theory.html