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

EIA-0072761Launchbury，John Oregon Graduate Institute CSE实验计算机科学博士后助理：验证模型检查算法的实现模型检查器开始对计算机系统的设计产生深远的影响，无论是硬件还是软件。它们不仅证明了发现传统测试方法无法发现的系统中的深层次错误的能力，而且还证明了设计和实现的正确性。然而，为了变得越来越有效，模型检查器的复杂性一直在增加，现在它们本身变得容易受到错误实现的影响，因此包含严重的健壮性缺陷。博士后助理将制定方法，以确保模型检查器的复杂实现是合理的，从而能够放心地使用。他或她将分析支撑现代模型检查算法的关键实现技术，例如用于实现二叉决策图(BDD)算法的实现技术，并开发这些实现策略的形式化(机器检查)理论。该理论将被用于验证相应的BDD算法的正确性。

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.