Abstract
The Toolkit for Accurate Scientific Software (TASS) is a suite of integrated tools for the formal verification of programs used in computational science, including numerically-intensive message-passing-based parallel programs. While TASS can verify a number of standard safety properties (such as absence of deadlocks and out-of-bound array indexing), its most powerful feature is the ability to establish that two programs are functionally equivalent. These properties are verified by performing an explicit state enumeration of a model of the program(s). In this model, symbolic expressions are used to represent the inputs and the values of variables. TASS uses novel techniques to simplify the symbolic representation of the state and to reduce the number of states explored and saved. The TASS front-end supports a large subset of C, including (multi-dimensional) arrays, structs, dynamically allocated data, pointers and pointer arithmetic, functions and recursion, and other commonly used language constructs. A number of experiments on small but realistic numerical programs show that TASS can scale to reasonably large configurations and process counts. TASS is open source software distributed under the GNU Public License. The Java source code, examples, experimental results, and reference materials are all available at http://vsl.cis.udel.edu/tass.
Similar content being viewed by others
References
Ayad., A., Marché, C.: Multi-prover verification of floating-point programs. In: Jürgen, G., Reiner, H. (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 6173, pp. 127–141, Springer, Berlin (2010)
Baier C., Katoen J.: Principles of Model Checking. The MIT Press, UK (2008)
Barrett, C., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.: TVOC: A translation validator for optimizing compilers. In: Kousha, E., Sriram, K.R. (eds.) Computer Aided Verification, Proceedings of 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, LNCS, vol. 3576, pp. 291–295, Springer (2005)
Barrett, C., Tinelli, C.: CVC3. In: Werner, D., Holger, H. (eds.) Proceedings of Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3–7, 2007, LNCS, vol. 4590, pp. 298–302, Springer (2007)
Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of 8th USENIX Symposium on Operating Systems Design and Implementation (2008)
Cappello, F., Hérault, T., Dongarra, J. (eds.): Recent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User’s Group Meeting, Paris, France, September 30–October 3, 2007, LNCS, vol. 4757, Springer (2007)
Clarke L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 215–222 (1976)
Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of floating-point and SIMD code. In: Proceedings of the sixth conference on Computer systems, EuroSys 2011, pp. 315–328, ACM, New York, NY, USA (2011)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE 2000: Proceedings of the 22nd International Conference on Software Engineering, pp. 439–448, ACM, New York, NY, USA (2000)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252, Los Angeles, California, 1977, ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, pp. 269–282, New York, NY, USA, ACM (1979)
Cousot P., Cousot R.: Abstract interpretation frameworks. J. Logic Comput. 2(4), 511–547 (1992)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyser. In: Mooly, S. (ed.) Proceedings of European Symposium on Programming (ESOP’05), LNCS, vol. 3444, pp. 21–30, Edinburgh, April 2–10, 2005. Springer (2005)
Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of fluctuat on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) Formal Methods for Industrial Critical Systems, LNCS, vol. 5825, pp. 53–69, Springer, Berlin (2009)
Deng, X., Lee, J., Robby.: Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 18–22 September 2006, Tokyo, Japan, pp. 157–166, IEEE Computer Society (2006)
Filliâtre, J-C, Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Werner, D., Holger, H. (eds.) CAV 2007, LNCS, vol. 4590, pp. 173–177, Springer (2007)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem, LNCS, vol. 1032, Springer (1996)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: SPIN 2003, vol. 2648, pp. 235–239 (2003)
Holzmann G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)
Iosif, R.: Exploiting heap symmetries in explicit-state model checking of software. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, ASE ’01, pp. 254–261, Washington, DC, USA, 2001. IEEE Computer Society (2001)
Kästner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Astrée: proving the absence of runtime errors. In: Embedded Real-Time Software and Systems (2010)
Khurshid, S., Pǎsǎreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of 9th International Conference, TACAS 2003, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7–11, 2003, LNCS, vol. 2619, pp. 553–568, Springer (2003)
King J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)
Lattner. C., et al.: The LLVM compiler infrastructure. http://llvm.org (2011)
Message Passing Interface Forum. MPI: A Message-Passing Interface Standard, version 2.2, September 4, 2009. http://www.mpi-forum.org/docs/ (2009)
Parnas D.L.: Designing software for ease of extension and contraction. IEEE Trans. Softw. Eng. 5, 128–138 (1979)
Parr, T.: ANTLR Parser Generator. http://www.antlr.org
Quinlan, D.J., et al.: ROSE. http://www.rosecompiler.org/ (2011)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly modular software model checking framework. In: ESEC/FSE-11: Proceedings of the 9th European Software Engineering Conference Held Jointly With the 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 267–276 (2003)
Robby, Dwyer, M.B., Hatcliff, J., Iosif, R.: Space-reduction strategies for model checking dynamic software. Electr. Notes Theor. Comput. Sci. 89(3) (2003)
Siegel, S.F.: Efficient verification of halting properties for MPI programs with wildcard receives. In: Cousot, R. (ed.) Verification, Model Checking, and Abstract Interpretation: Proceedings of 6th International Conference, VMCAI 2005, Paris, January 17–19, 2005, LNCS, vol. 3385, pp. 413–429 (2005)
Siegel, S.F.: Model checking nonblocking MPI programs. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation: Proceedings 8th International Conference, VMCAI 2007, Nice, France, January 14–16, 2007 LNCS, vol. 4349, pp. 44–58 (2007)
Siegel, S.F.: Verifying parallel programs with MPI-Spin. In: Cappello, F., Hérault, T., Dongarra, J. (eds.) Proceedings of Recent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User’s Group Meeting, Paris, France, September 30–October 3, 2007, pp. 13–14, LNCS, vol. 4757, Springer (2007)
Siegel, S.F., Avrunin, G.S.: Verification of halting properties for MPI programs using nonblocking operations. In: Cappello, F., Hérault, T., Dongarra, J. (eds.) Proceedings of Recent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User’s Group Meeting, Paris, France, September 30–October 3, 2007, pp. 326–334, LNCS, vol. 4757, Springer (2007)
Siegel S.F. et al.: The Toolkit for Accurate Scientific Software. http://vsl.cis.udel.edu/tass (2011)
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock, L.L., Mauro, P. (eds.) Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17–20, 2006, pp. 157–168, ACM (2006)
Siegel S.F., Mironova A., Avrunin G.S., Clarke L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM Trans. Softw. Eng. Methodol. 17(2), 1–34 (2008)
Siegel, S.F., Rossi, L.F.: Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In: Lastovetsky, A., Kechadi, T., Dongarra, J. (eds.) Proceedings of Recent Advances in Parallel Virtual Machine and Message Passing Interface, 15th European PVM/MPI User’s Group Meeting, LNCS, vol. 5205, Springer (2008)
Siegel, S.F., Zirkel, T.K.: A Functional Equivalence Verification Suite. http://vsl.cis.udel.edu/fevs
Siegel, S.F., Zirkel, T.K.: Automatic formal verification of MPI-based parallel programs (poster). In: Cascaval, C., Yew, P.-C. (eds.) The 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming (PPoPP), pp. 309–310, ACM (2011)
Siegel, S.F., Zirkel, T.K.: Collective assertions. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, LNCS, vol. 6538, pp. 387–402 (2011)
Vakkalanka, S., Sharma, S.V., Gopalakrishnan, G., Kirby, R.M.: ISP: a tool for model checking MPI programs. In: Principles and Practices of Parallel Programming (PPoPP), pp. 285–286 (2008)
Author information
Authors and Affiliations
Corresponding authors
Additional information
This material is based upon work supported by the National Science Foundation under Grants CCF-0733035 and CCF-0953210, and by the University of Delaware Research Foundation.
Rights and permissions
About this article
Cite this article
Siegel, S.F., Zirkel, T.K. TASS: The Toolkit for Accurate Scientific Software. Math.Comput.Sci. 5, 395–426 (2011). https://doi.org/10.1007/s11786-011-0100-7
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11786-011-0100-7
Keywords
Mathematics Subject Classification (2000)
- Primary 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
- Secondary 68Q60 Specification and verification (program logics, model checking, etc.)
- 68N19 Other programming techniques (object-oriented, sequential, concurrent, automatic, etc.)
- 65D99 Numerical analysis