Complete formal verification of software remains extremely expensive and often reserved in practice for the most critical products. Test generation techniques are much less costly and can be used in combination with theorem proving tools to provide high confidence in the software correctness at an acceptable cost when an automatic prover does not succeed alone. This short paper presents a case study on verification of a cloud hypervisor with the Frama-C toolset, in which deductive verification has been advantageously combined with structural all-path testing. We describe our combined verification approach, present the adopted methodology and emphasize its benefits and limitations. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Kosmatov, N., Lemerre, M., & Alec, C. (2014). A case study on verification of a cloud hypervisor by proof and structural testing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8570 LNCS, pp. 158–164). Springer Verlag. https://doi.org/10.1007/978-3-319-09099-3_12
Mendeley helps you to discover research relevant for your work.