Using the static verification tools for checking the ScopeShell system
Keywords:
static verification, detecting bugs in software, automated code analysis, Java programming languageAbstract
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.
References
- Gnuplot (http://www.gnuplot.info/).
- Hovemeyer D., Pugh W. Finding bugs is easy // ACM Sigplan Notices. 2004. 39. 92-106.
- FindBugs (http://findbugs.sourceforge.net).
- BCEL (http://jakarta.apache.org/bcel).
- PMD/Java (http://pmd.sourceforge.net).
- Lint4j (http://www.jutils.com).
- JLint (http://artho.com/jlint).
- Artho C. Finding faults in multi-threaded programs. Master’s Th. Institute of Computer Systems, Federal Institute of Technology. Zürich/Austin, 2001.
- 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.
- 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.
- 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.
- Hammurapi (http://www.hammurapi.biz).
- QJ-Pro (http://qjpro.sourceforge.net).
- Clarkware Consulting (http://www.clarkware.com).
- Condenser (http://condenser.sourceforge.net).
- Dependency Finder (http://depfind.sourceforge.net).
- UCDetector (http://www.ucdetector.org).
- Jackson D. Micromodels of software: modelling and analysis with Alloy (http://sdg.lcs.mit.edu/alloy/book.pdf).
- Alloy (http://alloy.mit.edu).
- Jackson D., Schechter I., Shlyakhter I. ALCOA: The Alloy constraint analyzer // Proc. of the 22nd Int. Conf. on Software Engineering. Limerick, 2000. 730-733.
Downloads
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