Using the static verification tools for checking the ScopeShell system

Authors

  • S.V. Stepanov Lomonosov Moscow State University
  • A.G. Shishkin Lomonosov Moscow State University

Keywords:

static verification, detecting bugs in software, automated code analysis, Java programming language

Abstract

Freeware static verification tools for Java code analysis are considered. Test results and an estimate for the efficiency of different tools for checking the ScopeShell system developed at the Department of Research Automation (Faculty of Computational Mathematics and Cybernetics, Moscow State University) are given.

Author Biographies

S.V. Stepanov

A.G. Shishkin

References

  1. Gnuplot (http://www.gnuplot.info/).
  2. Hovemeyer D., Pugh W. Finding bugs is easy // ACM Sigplan Notices. 2004. 39. 92-106.
  3. FindBugs (http://findbugs.sourceforge.net).
  4. BCEL (http://jakarta.apache.org/bcel).
  5. PMD/Java (http://pmd.sourceforge.net).
  6. Lint4j (http://www.jutils.com).
  7. JLint (http://artho.com/jlint).
  8. Artho C. Finding faults in multi-threaded programs. Master’s Th. Institute of Computer Systems, Federal Institute of Technology. Zürich/Austin, 2001.
  9. Flanagan C., Leino K.R. M., Lillibridge N.M. G., Saxe J.B., Stata R. Extended static checking for Java // Proc. of the 2002 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Berlin, 2002. 234-245.
  10. Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Leino K.R. M., Poll E. An overview of JML tools and applications // Int. J. on Software Tools for Technology Transfer. 2005. 7, N 3. 212-232.
  11. Leavens G.T., Leino K.R. M., Poll E., Ruby C., Jacobs B. JML: Notations and tools supporting detailed design in Java // OOPSLA’00 Companion. Minneapolis, 2000. 105-106.
  12. Hammurapi (http://www.hammurapi.biz).
  13. QJ-Pro (http://qjpro.sourceforge.net).
  14. Clarkware Consulting (http://www.clarkware.com).
  15. Condenser (http://condenser.sourceforge.net).
  16. Dependency Finder (http://depfind.sourceforge.net).
  17. UCDetector (http://www.ucdetector.org).
  18. Jackson D. Micromodels of software: modelling and analysis with Alloy (http://sdg.lcs.mit.edu/alloy/book.pdf).
  19. Alloy (http://alloy.mit.edu).
  20. Jackson D., Schechter I., Shlyakhter I. ALCOA: The Alloy constraint analyzer // Proc. of the 22nd Int. Conf. on Software Engineering. Limerick, 2000. 730-733.

Published

14-01-2009

How to Cite

Степанов С., Шишкин А. Using the Static Verification Tools for Checking the ScopeShell System // Numerical Methods and Programming (Vychislitel’nye Metody i Programmirovanie). 2009. 10. 22-33

Issue

Section

Section 2. Programming