FEVS: A Functional Equivalence Verification Suite for High-Performance Scientific Computing
Tóm tắt
Từ khóa
Tài liệu tham khảo
Andrews G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Boston (2000)
Barrett, C., Fang, Y., Benjamin, G., Hu, Y., Pnueli, A., Zuck, L.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, Proceedings of LNCS, vol. 3576, pp. 291–295. Springer, Berlin (2005)
Boldo S., Nguyen T.T.: Hardware-Independent Proofs of Numerical Programs. In: Muñoz, C. (eds) Proceedings of the Second NASA Formal Methods Symposium, pp. 14–23. Number NASA/CP-2010-216215 in NASA Conference Publication, Washington, D.C. (2010)
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)
Cousot P., Cousot R., Feret J., Mauborgne L., Miné A., Monniaux D., Rival X. : The ASTRÉE Analyser. In: Sagiv, M. (ed.) (eds) Proceedings of European Symposium on Programming (ESOP’05), LNCS, vol. 3444, pp. 21–30, Springer, Edinburgh (2005)
Emerson, E.A., Vineet, K.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic, Lecture Notes in Computer Science, vol. 3210, pp. 325–339. Springer, Berlin (2004)
Filliâtre J.-C., Marché C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds) CAV 2007, LNCS, vol. 4590, pp. 173–177, Springer, Berlin (2007)
Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: a simple abstract interpreter. In: European Symposium on Programming, LNCS, vol. 2305, pp. 209–212. Springer, Berlin (2002)
Gropp W., Lusk E., Skjellum A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge (1999)
Hatton L.: The T experiments: errors in scientific software. IEEE Comput. Sci. Eng. 4(2), 27–38 (1997)
Isaacson E., Keller H.B.: Analysis of Numerical Methods. John Wiley & Sons, New York (1966)
Krammer B., Müller M.S., Resch M.M.: MPI application development using the analysis tool MARMOT. In: Bubak, M., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds) International Conference on Computational Science, LNCS, vol. 3038, pp. 464–471, Springer, UK (2004)
Message Passing Interface Forum.: MPI: A Message-Passing Interface Standard, version 2.2, September 4, 2009. http://www.mpi-forum.org/docs/ (2009)
Post, D.E., Votta, L.G.: Computational science demands a new paradigm. Physics Today, pp. 35–41 (2005)
Quinn M.J.: Parallel Programming in C with MPI and OpenMP. McGraw-Hill, New York (2004)
Siegel, S.F.: Verifying parallel programs with MPI-Spin. In: 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, Proceedings of the Lecture Notes in Computer Science, vol. 4757, pp. 13–14. Springer, Berlin (2007)
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM TOSEM, vol. 17(2), pp. 1–34 (2008)
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)
Snir M., Otto S., Huss-Lederman S., Walker D., Dongarra J.: MPI—The Complete Reference, vol. 1: The MPI Core, 2nd edn. MIT Press, Berlin (1998)
Vakkalanka, S., Sharma, S.V., Ganesh, G., Kirby, R.M.: ISP: A tool for model checking MPI programs. In: Principles and Practices of Parallel Programming (PPoPP), pp. 285–286 (2008)
Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26–July, 2009, Proceedings of Lecture Notes in Computer Science, vol. 5643, pp. 599–613. Springer, Berlin (2009)