CISE Postdoctoral Research Associateships in Experimental Computer Science - Verifying Implementations of Model Checking Algorithms

CISE 实验计算机科学博士后研究奖学金 - 验证模型检查算法的实现

• 批准号: 0072761
• 负责人: John Launchbury
• 金额: $ 6.6万
• 依托单位: Oregon Health & Science University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2000
• 资助国家: 美国
• 起止时间: 2000-10-01 至 2003-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0072761&HistoricalAwards=false
• 关键词: CISE; Postdoctoral; Research; Associateships; Experimental

EIA-0072761Launchbury, JohnOregon Graduate InstituteCISE Postdoctoral Associates in Experimental Computer Science: VerifyingImplementations of Model Checking AlgorithmsModel checkers are starting to have a profound impact on the design ofcomputer systems, both hardware and software. They have demonstrated anability not only of discovering deep bugs in systems that traditionaltesting methods could not discover, but also of demonstrating thecorrectness of designs and implementations. However, in order to beincreasingly effective, model checkers have been increasing in complexity,and now are themselves becoming susceptible to buggy implementations, andhence contain serious soundness defects. The postdoctoral associate willdevelop methods for ensuring that complex implementations of model checkersare sound, and hence able to be used with confidence. He or she willanalyze the key implementation techniques that underlie modern modelchecking algorithms, such as those used to implement Binary DecisionDiagram (BDD) algorithms, and develop a formal (machine-checked) theory ofthese implementation strategies. The theory will be used to verify thecorrectness of the corresponding BDD algorithms.

EIA-0072761 Launchbury，JohnOregon Graduate InstituteCISE Postdoctoral Associates in Experimental Computer Science：Verifying Implementations of Model Checking模型检查器开始对计算机系统的设计产生深远的影响，包括硬件和软件。 他们不仅展示了发现系统中传统测试方法无法发现的深层错误的能力，而且展示了设计和实现的正确性。 然而，为了提高效率，模型检查器的复杂性一直在增加，现在它们本身也变得容易受到错误实现的影响，因此包含严重的可靠性缺陷。 博士后助理将开发方法，以确保模型检查器的复杂实现是合理的，因此能够放心使用。 他或她将分析现代模型检查算法的关键实现技术，例如用于实现二进制决策图（BDD）算法的技术，并开发这些实现策略的正式（机器检查）理论。 该理论将用于验证相应BDD算法的正确性。