Abstract
Computer science has seen much progress in the area of automated verification in the last decades. Yet, there are many domains where abstract strategies for verifying standard properties are well-understood by domain experts, but still not automated to a satisfactory degree. One example for such a domain are type soundness proofs. Being able to express domain-specific verification strategies using domain-specific terminology and concepts can help to narrow down this gap toward more automated verification.
We present the requirements, design, and implementation of a configurable verification infrastructure that allows for expressing domain knowledge about proofs and for interfacing with existing automated theorem provers and solvers to verify individual proof steps. As an application scenario for our infrastructure, we present the development of a standard type soundness proof for a typed subset of SQL.
We present the requirements, design, and implementation of a configurable verification infrastructure that allows for expressing domain knowledge about proofs and for interfacing with existing automated theorem provers and solvers to verify individual proof steps. As an application scenario for our infrastructure, we present the development of a standard type soundness proof for a typed subset of SQL.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming |
| Place of Publication | New York, NY |
| Publisher | Association for Computing Machinery (ACM) |
| Pages | 1-10 |
| Number of pages | 10 |
| ISBN (Electronic) | 978-1-4503-6441-6 |
| DOIs | |
| Publication status | Published - 2018 |