Name
Abstract | ||
|---|---|---|
VCC is an industrial-strength verification environment for low-level concurrent system code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. It includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs. This paper motivates VCC, describes our verification methodology, describes the architecture of VCC, and reports on our experience using VCC to verify the Microsoft Hyper-V hypervisor. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-03359-9_2 | TPHOLs |
Keywords | Field | DocType |
partial counterexample execution,industrial-strength verification environment,c. vcc,practical system,function contract,state assertion,low-level concurrent system code,concurrent c.,failed proof,verification methodology,microsoft hyper-v hypervisor,proof attempt | Architecture,Separation logic,Computer science,Page table,Correctness,Hypervisor,Theoretical computer science,Mathematical proof,Invariant (mathematics),Counterexample | Conference |
Volume | ISSN | Citations |
5674 | 0302-9743 | 242 |
PageRank | References | Authors |
7.99 | 24 | 8 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ernie Cohen | 1 | 661 | 33.40 |
| Markus Dahlweid | 2 | 370 | 13.01 |
| Mark Hillebrand | 3 | 365 | 16.45 |
| Dirk Leinenbach | 4 | 534 | 27.36 |
| Michał Moskal | 5 | 360 | 15.83 |
| Thomas Santen | 6 | 588 | 26.33 |
| Wolfram Schulte | 7 | 2342 | 153.40 |
| Stephan Tobies | 8 | 1599 | 158.86 |