Exploration of Language Specifications by Compilation to First-order Logic

Sylvia Grewe, Sebastian Erdweg, Michael Raulf, Mira Mezini

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

5 Citations (Scopus)


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
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Number of pages14
ISBN (Electronic)978-1-4503-4148-6
Publication statusPublished - 2016
EventPPDP 2016: 18th International Symposium of Declarative Programming - Edinburgh, United Kingdom
Duration: 5 Sep 20167 Sep 2016
Conference number: 18


ConferencePPDP 2016
Country/TerritoryUnited Kingdom
Internet address


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


Dive into the research topics of 'Exploration of Language Specifications by Compilation to First-order Logic'. Together they form a unique fingerprint.

Cite this