Downloads provided by UsageCounts
A language-agnostic program verifier takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. It then uses a language-agnostic verification algorithm to prove the program correct with respect to its specification, using directly the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate for it. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for the verification of an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic.
Program Verification, Matching Logic, Reachability Logic
Program Verification, Matching Logic, Reachability Logic
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 28 | |
| downloads | 3 |

Views provided by UsageCounts
Downloads provided by UsageCounts