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

Oregon Health & Science University, Portland OR

Investigators

Abstract

EIA-0072761 Launchbury, John Oregon Graduate Institute CISE Postdoctoral Associates in Experimental Computer Science: Verifying Implementations of Model Checking Algorithms Model checkers are starting to have a profound impact on the design of computer systems, both hardware and software. They have demonstrated an ability not only of discovering deep bugs in systems that traditional testing methods could not discover, but also of demonstrating the correctness of designs and implementations. However, in order to be increasingly effective, model checkers have been increasing in complexity, and now are themselves becoming susceptible to buggy implementations, and hence contain serious soundness defects. The postdoctoral associate will develop methods for ensuring that complex implementations of model checkers are sound, and hence able to be used with confidence. He or she will analyze the key implementation techniques that underlie modern model checking algorithms, such as those used to implement Binary Decision Diagram (BDD) algorithms, and develop a formal (machine-checked) theory of these implementation strategies. The theory will be used to verify the correctness of the corresponding BDD algorithms.