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

launchbury， john norregon研究生院，ise实验计算机科学博士后助理：验证模型检查算法的实现模型检查器开始对计算机系统的设计产生深远的影响，包括硬件和软件。他们不仅展示了发现传统测试方法无法发现的系统深层缺陷的能力，而且还展示了设计和实现的正确性。然而，为了变得越来越有效，模型检查器的复杂性一直在增加，并且现在它们自己变得容易受到错误实现的影响，因此包含严重的可靠性缺陷。博士后助理将开发方法，以确保模型检查器的复杂实现是健全的，因此能够自信地使用。他或她将分析现代模型检查算法的关键实现技术，例如用于实现二进制决策图（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.