Standard

Exploration of language specifications by compilation to first-order logic. / Grewe, Sylvia; Erdweg, Sebastian; Pacak, André; Raulf, Michael; Mezini, Mira.

In: Science of Computer Programming, Vol. 155, 2018, p. 146-172.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

Grewe, S, Erdweg, S, Pacak, A, Raulf, M & Mezini, M 2018, 'Exploration of language specifications by compilation to first-order logic' Science of Computer Programming, vol. 155, pp. 146-172. https://doi.org/10.1016/j.scico.2017.08.001

APA

Grewe, S., Erdweg, S., Pacak, A., Raulf, M., & Mezini, M. (2018). Exploration of language specifications by compilation to first-order logic. Science of Computer Programming, 155, 146-172. https://doi.org/10.1016/j.scico.2017.08.001

Vancouver

Grewe S, Erdweg S, Pacak A, Raulf M, Mezini M. Exploration of language specifications by compilation to first-order logic. Science of Computer Programming. 2018;155:146-172. https://doi.org/10.1016/j.scico.2017.08.001

Author

Grewe, Sylvia ; Erdweg, Sebastian ; Pacak, André ; Raulf, Michael ; Mezini, Mira. / Exploration of language specifications by compilation to first-order logic. In: Science of Computer Programming. 2018 ; Vol. 155. pp. 146-172.

BibTeX

@article{8238a0cc6466434a9627c1416795d9af,
title = "Exploration of language specifications by compilation to first-order logic",
abstract = "Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we translate language specifications and exploration tasks to first-order logic, which many ATPs accept as input. However, there are several different strategies for compiling a language specification to first-order logic, and even small variations in the translation may have a large impact on the time it takes ATPs to find proofs. In this paper, we first present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As benchmarks, we developed language specifications for typed SQL and for a Questionnaire Language (QL), with 50 exploration goals each. Our study empirically confirms that the choice of a compilation strategy greatly influences prover performance in general and shows which strategies are advantageous for prover performance. Second, we extend our empirical study with 4 domain-specific strategies for axiom selection and find that axiom selection does not influence prover performance in our benchmark specifications.",
keywords = "Declarative languages, Domain-specific languages, First-order theorem proving, Formal specification, Type systems",
author = "Sylvia Grewe and Sebastian Erdweg and Andr{\'e} Pacak and Michael Raulf and Mira Mezini",
note = "Accepted Author Manuscript",
year = "2018",
doi = "10.1016/j.scico.2017.08.001",
language = "English",
volume = "155",
pages = "146--172",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",

}

RIS

TY - JOUR

T1 - Exploration of language specifications by compilation to first-order logic

AU - Grewe, Sylvia

AU - Erdweg, Sebastian

AU - Pacak, André

AU - Raulf, Michael

AU - Mezini, Mira

N1 - Accepted Author Manuscript

PY - 2018

Y1 - 2018

N2 - Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we translate language specifications and exploration tasks to first-order logic, which many ATPs accept as input. However, there are several different strategies for compiling a language specification to first-order logic, and even small variations in the translation may have a large impact on the time it takes ATPs to find proofs. In this paper, we first present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As benchmarks, we developed language specifications for typed SQL and for a Questionnaire Language (QL), with 50 exploration goals each. Our study empirically confirms that the choice of a compilation strategy greatly influences prover performance in general and shows which strategies are advantageous for prover performance. Second, we extend our empirical study with 4 domain-specific strategies for axiom selection and find that axiom selection does not influence prover performance in our benchmark specifications.

AB - Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we translate language specifications and exploration tasks to first-order logic, which many ATPs accept as input. However, there are several different strategies for compiling a language specification to first-order logic, and even small variations in the translation may have a large impact on the time it takes ATPs to find proofs. In this paper, we first present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As benchmarks, we developed language specifications for typed SQL and for a Questionnaire Language (QL), with 50 exploration goals each. Our study empirically confirms that the choice of a compilation strategy greatly influences prover performance in general and shows which strategies are advantageous for prover performance. Second, we extend our empirical study with 4 domain-specific strategies for axiom selection and find that axiom selection does not influence prover performance in our benchmark specifications.

KW - Declarative languages

KW - Domain-specific languages

KW - First-order theorem proving

KW - Formal specification

KW - Type systems

UR - http://www.scopus.com/inward/record.url?scp=85028400628&partnerID=8YFLogxK

UR - http://resolver.tudelft.nl/uuid:8238a0cc-6466-434a-9627-c1416795d9af

U2 - 10.1016/j.scico.2017.08.001

DO - 10.1016/j.scico.2017.08.001

M3 - Article

VL - 155

SP - 146

EP - 172

JO - Science of Computer Programming

T2 - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -

ID: 45517371