Using the static verification tools for checking the ScopeShell system

Authors

  • S.V. Stepanov
  • A.G. Shishkin

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.

New computational technologies

Downloads

Published

2009-01-14

Issue

Vol. 10 (2009): Issue 1.

Section

Section 2. Programming

Author Biographies

S.V. Stepanov

Lomonosov Moscow State University,
Faculty of Computational Mathematics and Cybernetics
• Student

A.G. Shishkin

Lomonosov Moscow State University,
Faculty of Computational Mathematics and Cybernetics
• Senior Researcher

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.