Formal Software Analysis Emerging Trends in Software Model Checking

ABSTRACT

The study of methodologies and techniques to produce correct software has been active for four decades. During this period, researchers have developed and investigated a wide variety of approaches, but techniques based on mathematical modeling of program behavior have been a particular focus since they offer the promise of both finding errors and assuring important program properties. The past fifteen years have seen a marked and accelerating shift towards algorithmic formal reasoning about program behavior - we refer to these as formal software analysis. In this paper, we define formal software analyses as having several important properties that distinguish them from other forms of software analysis. We describe three foundational formal software analyses, but focus on the adaptation of model checking to reason about software. We review emerging trends in software model checking and identify future directions that promise to significantly improve its cost-effectiveness.

REFERENCES

• 1: [1] J.-R. Abrial, E. Böorger, and H. Langmaack, editors. Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control, volume 1165 of Lecture Notes in Computer Science. Springer, 1996.
• 2: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 3: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 4: [4] R. Alur, P. Madhusudan, and W. Nam. Symbolic Compositional Verification by Learning Assumptions. In Proceedings of CAV'05, pages 548-562, 2005.
• 5: J. H. Andrews , L. C. Briand , Y. Labiche, Is mutation an appropriate tool for testing experiments?, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062530]
• 6: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 7: [7] J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, pages 115-137, 2005.
• 8: Antonia Bertolino, Software Testing Research: Achievements, Challenges, Dreams, 2007 Future of Software Engineering, p.85-103, May 23-25, 2007 [doi>10.1109/FOSE.2007.25]
• 9: David Binkley, Source Code Analysis: A Road Map, 2007 Future of Software Engineering, p.104-119, May 23-25, 2007 [doi>10.1109/FOSE.2007.27]
• 10: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 11: [11] L. Briand and A. Wolf, editors. Future of Software Engineering 2007. IEEE-CS Press, 2007.
• 12: [12] http://research.microsoft.com/ qadeer/cav-issta.htm.
• 13: Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004 [doi>10.1109/TSE.2004.22]
• 14: [14] Y. Cheon and G. T. Leavens. A runtime assertion checker for the Java modeling language. In Proceedings of the International Conference on Software Engineering Research and Practice, 2002.
• 15: [15] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV : a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410-425, 2000.
• 16: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 17: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 18: [18] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
• 19: [19] J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning Assumptions for Compositional Verification. In Proceedings of TACAS'03, pages 331-346, 2003.
• 20: Brian Cole , Daniel Hakim , David Hovemeyer , Reuven Lazarus , William Pugh , Kristin Stephens, Improving your software using static analysis to find bugs, Companion to the 21st ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1176617.1176667]
• 21: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 22: [22] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The astreé analyzer. In Proceeding of ESOP'05, pages 21-30, 2005.
• 23: Xianghua Deng , Jooyong Lee , Robby, Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.157-166, September 18-22, 2006 [doi>10.1109/ASE.2006.26]
• 24: Hyunsook Do , Sebastian Elbaum , Gregg Rothermel, Infrastructure Support for Controlled Experimentation with Software Testing and Regression Testing Techniques, Proceedings of the 2004 International Symposium on Empirical Software Engineering, p.60-70, August 19-20, 2004 [doi>10.1109/ISESE.2004.23]
• 25: Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004 [doi>10.1023/B:FORM.0000040028.49845.67]
• 26: Matthew B. Dwyer , Suzette Person , Sebastian Elbaum, Controlling factors in evaluating path-sensitive error detection techniques, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181787]
• 27: [27] S. Edelkamp, S. Leue, and A. Lluch-Lafuente. Partial-order reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology Transfer, 6(4), 2004.
• 28: Stefan Edelkamp , Alberto Lluch Lafuente , Stefan Leue, Directed explicit model checking with HSF-SPIN, Proceedings of the 8th international SPIN workshop on Model checking of software, p.57-79, May 2001, Toronto, Ontario, Canada
• 29: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 30: Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Thread-Modular Verification for Shared-Memory Programs, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.262-277, April 08-12, 2002
• 31: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 32: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 33: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 34: [34] C. Flanagan and S. Qadeer. Thread-modular model checking. In Proceedings of SPIN'03, pages 213-224, 2003.
• 35: [35] R. Floyd. Assigning meaning to programs. In Proceedings of the Symposium on Applied Mathematics, 1967.
• 36: P. G. Frankl , E. J. Weyuker, A Formal Analysis of the Fault-Detecting Ability of Testing Methods, IEEE Transactions on Software Engineering, v.19 n.3, p.202-213, March 1993 [doi>10.1109/32.221133]
• 37: Patrice Godefroid, Compositional dynamic test generation, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 38: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 39: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 40: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 41: [41] A. Groce and W. Visser. Heuristics for model checking java programs. Int'l. Journal on Software Tools for Tech. Transfer , 6(4):260-276, 2004.
• 42: Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , Sriram K. Rajamani, SYNERGY: a new algorithm for property checking, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181790]
• 43: [43] T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. pages 262-274, July 2003.
• 44: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 45: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 46: [46] G. Holzmann and D. Bosnacki. Multi-Core Model Checking with SPIN. In Proceedings of HIPS-TOPMoDRS, Long Beach, CA, 2007. IEEE.
• 47: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 48: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 49: [49] G. J. Holzmann and R. Joshi. Model-driven software verification. In Proceedings of SPIN'04, 2004.
• 50: Monica Hutchins , Herb Foster , Tarak Goradia , Thomas Ostrand, Experiments of the effectiveness of dataflow- and controlflow-based test adequacy criteria, Proceedings of the 16th international conference on Software engineering, p.191-200, May 16-21, 1994, Sorrento, Italy
• 51: [51] R. Iosif. Symmetry reductions for model checking of concurrent dynamic software. STTT, 6(4):302-319, 2004.
• 52: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 53: [53] C. B. Jones. Specification and Design of (Parallel) Programs. In Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 321-332. IFIP: North Holland, 1983.
• 54: Neil D. Jones , Flemming Nielson, Abstract interpretation: a semantics-based tool for program analysis, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995
• 55: [55] S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of TACAS'03, 2003.
• 56: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 57: Barbara A. Kitchenham , Shari Lawrence Pfleeger , Lesley M. Pickard , Peter W. Jones , David C. Hoaglin , Khaled El Emam , Jarrett Rosenberg, Preliminary guidelines for empirical research in software engineering, IEEE Transactions on Software Engineering, v.28 n.8, p.721-734, August 2002 [doi>10.1109/TSE.2002.1027796]
• 58: [58] G. T. Leavens, A. L. Baker, and C. Ruby. JML: a Java modeling language. In Formal Underpinnings of Java Workshop, Oct. 1998.
• 59: [59] A. Loginov, T. W. Reps, and S. Sagiv. Abstraction refinement via inductive learning. In Proceedings of CAV'05, pages 519-533, 2005.
• 60: Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 61: Madanlal Musuvathi , Dawson R. Engler, Model checking large network protocol implementations, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.12-12, March 29-31, 2004, San Francisco, California
• 62: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 63: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 64: [64] C. S. Pasareanu, R. Pelánek, and W. Visser. Concrete search with abstract matching and refinement. In Proceedings CAV'05, pages 52-66, 2005.
• 65: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 66: [66] Robby, E. Rodríguez, M. Dwyer, and J. Hatcliff. Checking Strong Specifications Using an Extensible Software Model Checking Framework. In Proceedings of TACAS'04, pages 404-420, 2004.
• 67: [67] E. Rodríguez, M. Dwyer, C. Flanagan, J. Hatcliff, G. T. Leavens, and Robby. Extending sequential specification techniques for modular specification and verification of multi-threaded programs. In Proceedings of ECOOP'05, pages 551-576, 2005.
• 68: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 69: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 70: [70] N. Sharygina, S. Chaki, E. Clarke, and N. Sinha. Dynamic Component Substitutability Analysis. In Proceedings of FM'05), volume 3582 of LNCS, pages 512-528, 2005.
• 71: Dag I. K. Sjoberg , Tore Dyba , Magne Jorgensen, The Future of Empirical Methods in Software Engineering Research, 2007 Future of Software Engineering, p.358-378, May 23-25, 2007 [doi>10.1109/FOSE.2007.30]
• 72: Mana Taghdiri , Robert Seater , Daniel Jackson, Lightweight extraction of syntactic specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181809]
• 73: Jianbin Tan , George S. Avrunin , Lori A. Clarke , Shlomo Zilberstein , Stefan Leue, Heuristic-guided counterexample search in FLAVERS, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 74: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001
• 75: Willem Visser , Corina S. Pǎsǎreanu , Radek Pelánek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146243]
• 76: [76] T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proceedings of TACAS'05, 2005.
• 77: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-40, January 2001, London, United Kingdom
• 78: Greta Yorsh , Thomas Ball , Mooly Sagiv, Testing, abstraction, theorem proving: better together!, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146255]
• 79: [79] http://pmd.sourceforge.net.
• 80: [80] http://www.satcompetition.org.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Verification