Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: CAV, pp. 484–487 (2004)
Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proc. 7th International SPIN Workshop (2000)
Barner, S., Rabinovitz, I.: Effcient symbolic model checking of software using partial disjunctive partitioning. In: CHARME, pp. 35–50 (2003)
Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: An industry-oriented formal verification tool. In: Design Automation Conference, pp. 655–660 (1996)
Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Design Automation Conference, June 2000, pp. 29–34 (2000)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ansi-c programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: IPDPS, p. 286 (2003)
Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA pathfinder. STTT 2(4), 366–381 (2000)
Holzmann, G.: On the fly, LTL model checking with SPIN: Simple Spin manual, At http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html
Ivancic, F., Yang, Z., Gupta, A., Ganai, M.K., Ashar, P.: Efficient SAT-based bounded model checking for software verification, ISoLA (2004)
Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: CAV (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barner, S., Glazberg, Z., Rabinovitz, I. (2005). Wolf – Bug Hunter for Concurrent Software Using Formal Methods. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_16
Download citation
DOI: https://doi.org/10.1007/11513988_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)