Name
Title | ||
|---|---|---|
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems |
Abstract | ||
|---|---|---|
A major challenge for verifying completesoftware systems is their complexity. A complete software system consists of program modules that use many language features and span different abstraction levels (e.g. user code and run-time system code). It is extremely difficult to use one verification system (e.g. type system or Hoare-style program logic) to support all these features and abstraction levels. In our previous work, we have developed a new methodology to solve this problem. We apply specialized "domain-specific" verification systems to verify individual program modules and then link the modules in a foundational open logical framework to compose the verified complete software package. In this paper, we show how this new methodology is applied to verify a software package containing implementations of preemptive threads and a set of synchronization primitives. Our experience shows that domain-specific verification systems can greatly simplify the verification process of low-level software, and new techniques for combining domain-specific and foundational logics are critical for the successful verification of complete software systems. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87873-5_8 | VSTTE |
Keywords | Field | DocType |
combining domain-specific,complete software package,new methodology,verification system,software package,domain-specific verification system,complete software systems,successful verification,low-level software,completesoftware system,verification process,complete software system,foundational logics,type system,logical framework,software systems | Programming language,Software design,Computer science,Theoretical computer science,Software system,Component-based software engineering,Software verification and validation,Software construction,Software framework,Software development,Software verification | Conference |
Volume | ISSN | Citations |
5295 | 0302-9743 | 14 |
PageRank | References | Authors |
0.80 | 15 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xinyu Feng | 1 | 443 | 30.52 |
| Zhong Shao | 2 | 897 | 68.80 |
| Yu Guo | 3 | 14 | 0.80 |
| Yuan Dong | 4 | 90 | 10.67 |