A dead variable analysis for explicit model checking

ABSTRACT

Explicit state enumeration model checking for software is a kind of formal verification in which the reachable states of a software artifact are generated using an exhaustive search algorithm. The limiting factor in explicit software model checking is the size of the hash table of visited states used to avoid duplicate work and detect termination. The size of the hash table can be reduced by identifying and ignoring dead variables. We present a new kind of dead variable analysis that combines the usual static dead variable analysis with a specialized data flow analysis and an incomplete forward simulation to identify dead variables based on variable valuations at run time. The analysis is implemented in an explicit model checker for machine code programs on embedded processors. The analysis is most effective for code segments with pointers and nested conditional expressions in which disjoint sets of variables are used in each branch. Results for an ideal synthetic program are quite encouraging while results for three non-synthetic programs are more modest. The results suggest that the run-time portion of the analysis should only be performed on code segments which contain pointer dereferences and nested branches. Segments with these properties can be identified statically. The results also suggest that the analysis will result in a larger reduction using a specialized hash table.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 2: Marius Bozga , Jean-Claude Fernandez , Lucian Ghirvu, State Space Reduction Based on Live Variables Analysis, Proceedings of the 6th International Symposium on Static Analysis, p.164-178, September 22-24, 1999
• 3: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 4: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 5: 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]
• 6: Yifei Dong , C. R. Ramakrishnan, An Optimizing Compiler for Efficient Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.241-256, October 05-08, 1999
• 7: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In T. Ball and S. K. Rajamani, editors, Proceedings of the 10th International Workshop on Model Checking of Software (SPIN), volume 2648 of Lecture Notes in Computer Science, pages 235--239, Portland, OR, May 2003.
• 8: G. J. Holzmann. State compression in Spin. In Proceedings of the Third Spin Workshop, Twente University, The Netherlands, April 1997.
• 9: Gerard J. Holzmann, The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.232-244, September 21-24, 1999
• 10: Peter Leven, Tilman Mehler, and Stefan Edelkamp. Directed error detection in C++ with the assembley-level model checker StEAM. In Proceedings of 11th International SPIN Workshop, Barcelona, Spain, volume 2989 of Lecture Notes in Computer Science, pages 39--56. Springer, 2004.
• 11: M. Lewis. Interrupt handlers in dead variable analysis. Technical Report SMC-BYU-0105, Software Model Checking Laboratory, Brigham Young U., October 2005.
• 12: E. G. Mercer and M. Jones. Model checking machine code with the gnu debugger. In 12th International SPIN Workshop, pages 251--265, San Fancisco, USA, August 2005, Springer.
• 13: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
• 14: Neha Rungta , Eric G. Mercer, A context-sensitive structural heuristic for guided search model checking, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101982]
• 15: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 16: W. Visser, K. Havelund, G. Brat, and S. Park. Java PathFinder: Second generation of a Java model checker. In G. Gopalakrishnan, editor, Proceedings of the Workshop on Advances in Verification (WAVE'00), July 2000.

INDEX TERMS

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

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

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

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Design, Verification