Abstract
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a host of logical and practical completeness and soundness issues. Interactive verification technology, on the other hand, is usually complete and sound, but requires a large amount of mathematical and practical expertise. Most programmers can be expected to use automatic, but not interactive, verification. The focus of this proposal is to integrate these two approaches into a single theoretical and practical framework, leveraging the benefits of each approach.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Breunesse, C.-B.: On JML: Topics in Tool-assisted Verification of Java Programs. PhD thesis, Radboud University Nijmegen (2006)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)
Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer’s Guide (2000)
Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (1999)
Cok, D.R., Kiniry, J.R.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), pp. 234–245 (2002)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Gosling, J., Joy, B., Steele, G.: The Java Language Specification, 1st edn. (August 1996)
Jacobs, B.: JavaCard program verification. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics TPHOL 2001, vol. 2151, pp. 1–3 (2001)
Jacobs, B.: Counting votes with formal methods. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 21–22. Springer, Heidelberg (2004)
Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 134–153. Springer, Heidelberg (2004)
Kiniry, J.R., Cok, D.R.: ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual. Department of Computer Science, Iowa State University, 226 Atanasoff Hall, draft revision 1.94 edition (2004)
The MOBIUS project. http://mobius.inria.fr/
Ranise, S., Deharbe, D.: Light-weight theorem proving for debugging and verifying units of code. In: International Conference on Software Engineering and Formal Methods SEFM 2003, Canberra, Australia (September 2003)
Rioux, F., Chalin, P.: Improving the quality of web-based enterprise applications with extended static checking: A case study. Electronic Notes in Theoretical Computer Science 157(2), 119–132 (2006)
RTI: Health, Social, and Economics Research, Research Triangle Park, NC. The economic impacts of inadequate infrastructure for software testing. Technical Report Planning Report 02-3, NIST (May 2002)
SMT-LIB: The satisfiability modulo theories library. http://goedel.cs.uiowa.edu/smtlib/
The Systems Research Group GForge. http://sort.ucd.ie/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kiniry, J.R., Chalin, P., Hurlin, C. (2008). Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)