skip to main content
10.1145/1111542.1111551acmconferencesArticle/Chapter ViewAbstractPublication PagespepmConference Proceedingsconference-collections
Article

A dead variable analysis for explicit model checking

Published: 09 January 2006 Publication History

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]
T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Klaus Havelund, John Penix, and Willem Visser, editors, 7th International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 113--130. Springer, August 2000.]]
[2]
Marius Bozga, Jean-Claude Fernandez, and Lucian Ghirvu. State space reduction based on live variables analysis. In Agostino Cortesi and Gilberto Filé, editors, Static Analysis, 6th International Symposium, SAS '99, Venice, Italy, September 22--24, 1999, Proceedings, volume 1694 of Lecture Notes in Computer Science, pages 164--178. Springer, 1999.]]
[3]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic. ACM Trans. on Programming Languages and Systems, 8(2):244--263, April 1986.]]
[4]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Păsăreanu, R. Zheng, and H. Zheng. Bandera: extracting finite-state models from Java source code. In International Conference on Software Engineering, pages 439--448, 2000.]]
[5]
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages (POPL77), pages 238--252. ACM Press, 1977.]]
[6]
Yifei Dong and C. R. Ramakrishnan. An optimizing compiler for efficient model checking. In FORTE XII / PSTV XIX '99: 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), pages 241--256. Kluwer, B. V., 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]
G. J. Holzmann. The engineering of a model checker: the gnu i-protocol case study revisited. In Proc. of the 6th Spin Workshop, volume 1680 of Lecture Notes in Computer Science, Toulouse, France, 1999. Springer Verlag.]]
[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, M. B. Dwyer, and J. Hatcliff. Bogor: An extensible and highly-modular model checking framework. ACM SIGSOFT Software Engineering Notes, 28(5):267--276, September 2003.]]
[14]
N. Rungta and E. G. Mercer. A context-sensitive structural heuristic for guided search model checking. In 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, California, USA, November 2005.]]
[15]
D. A. Schmidt. Data flow analysis is model checking of abstract interpretations. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 38--48. ACM Press, 1998.]]
[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.]]

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PEPM '06: Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation
January 2006
176 pages
ISBN:1595931961
DOI:10.1145/1111542
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 January 2006

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

PEPM06
Sponsor:
PEPM06: Partial Evaluation and Program Manipulation 2006
January 9 - 10, 2006
South Carolina, Charleston

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)1
Reflects downloads up to 12 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2017)On partial state matchingFormal Aspects of Computing10.1007/s00165-016-0413-z29:5(777-803)Online publication date: 1-Sep-2017
  • (2016)Dead variable analysis for multi-threaded heap manipulating programsProceedings of the 31st Annual ACM Symposium on Applied Computing10.1145/2851613.2851826(1620-1627)Online publication date: 4-Apr-2016
  • (2011)On-The-Fly Path ReductionElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2011.07.003274(3-16)Online publication date: 1-Aug-2011
  • (2008)RWsetProceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1792734.1792770(351-366)Online publication date: 29-Mar-2008
  • (2008)Application of Static Analyses for State Space Reduction to Microcontroller Assembly CodeFormal Methods for Industrial Critical Systems10.1007/978-3-540-79707-4_4(21-37)Online publication date: 2008
  • (2008)RWset: Attacking Path Explosion in Constraint-Based Test GenerationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-540-78800-3_27(351-366)Online publication date: 2008
  • (2007)Application of static analyses for state space reduction to microcontroller assembly codeProceedings of the 12th international conference on Formal methods for industrial critical systems10.5555/1793603.1793609(21-37)Online publication date: 1-Jul-2007
  • (2007)On-the-fly dynamic dead variable analysisProceedings of the 14th international SPIN conference on Model checking software10.5555/1770532.1770545(113-130)Online publication date: 1-Jul-2007
  • (2007)On-the-Fly Dynamic Dead Variable AnalysisModel Checking Software10.1007/978-3-540-73370-6_9(113-130)Online publication date: 2007

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media