Standard

System Description : An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers. / Grewe, Sylvia; Erdweg, Sebastian; Pacak, André; Mezini, Mira.

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. New York, NY : Association for Computing Machinery (ACM), 2018. p. 1-10.

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Harvard

Grewe, S, Erdweg, S, Pacak, A & Mezini, M 2018, System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers. in Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery (ACM), New York, NY, pp. 1-10. https://doi.org/10.1145/3236950.3236960

APA

Grewe, S., Erdweg, S., Pacak, A., & Mezini, M. (2018). System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (pp. 1-10). New York, NY: Association for Computing Machinery (ACM). https://doi.org/10.1145/3236950.3236960

Vancouver

Grewe S, Erdweg S, Pacak A, Mezini M. System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. New York, NY: Association for Computing Machinery (ACM). 2018. p. 1-10 https://doi.org/10.1145/3236950.3236960

Author

Grewe, Sylvia ; Erdweg, Sebastian ; Pacak, André ; Mezini, Mira. / System Description : An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers. Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. New York, NY : Association for Computing Machinery (ACM), 2018. pp. 1-10

BibTeX

@inproceedings{0fb5da8b5d9c4ff9b7693a5e4a004eef,
title = "System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers",
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.",
author = "Sylvia Grewe and Sebastian Erdweg and Andr{\'e} Pacak and Mira Mezini",
year = "2018",
doi = "10.1145/3236950.3236960",
language = "English",
pages = "1--10",
booktitle = "Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",

}

RIS

TY - GEN

T1 - System Description

T2 - An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers

AU - Grewe, Sylvia

AU - Erdweg, Sebastian

AU - Pacak, André

AU - Mezini, Mira

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

UR - https://dl.acm.org/citation.cfm?doid=3236950.3236960

U2 - 10.1145/3236950.3236960

DO - 10.1145/3236950.3236960

M3 - Conference contribution

SP - 1

EP - 10

BT - Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming

PB - Association for Computing Machinery (ACM)

CY - New York, NY

ER -

ID: 52211555