Abstract
We discuss problems and barriers which stand in the way of producing verification tools that are robust, scalable and integrated in the software development cycle. Our analysis is that these barriers span a spectrum from theoretical, through practical and even logistical issues. Theoretical issues are the inherent complexity of program verification and the absence of a common, accepted semantic model in tools. Practical hurdles include the challenges arising from real-world systems features, such as floating-point arithmetic and weak memory. Logistical obstacles we identify are the lack of standard benchmarks to drive tool quality and efficiency, and the difficulty for academic research institutions of allocating resources to tool development. We propose simple measures which we, as a community, could adopt to make the design of serious verification tools easier and more credible. Our long-term vision is for the community to produce tools that are indispensable for a developer but so seamlessly integrated into a development environment, as to be invisible.
Supported by the Engineering and Physical Sciences Research Council (EPSRC) under grants no. EP/G051100/1 and EP/H017585/1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adve, S., Hill, M.: Weak Ordering – A New Definition. In: ISCA (1990)
Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Tech. Rep. 2000-14, Microsoft Research (February 2000)
Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: FMCAD, pp. 35–42. IEEE, Los Alamitos (2010)
Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119–122. Springer, Heidelberg (2010)
Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Principles of Programming Languages (POPL), pp. 1–3. ACM, New York (2002)
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Ball, T., Rajamani, S.K.: SLIC: a specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2001)
Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144–152. Springer, Heidelberg (2008)
Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), http://www.smt-lib.org
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: BLAST documentation, http://www.sosy-lab.org/~dbeyer/blast_doc/ (retrieved July 11, 2011)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. STTT 9(5-6), 505–525 (2007)
Beyer, D., Keremoglu, M.E.: cPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)
Biere, A.: Picosat essentials. JSAT 4(2-4), 75–97 (2008)
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers (2003)
Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD, pp. 69–76. IEEE, Los Alamitos (2009)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Information and Computation (1992)
Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM) (2003)
Clarke, E., Kröning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD), 105–127 (2004)
Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys. ACM, New York (2011)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289–300 (2009)
Satisfiability: Suggested Format (1993), ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/
Donaldson, A., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351–368. Springer, Heidelberg (2011)
Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356–371. Springer, Heidelberg (2011)
Donaldson, A.F., Kroening, D., Ruemmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods in System Design 39(1), 83–113 (2011)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Fraser, K., Harris, T.: Concurrent Programming Without Locks. ACM Trans. Comput. Syst. 25(2) (2007)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Hoare, C., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: A manifesto. ACM Comput. Surv. 41, article 22 (October 2009)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279–295 (1997)
Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)
Kurshan, R.P.: Verification technology transfer. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 46–64. Springer, Heidelberg (2008)
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput. 46(7), 779–782 (1979)
Manolescu, I., Manegold, S.: Performance evaluation and experimental assessment – conscience or curse of database research? In: VLDB, pp. 1441–1442. ACM, New York (2007)
McKenney, P.: http://www.rdrop.com/users/paulmck/RCU/
Post, H., Sinz, C., Merz, F., Gorges, T., Kropf, T.: Linking functional requirements and software verification. In: RE, pp. 295–302. IEEE Computer Society, Los Alamitos (2009)
Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT) (2010)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Steffen, B.: Major threat: From formal methods without tools to tools without formal methods. In: ICECCS, p. 15. IEEE Computer Society, Los Alamitos (2004), panel discussion
Veldhuizen, T.L.: C++ templates are Turing complete. Tech. rep. (2003), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.3670 (retrieved July 11, 2011)
Wilson, M.L., Mackay, W., Chi, E., Bernstein, M., Russell, D., Thimbleby, H.: RepliCHI – CHI should be replicating and validating results more: discuss. In: CHI Extended Abstracts, pp. 463–466. ACM, New York (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M. (2011). Making Software Verification Tools Really Work. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)