This award supports a three year collaborative research project between Professor Andre Scedrov of the University of Pennsylvania and Professor Mitsuhiro Okada of KeioUniversity in Tokyo, Japan. The researchers will undertake a study of the logical methods for formal verification of software, with an emphasis on logical methods. The research effort will involve applying logical notions and methods to various aspects of software specification and verification. The main research themes are: 1) linear logic as a specification language and the related automated environments; 2) protocols, games, security and logic; 3) program analysis, security and logic; and 4) concurrent constraint programming. Planned research topics include: 1) proposed proof-based state exploration and verification techniques and decision procedures with applications to real-time and hybrid system specification and verification; 2) applications to protocol analysis and threat analysis; 3) Java bytecode verification and array-bound checking; 4) extensions of proof-carrying code methodology for safety and security properties of untrusted code to properties involving state; 5) type systems for mobile computation and communication; and 6) the design and implementation of programming languages for the domain of software systems that include concurrency and distribution.
This project brings together the efforts of two laboratories that have complementary expertise and research capabilities. Results of this research would provide for more predictable, reliable software. This, in turn, would provide for more reliable computing systems. This research advances international human resources through the participation of younger scientists. Through the exchange of ideas and technology, this project will broaden our base of basic knowledge and promote international understanding and cooperation. ***
