U.S.-Japan Cooperative Science: Logical Methods for Formal Verification of Software

9815731Scedrov该奖项支持宾夕法尼亚大学的安德烈·塞德罗夫教授和日本东京庆应义乌大学的冈田光弘教授之间为期三年的合作研究项目。研究人员将对软件形式验证的逻辑方法进行研究，重点是逻辑方法。研究工作将涉及将逻辑概念和方法应用于软件规范和验证的各个方面。主要研究内容有：1)线性逻辑及其自动化环境；2)协议、游戏、安全与逻辑；3)程序分析、安全与逻辑；4)并发约束编程。计划的研究课题包括：1)提出了基于证明的状态探测和验证技术和决策程序，并应用于实时和混合系统规范和验证；2)应用于协议分析和威胁分析；3)Java字节码验证和数组界限检查；4)将不可信代码的安全和安全属性的证明携带代码方法扩展到涉及状态的属性；5)用于移动计算和通信的类型系统；以及6)软件系统领域的编程语言的设计和实现。该项目结合了两个具有互补专业知识和研究能力的实验室的努力。这项研究的结果将提供更可预测、更可靠的软件。反过来，这将提供更可靠的计算系统。这项研究通过年轻科学家的参与促进了国际人力资源的发展。通过思想和技术的交流，这个项目将扩大我们的基础知识基础，促进国际理解与合作。***

9815731ScedrovThis 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. ***