Automated Test Generation and Verified Software

1. Hayhurst, K.J., Veerhusen, D.S., Chilenski, J.J., Rierson, L.K.: A practical tutorial on modified condition/decision coverage. NASA Technical Memorandum TM-2001-210876, NASA Langley Research Center, Hampton, VA (2001), http://www.faa.gov/certification/aircraft/av-info/software/Research/MCDC%20Tutorial.pdf

2. Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, pp. 146–162. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

3. Hamon, G., de Moura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM), pp. 261–270. IEEE Computer Society, Beijing (2004)

   Google Scholar 

4. Saïdi, H., Graf, S.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

   Chapter  Google Scholar 

5. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

6. Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: [48], pp. 67–81

   Google Scholar 

7. Xia, S., Di Vito, B., Muñoz, C.: Predicate abstraction of programs with non-linear computation. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 352–368. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

8. Boppana, V., Rajan, S.P., Takayama, K., Fujita, M.: Model checking based on sequential ATPG. In: [49], pp. 418–430

   Google Scholar 

9. Ho, P.H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal simulation engines. In: International Conference on Computer Aided Design (ICCAD), Jan Jose, CA, Association for Computing Machinery, pp. 120–126 (2000)

   Google Scholar 

10. Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Conference on Programming Language Design and Implementation: PLDI, Chicago, IL. Association for Computing Machinery, pp. 213–223 (2005)

    Google Scholar 

11. Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability modulo theories competition. In: [48], pp. 20–23.

    Google Scholar 

12. de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

13. Bernot, G., Gaudel, M.C., Marre, B.: Software testing based on formal specifications: A theory and a tool. IEE/BCS Software Engineering Journal 6, 387–405 (1991)

    Article  Google Scholar 

14. Gaudel, M.C.: Testing from formal specifications, a generic approach. In: Strohmeier, A., Craeynest, D. (eds.) Ada-Europe 2001. LNCS, vol. 2043, pp. 35–48. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

15. Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy. Association for Computing Machinery, pp. 123–122 (2002)

    Google Scholar 

16. Jéron, T., Morel, P.: Test generation derived from model-checking. In: [49], pp. 108–121

    Google Scholar 

17. Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: Proceedings of the 13th Annual Symposium on Foundations of Software Engineering (FSE), Lisbon, Portugal. Association for Computing Machinery, pp. 273–282 (2005)

    Google Scholar 

18. Tiwari, A.: Abstractions for hybrid systems. In: Formal Methods in Systems Design (to appear, 2007), http://www.csl.sri.com/~tiwari/new.pdf

19. Ben-David, S., Gringauze, A., Sterin, B., Wolfsthal, Y.: PathFinder: A tool for design exploration. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 510–514. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

20. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: International Conference on Functional Programming, Montreal, Canada. Association for Computing Machinery, pp. 268–279 (2000)

    Google Scholar 

21. Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: 2nd International Conference on Software Engineering and Formal Methods, Beijing, China, pp. 230–239. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

22. Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM), Seattle, WA (2006), http://fm.csl.sri.com/AFM06/papers/5-Owre.pdf

23. Sullivan, K., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: International Symposium on Software Testing and Analysis (ISSTA), Boston, MA. Association for Computing Machinery, pp. 133–142 (2004)

    Google Scholar 

24. Beck, K.: Test Driven Development: By Example. Addison-Wesley, Reading (2002)

    Google Scholar 

25. Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 332–358. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

26. Kosmatov, N., Legeard, B., Peureux, F., Utting, M.: Boundary coverage criteria for test generation from formal models. In: 15th International Symposium on Software Reliability Engineering (ISSRE 2004), Saint-Malo, France, pp. 139–150. IEEE Computer Society, Los Alamitos (2004)

    Chapter  Google Scholar 

27. Weyuker, E., Goradia, T., Singh, A.: Automatically generating test data from a Boolean specification. IEEE Transactions on Software Engineering 20, 353–363 (1994)

    Article  MATH  Google Scholar 

28. Kuhn, D.R.: Fault classes and error detection capability of specification-based testing. ACM Transactions on Software Engineering and Methodology 8, 411–424 (1999)

    Article  Google Scholar 

29. Tsuchiya, T., Kikuno, T.: On fault classes and error detection capability of specification-based testing. ACM Transactions on Software Engineering and Methodology 11, 58–62 (2002)

    Article  Google Scholar 

30. Okun, V., Black, P.E., Yesha, Y.: Comparison of fault classes in specification-based testing. Information and Software Technology 46, 525–533 (2004)

    Article  Google Scholar 

31. Utting, M., Legeard, B.: Practical Model-Based Testing. Morgan Kaufmann, San Francisco (2006)

    Google Scholar 

32. Clarke, D., Jéron, T., Rusu, V., Zinovieva, E.: STG: a symbolic test generation tool. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 470–475. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

33. Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy. Association for Computing Machinery, pp. 112–122 (2002)

    Google Scholar 

34. du Bosquet, L., Ouabdesselam, F., Richier, J.L., Zuanon, N.: Lutess: A specification-driven testing environment for synchronous software. In: 21st International Conference on Software Engineering, pp. 267–276. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

35. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines. Proceedings of the IEEE 84, 1090–1123 (1996)

    Article  Google Scholar 

36. Whalen, M.W., Rajan, A., Heimdahl, M.P.E., Miller, S.P.: Coverage metrics for requirements-based testing. In: International Symposium on Software Testing and Analysis (ISSTA), Portland, ME. Association for Computing Machinery, pp. 25–36 (2006)

    Google Scholar 

37. Heimdahl, M.P., George, D., Weber, R.: Specification test coverage adequacy criteria = specification test generation Inadequacy criteria? In: High-Assurance Systems Engineering Symposium, Tampa, FL, pp. 178–186. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

38. Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR 1999: 7^th European Int. Conference on Software Testing, Analysis & Review. EuroStar Conferences, Barcelona, Spain, Galway, Ireland (1999)

    Google Scholar 

39. Bozga, M., Fernandez, J.C., Ghirvu, L.: Using static analysis to improve automatic test generatin. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 235–250. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

40. Rusu, V.: Verification using test generation techniques. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 252–271. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

41. Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proceedings of the 14th Annual Symposium on Foundations of Software Engineering (FSE), Portland, OR. Association for Computing Machinery, pp. 117–127 (2006)

    Google Scholar 

42. Duprat, S., Souyris, J., Favre-Felix, D.: Formal verification workbench for Airbus avionics software. In: ERTS 2006: Embedded Real Time Software, Societe des Ingenieurs de l’Automobile (2006)

    Google Scholar 

43. Hamon, G., de Moura, L., Rushby, J.: Automated test generation with SAL. Technical note, Computer Science Laboratory, SRI International, Menlo Park, CA (2005), http://www.csl.sri.com/users/rushby/abstracts/sal-atg

44. de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N.: Integrating verification components. In: These proceedings (2007)

    Google Scholar 

45. Bloomfield, R., Littlewood, B.: Multi-legged arguments: The impact of diversity upon confidence in dependability arguments. In: The International Conference on Dependable Systems and Networks, pp. 25–34. IEEE Computer Society, San Francisco (2003)

    Google Scholar 

46. Littlewood, B., Wright, D.: The use of multi-legged arguments to increase confidence in safety claims for software-based systems: a study based on a BBN analysis of an idealised example. IEEE Transactions on Software Engineering 33, 347–365 (2007)

    Article  Google Scholar 

47. Rushby, J.: What use is verified software? In: 12th IEEE International Conference on the Engineering of Complex Computer Systems (ICECCS), Auckland, New Zealand, IEEE Computer Society, Los Alamitos (2007), http://www.csl.sri.com/~rushby/abstracts/iceccs07-vsi

    Google Scholar 

48. Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol. 3576. Springer, Heidelberg (2005)

    MATH  Google Scholar 

49. Halbwachs, N., Peled, D.A. (eds.): CAV 1999. LNCS, vol. 1633. Springer, Heidelberg (1999)

    MATH  Google Scholar 

Download references