Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification

  • Shaoying LiuEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


Verifying a specification for software can be converted into theorem proving. In this paper, we describe a testing-based formal verification (TBFV) method for automatically testing theorems. The advantage of the method over conventional theorem proving is that it can quickly detect faults if the theorem is not valid and quickly provide us with confidence in the validity of the theorem if it is valid. We discuss the principle and algorithms for test case generation in TBFV and present an example to illustrate how TBFV can be applied in checking designs. We also present a prototype supporting tool we have developed and a controlled experiment for evaluating the performance of TBFV. The result shows that TBFV is effective and efficient to find faults in certain setting.


Boolean Function Free Variable Formal Proof Disjunctive Normal Form Test Case Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



I would like to thank my students Mo Li, Hayato Ikeda, and Ye Yan for their contributions in developing the supporting tool for the TBFV method proposed in this paper. Hayato Ikeda’s work on the tool is particularly appreciated.


  1. 1.
    Dillinger, P.C., Manolios, P., Vroon, D., Moore, J.S.: The ACL2 Sedan. In: Proceedings of 7th Workshop on User Interfaces for Theorem Provers (UITP 2006). Electronic Notes in Theoretical Computer Science, pp. 3–18. Elsevier, 15 May 2007Google Scholar
  2. 2.
    Owre, S., Rushby, J., Shankar, N., Henke, F.V.: Formal verification for fault-tolerant architetures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107–125 (1995)CrossRefGoogle Scholar
  3. 3.
    Leavens, T., Rustand, K., Leino, M., Muller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19, 159–189 (2007)CrossRefzbMATHGoogle Scholar
  4. 4.
    Liu, S.: Formal Engineering for Industrial Software Development Using the SOFL Method. Springer, Heidelberg (2004). ISBN: 3-540-20602-7CrossRefzbMATHGoogle Scholar
  5. 5.
    Liu, S., Nakajima, S.: A decompositional approach to automatic test case generation based on formal specifications. In: 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010), Singapore, 9–11 June 2010, pp. 147–155 (2010)Google Scholar
  6. 6.
    Manthey, N.: Solver Description of RISS 2.0 and PRISS 2.0, KRR Teport 12–02, Knowledge Representation and Reasoning, Technical University Dresden (2012)Google Scholar
  7. 7.
    Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014)Google Scholar
  8. 8.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Beizer, B.: Black-Box Testing. Wiley, New York (1995)Google Scholar
  10. 10.
    Liu, S., McDermid, J.A., Chen, Y.: A rigorous method for inspection of model-based formal specifications. IEEE Trans. Reliab. 59(4), 667–684 (2010)CrossRefGoogle Scholar
  11. 11.
    Kuhn, D.R.: Fault classes and error detection capability of specification-based testing. ACM Trans. Softw. Eng. Methodol. 8(4), 411–424 (1999)CrossRefGoogle Scholar
  12. 12.
    Chamarthi, H.R., Manolios, P.: Automated specification analysis using an interactive theorem prover. In: Formal Methods in Computer-Aided Design (FMCAD 2011), 30 October–2 November 2011, pp. 46–53. IEEE Press (2011)Google Scholar
  13. 13.
    Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 188–203. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Bertot, Y., Castern, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)Google Scholar
  15. 15.
    Paraskevopoulou, Z., Hirtcu, C., Denes, M., Lamproulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) ITP. LNCS, vol. 9236, pp. 325–343. Springer, Heidelberg (2015)Google Scholar
  16. 16.
    Bulwahn, L.: The new quickcheck for isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  17. 17.
    Hähnle, R., Wallenburg, A.: Using a software testing technique to improve theorem proving. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 30–41. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Chamarthi, H.R., Dillinger, P.C., Kaufmann, M.: Integrating testing and interactive theorem proving. In: Proceedings of 10th International Workshop on the ACL2 Theorem Prover and Its Applications (EPTCS 70), 3–4 November 2011, pp. 4–19 (2011)Google Scholar
  19. 19.
    Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)Google Scholar
  20. 20.
    Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Larsen, P.G., Wing, J.M. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993)Google Scholar
  21. 21.
    Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 21–40. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Helke, S., Neustupny, T., Santen, T.: Automating test case generation from Z specifications with Isabelle. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 52–71. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  23. 23.
    Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)CrossRefGoogle Scholar
  24. 24.
    Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 272–286. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  25. 25.
    Aichernig, B.K., Salas, P.A.P.: Test case generation by OCL mutation and constraint solving. In: Cai, K.-Y., Ohnishi, A. (eds.) Proceedings of Fifth International Conference on Quality Software (QSIC 2005), Melbourne, Australia, 19–21 September 2005, pp. 64–71. IEEE CS Press (2005)Google Scholar
  26. 26.
    Aichernig, B.K.: Model-based mutation testing of reactive systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 23–36. Springer, Heidelberg (2013)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Computer ScienceHosei UniversityTokyoJapan

Personalised recommendations