Name
Title | ||
|---|---|---|
Counterexample generation for program verification based on ownership refinement types |
Abstract | ||
|---|---|---|
ABSTRACTType-based program verification, which reduces program verification to type inference, has been used as a lightweight approach to automated program verification. Whilst it is often effective and faster than other methods such as model checking, the type-based approach often fails to provide useful information upon a failure of the verification. We address this problem for a recent type-based verification tool called ConSORT for imperative programs. Producing a useful error message is particularly challenging for ConSORT, as the underlying type system combines the notions of ownership, refinement types, and context-sensitivity. This paper proposes a method to produce error messages for ConSORT and reports an implementation and experimental results. The proposed method is potentially useful also for other type-based tools for automated program verification. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3441296.3441396 | PEPM |
Keywords | DocType | Citations |
Type-based program verification, counterexample, ownership type, refinement type, constrained Horn clauses | Conference | 0 |
PageRank | References | Authors |
0.34 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hideto Ueno | 1 | 0 | 0.68 |
| John Toman | 2 | 0 | 0.34 |
| Naoki Kobayashi | 3 | 0 | 3.38 |
| Takeshi Tsukada | 4 | 0 | 2.03 |