Verifying OpenJDK’s Sort Method for Generic Collections
Tóm tắt
Từ khóa
Tài liệu tham khảo
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P., Ulbrich, M. (eds.): Deductive Software Verification—The KeY Book: From Theory to Practice, LNCS, vol. 10001. Springer, Berlin (2016)
Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES ’12, pp. 145–154. ACM, New York (2012)
Akbarpour, B., Abdel-Hamid, A.T., Tahar, S., Harrison, J.: Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 53(4), 465–488 (2010)
Beckert, B., Klebanov, V.: Proof reuse for deductive program verification. In: Cuellar, J., Liu, Z. (eds.) Proceedings, Software Engineering and Formal Methods (SEFM). IEEE Press, Beijing (2004)
Beyer, D.: Software verification and verifiable witnesses (report on SV-COMP 2015). In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference TACAS, London, UK, LNCS, vol. 9035, pp. 401–416. Springer, Berlin (2015)
Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)
Breunesse, C.B.: On JML: Topics in tool-assisted verification of Java programs. Ph.D. Thesis, Radboud University of Nijmegen (2006)
Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013)
Filliâtre, J.C., Magaud, N.: Certification of sorting algorithms in the system Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends. Nice, France (1999). http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz
de Gouw, S., de Boer, F.S., Rot, J.: Proof pearl: the KeY to correct and stable sorting. J. Autom. Reason. 53(2), 129–139 (2014)
de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: The good, the bad and the worst case. In: Computer Aided Verification—27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, pp. 273–289 (2015)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., WernerDietl: JML Reference Manual (2013). http://www.eecs.ucf.edu/~leavens/JML//OldReleases/jmlrefman.pdf . Draft revision 2344
McIlroy, P.M.: Optimistic sorting and information theoretic complexity. In: Ramachandran, V. (ed.) Proceedings of the Fourth Annual ACM/SIGACT-SIAM Symposium on Discrete Algorithms, Austin, pp. 467–474. ACM/SIAM, Philadelphia (1993)
Mostowski, W.: Formalisation and verification of Java card security properties in dynamic logic. In: Cerioli, M. (ed.) Proceedings of Fundamental Approaches to Software Engineering (FASE), Edinburgh, LNCS, vol. 3442, pp. 357–371. Springer, Berlin (2005)
Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop in Connection with CADE-21, Bremen, Germany, CEUR Workshop Proceedings, vol. 259. CEUR-WS.org (2007)
Peters, T.: TimSort description. http://svn.python.org/projects/python/trunk/Objects/listsort.txt . Accessed Feb 2015
Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bjørner, N., de Boer, F.S. (eds.) Formal Methods, 20th International Symposium Oslo, Norway, LNCS, vol. 9109, pp. 414–434. Springer, Berlin (2015)
Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) Foundations of Software Technology and Theoretical Computer Science, 13th Conference, Bombay, India, LNCS, vol. 761, pp. 284–293. Springer, Berlin (1993)
Scheurer, D., Hähnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) Formal Methods and Software Engineering—18th International Conference on Formal Engineering Methods (ICFEM), Proceedings, LNCS, vol. 10009, pp. 57–73. Springer, Berlin (2016)
Sforza, F., Battú, L., Brunelli, M., Castelnuovo, A., Magnaghi, M.: A “design for verification” methodology. In: 2nd International Symposium on Quality of Electronic Design (ISQED), San Jose, CA, USA, pp. 50–55. IEEE Computer Society (2001)
Sternagel, C.: Proof Pearl: a mechanized proof of GHC’s mergesort. J. Autom. Reason. 51(4), 357–370 (2013)
Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: Autoproof: auto-active functional verification of object-oriented programs. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 566–580. Springer, New York (2015)