Abstract
Currently, static verifiers based on counterexample-guided abstraction refinement (CEGAR) can prove correctness of a program against a specified requirement, find its violation in a program, and stop analysis or exhaust the given resources without producing any useful result. Theoretically, we could use this approach for checking several requirements at once; however, finding of the first violation of some requirement or exhausting resources for some requirement will prevent from checking the program against other requirements. Moreover, if the program contains more than one violation of the requirement, CEGAR will find only the very first violation and may miss potential errors in the program. At the same time, static verifiers perform similar actions during checking of the same program against different requirements, which results in waste of a lot of resources. This paper presents a new CEGAR-based method for software static verification, which is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR checking requirements one by one. To achieve this goal, the suggested method distributes resources over requirements and continues analysis after finding a violation of a requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by five times. The total number of divergent results in comparison with the base CEGAR was about 2%. Having continued the analysis after finding the first violation, this method guarantees that all violations of given requirements are found in 40% of cases, with the number of violations found being 1.5 times greater than in that in the base CEGAR approach.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Beyer, D., Competition on software verification, Lect. Notes Comput. Sci., 2012, vol. 7214, pp. 504–524. http://dxdoiorg/. doi 10.1007/978-3-642-28756-5_38
Beyer, D., Software verification and verifiable witnesses, Lect. Notes Comput. Sci., 2015, vol. 9035, pp. 401–416. http://dxdoiorg/. doi 10.1007/978-3- 662-46681-0_31
Khoroshilov, A., Mutilin, V., Novikov, E., et al., Towards an open framework for C verification tools benchmarking, Lect. Notes Comput. Sci., 2012, vol. 7162, pp. 179–192. http://dxdoiorg/. doi 10.1007 /978-3-642-29709-0_17
List of errors revealed in Linux Kernel modules by means of the LDV Tools system. http://linuxtestingorg /results/ldv.
Shved, P., Mandrykin, M., and Mutilin, V., Predicate analysis with BLAST 2.7, Lect. Notes Comput. Sci., 2012, vol. 7214, pp. 525–527. http://dxdoiorg/. doi 10.1007/978-3-642-28756-5_39
Beyer, D., Henzinger, T.A., Jhala, R., and Majumdar, R., The software model checker BLAST, Int. J. Software Tools Technology Transfer, 2007, vol. 9, nos. 5–6, pp. 505–525. http://dxdoiorg/doi10.1007/s10009-007-0044-z
Beyer, D. and Keremoglu, M.E., Cpachecker: A tool for configurable software verification // computer aided verification, Lect. Notes Comput. Sci., 2011, vol. 6806, pp. 184–190. http://dxdoiorg/ doi 10.1007/ 978-3-642-22110-1_16.10.1007/978-3-642-22110-1_16
Beyer, D. and Wendler, P., Reuse of verification results: Conditional model checking, precision reuse, and verification witnesses, Lect. Notes Comput. Sci., 2013, vol. 7976, pp. 1–17. http://sv-compsosy-laborg/.
Beyer, D., Keremoglu, M.E., and Wendler, P., Predicate abstraction with adjustable-block encoding, in Formal Methods in Computer-Aided Design, 2010.
Beyer, D. and Löwe, S., Explicit-state software model checking based on CEGAR and interpolation, Lect. Notes Comput. Sci., 2013, vol. 7793, pp. 146–162.
Clarke, E.M., Grumberg, O., Jha, S., et al., Counterexample- guided abstraction refinement, Lect. Notes Comput. Sci., 2000, vol. 185 5, pp. 154–169.
Mandrykin, M.U., Mutilin, V.S., and Khoroshilov, A.V., Introduction to CEGAR: Counterexample-guided abstraction refinement, Tr. Inst. Sistemnogo Program. Ross. Akad. Nauk, 2013, vol. 24, pp. 219–292.
Novikov, E.M., An approach to implementation of aspect-oriented programming for C, Program. Comput. Software, 2013, vol. 39, no. 4, pp. 194–206. http://dx. doiorg/. doi 10.1134/S0361768813040051
Beyer, D., Löwe, S., Novikov, E., et al., Precision reuse for efficient regression verification, Proc. of the 9th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on Foundations of Software Engineering, St. Petersburg, Russia, 2013.
Beyer, D., Henzinger, T.A., Keremoglu, M.E., and Wendler, P., A technique to Pass Information between Verifiers, Proc. of the 20th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering, Cary, NC, 2012.
Mordan, V. and Novikov, E., Minimizing the number of static verifier traces to reduce time for finding bugs in linux kernel modules, Proc. of the Spring/Summer Young Researchers’ Colloquium on Software Engineering, 2014, vol. 8.
Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., et al., Configurable toolset for static verification of operating systems kernel modules, Program. Comput. Software, 2015, vol. 41, no. 1, pp. 49–64.
Author information
Authors and Affiliations
Corresponding author
Additional information
Original Russian Text © V.O. Mordan, V.S. Mutilin, 2016, published in Programmirovanie, 2016, Vol. 42, No. 4.
Rights and permissions
About this article
Cite this article
Mordan, V.O., Mutilin, V.S. Checking several requirements at once by CEGAR. Program Comput Soft 42, 225–238 (2016). https://doi.org/10.1134/S0361768816040058
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S0361768816040058