Wolf: bug hunter for concurrent software using formal methods

Sharon Barner,Ziv Glazberg,Ishai Rabinovitz

COMPUTER AIDED VERIFICATION, PROCEEDINGS（2005）

引用 15|浏览0

暂无评分

摘要

Wolf is a “push-button” model checker for concurrent C programs developed in IBM Haifa. It automatically generates both the model and the specification directly from the C code. Currently, Wolf uses BDD-based symbolic methods integrated with a guided search framework. According to our experiments, these methods complement explicit exploration methods of software model checking.

查看译文

关键词

software model checking,formal method,model checker,concurrent c program,concurrent software,symbolic method,search framework,ibm haifa,explicit exploration method,c code,bug hunter

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要