CISE PostDoc: Verification Tools for Net-Based Programming

Cleaveland, Walter R.北卡罗莱纳州立大学CISE博士后：基于网络编程的验证工具本项目致力于开发有效的自动化技术，用于建模和推理基于网络的软件的正确性。该项目的动机源于Java等基于网络的语言编程的爆炸式流行，以及一个功能不正确的面向网络的程序可能对整个网络造成严重损害，而不仅仅是网络中的单个站点。研究工作所使用的方法是基于那些在有限状态系统（如通信协议）分析和编程语言结构严格建模中成功使用的方法。私家侦探在前者方面有丰富的经验，但在后者方面却很少；因此，增加一名具有后一种背景的博士后研究助理对于项目的预期结果——用于自动分析移动代码的安全性和容错性的一系列技术和相关工具——的实现至关重要。

98-05604 Cleaveland, Walter R. North Carolina State University CISE PostDoc: Verification Tool for Net-based Programming This project is devoted to the development of effective automated techniques for modeling and reasoning about the correctness of network-based software. The motivation for the project arises from the exploding popularity of programming in net-based languages like Java coupled with the fact that an incorrectly functioning net-oriented program can inflict serious damage on a whole network and not just on a single site within the network. The methods to be used by the research effort are based on those used successfully in the analysis of finite-state systems such as communications protocols and in the rigorous modeling of programming language constructs. The PI has substantial experience in the former but very little with the latter; the addition of a postdoctoral research associate with a background in the latter is therefore essential for the project's anticipated results---a collection of techniques, and associated tools, for analyzing automatically the safety and fault-tolerance of mobile code---to be achieved.