System Description

An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers

Conference paper (2018)

Authors

Sylvia Grewe Technische Universität Darmstadt
S.T. Erdweg Programming Languages - EEMCS
André Pacak Technische Universität Darmstadt
Mira Mezini Technische Universität Darmstadt
Research Group
Programming Languages (EEMCS) (TU Delft)
More Info
expand_more

Published Date

2018

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Programming Languages

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.

Files

3236950.3236960.pdf
(.pdf | 0.922 Mb)

Download not available