Wolf – Bug Hunter for Concurrent Software Using Formal Methods
作者： Sharon Barner , Ziv Glazberg , Ishai Rabinovitz
DOI: 10.1007/11513988_16
关键词:
摘要: Wolf is a “push-button” model checker for concurrent C programs developed in IBM Haifa. It automatically generates both the and specification directly from code. Currently, uses BDD-based symbolic methods integrated with guided search framework. According to our experiments, these complement explicit exploration of software checking.
springer.com
sci-hub.st 参考文章(14)
Sharon Barner, Ishai Rabinovitz, Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning Lecture Notes in Computer Science. pp. 35- 50 ,(2003) , 10.1007/978-3-540-39724-3_6
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Thomas Ball, Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs international workshop on model checking software. pp. 113- 130 ,(2000) , 10.1007/10722468_7
Ishai Rabinovitz, Orna Grumberg, Bounded Model Checking of Concurrent Programs Computer Aided Verification. pp. 82- 97 ,(2005) , 10.1007/11513988_9
Klaus Havelund, Thomas Pressburger, Model checking JAVA programs using JAVA PathFinder International Journal on Software Tools for Technology Transfer. ,vol. 2, pp. 366- 381 ,(2000) , 10.1007/S100090050043
Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar, Efficient SAT-based bounded model checking for software verification leveraging applications of formal methods. ,vol. 404, pp. 256- 274 ,(2008) , 10.1016/J.TCS.2008.03.013
Robby, Matthew B. Dwyer, John Hatcliff, Bogor: an extensible and highly-modular software model checking framework foundations of software engineering. ,vol. 28, pp. 267- 276 ,(2003) , 10.1145/940071.940107
Edmund Clarke, Daniel Kroening, Flavio Lerda, A Tool for Checking ANSI-C Programs tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 168- 176 ,(2004) , 10.1007/978-3-540-24730-2_15
Ilan Beer, Shoham Ben-David, Cindy Eisner, Avner Landver, RuleBase: an industry-oriented formal verification tool design automation conference. pp. 655- 660 ,(1996) , 10.1145/240518.240642
Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie, Zing: A Model Checker for Concurrent Software Computer Aided Verification. pp. 484- 487 ,(2004) , 10.1007/978-3-540-27813-9_42