Skip to Main content Skip to Navigation
Conference papers

A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01822965
Contributor : Bruno Savelli <>
Submitted on : Monday, June 25, 2018 - 4:03:16 PM
Last modification on : Wednesday, September 16, 2020 - 5:01:33 PM
Long-term archiving on: : Wednesday, September 26, 2018 - 2:14:43 PM

File

latap2014.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01822965, version 1

Collections

CEA | CNRS | DRT | UMR8623 | LIST

Citation

Nikolai Kosmatov, Matthieu Lemerre, Céline Alec. A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. TAP 2014: International Conference on Tests and Proofs, Jul 2014, York, United Kingdom. pp.158-164. ⟨cea-01822965⟩

Share

Metrics

Record views

156

Files downloads

179