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.
Original languageEnglish
Title of host publicationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming
Place of PublicationNew York, NY
PublisherAssociation for Computing Machinery (ACM)
Number of pages10
ISBN (Electronic)978-1-4503-6441-6
Publication statusPublished - 2018

ID: 52211555