Links

DOI

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 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 a benchmark, we developed a language specification for typed SQL with 50 exploration goals. Our study empirically confirms that the choice of a compilation strategy in general greatly influences prover performance and shows which strategies are advantageous for prover performance.
Original languageEnglish
Title of host publicationProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming
PublisherAssociation for Computing Machinery (ACM)
Pages104--117
Number of pages14
ISBN (Electronic)978-1-4503-4148-6
DOIs
StatePublished - 2017

    Research areas

  • declarative languages, domain-specific languages, first-order theorem proving, formal specification, type systems

ID: 32869744