Abstract
The correctness of software verification systems is vital, since they are used to confirm that safety and security critical software systems satisfy their requirements. Modern verification systems need to understand their target software, which can be done by using an axiomatization base. It captures the semantics of the programming language used for writing the target software. To ensure their correctness, it is necessary to validate both parts: the implementation and the axiomatization base. As a result, it is essential to increase the axiom coverage in order to verify its correctness. However, creating test cases manually is a time consuming and difficult task even for verification engineers. We present a beam search approach to automatically generate test cases by modifying existing test cases as well as a comparison between axiomatization and code coverage. Our results show that the overall coverage of the existing test suite can be improved by more than 20 %. In addition, our approach explores the search space more efficiently than existing ones.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
“Used” does not imply that the application of the axiom was necessary.
- 2.
“Equivalence” is not strictly logical here, but regarding the tool’s capability to find a proof in a different way.
- 3.
The full code and the logfiles are available online http://cs.adelaide.edu.au/~optlog/research/software.php.
- 4.
www.emma.sourceforge.net (last accessed: 5 April 2015).
References
Back, T., Fogel, D.B., Michalewicz, Z.: Handbook of evolutionary computation. IOP Publishing Ltd., (1997)
Barthe, G., et al.: MOBIUS: mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 10–29. Springer, Heidelberg (2007)
Beckert, B., Klebanov, V.: Must program verification systems and calculi be verified? In: Verification Workshop (VERIFY), Workshop at Federated Logic Conferences (FLoC), pp. 34–41 (2006)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)
Beckert, B., Bormer, T., Wagner, M.: Heuristically creating test cases for program verification systems. In: Metaheuristics International Conference (MIC) (2013)
Beckert, B., Bormer, T., Wagner, M.: A metric for testing program verification systems. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 56–75. Springer, Heidelberg (2013)
Bérard, B., Bidoit, B., Finkel, M., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-checking Techniques and Tools. Springer, Heidelberg (2010)
Blum, C., Blesa, M.J.: Probabilistic beam search for the longest common subsequence problem. In: Stützle, T., Birattari, M., H. Hoos, H. (eds.) SLS 2007. LNCS, vol. 4638, pp. 150–161. Springer, Heidelberg (2007)
Bokhari, M., Wagner, M.: Improving test coverage of formal verification systems via beam search. In: Companion of the 2015 Conference on Genetic and Evolutionary Computation, GECCO 2015. ACM (2015) (to be published)
Bormer, T., Wagner, M.: Towards testing a verifying compiler. In: International Conference on Formal Verification of Object-Oriented Software (FoVeOOS) Pre-Proceedings, pp. 98–112. Karlsruhe Institute of Technology (2010)
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453–457 (1975)
Dorigo, M., Birattari, M., Stutzle, T.: Ant colony optimization. IEEE Comput. Intell. Mag. 1, 28–39 (2006)
Filliâtre, J.-C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Jacobs, B., Poll, E.: Java program verification at nijmegen: developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 134–153. Springer, Heidelberg (2004)
Kuhn, D.R., Wallace, D.R., Gallo, A.M.: Software fault interactions and implications for software testing. IEEE Trans. Softw. Eng. 30, 418–421 (2004)
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurrency Comput. Pract. Experience 13, 1173–1214 (2001)
Wagner, M.: Maximising axiomatization coverage and minimizing regression testing time. In: IEEE Congress on Evolutionary Computation (CEC), pp. 2885–2892 (2014)
Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. 29, 366–427 (1997)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bokhari, M.A., Bormer, T., Wagner, M. (2015). An Improved Beam-Search for the Test Case Generation for Formal Verification Systems. In: Barros, M., Labiche, Y. (eds) Search-Based Software Engineering. SSBSE 2015. Lecture Notes in Computer Science(), vol 9275. Springer, Cham. https://doi.org/10.1007/978-3-319-22183-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-22183-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22182-3
Online ISBN: 978-3-319-22183-0
eBook Packages: Computer ScienceComputer Science (R0)