By a News Reporter-Staff News Editor at Computers, Networks & Communications -- Data detailed on Computers - Computer Programming have been presented. According to news originating from Darmstadt, Germany, by VerticalNews correspondents, research stated, “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).”
Financial support for this research came from European Research Council.
Our news journalists obtained a quote from the research from Technical University, “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.”
According to the news editors, the research concluded: “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.”
For more information on this research see: Exploration of language specifications by compilation to first-order logic. Science of Computer Programming , 2018;155():146-172. Science of Computer Programming can be contacted at: Elsevier Science Bv, PO Box 211, 1000 Ae Amsterdam, Netherlands. (Elsevier - www.elsevier.com; Science of Computer Programming - http://www.journals.elsevier.com/science-of-computer-programming/)
The news correspondents report that additional information may be obtained from S. Grewe, Technical Univ Darmstadt, D-64289 Darmstadt, Germany. Additional authors for this research include S. Erdweg, A. Pacak, M. Raulf and M. Mezini.
The direct object identifier (DOI) for that additional information is: https://doi.org/10.1016/j.scico.2017.08.001. This DOI is a link to an online electronic document that is either free or for purchase, and can be your direct source for a journal article and its citation.
Our reports deliver fact-based news of research and discoveries from around the world. Copyright 2018, NewsRx LLC
CITATION: (2018-04-12), Researchers from Technical University Report Findings in Computer Programming (Exploration of language specifications by compilation to first-order logic), Computers, Networks & Communications, 507, ISSN: 1944-1568, BUTTER® ID: 015460694
From the newsletter Computers, Networks & Communications.
https://www.newsrx.com/Butter/#!Search:a=15460694
This is a NewsRx® article created by NewsRx® and posted by NewsRx®. As proof that we are NewsRx® posting NewsRx® content, we have added a link to this steemit page on our main corporate website. The link is at the bottom left under "site links" at https://www.newsrx.com/NewsRxCorp/.
We have been in business for more than 20 years and our full contact information is available on our main corporate website.
We only upvote our posts after at least one other user has upvoted the article to increase the curation awards of upvoters.
NewsRx® offers 195 weekly newsletters providing comprehensive information on all professional topics, ranging from health, pharma and life science to business, tech, energy, law, and finance. Our newsletters report only the most relevant and authoritative information from qualified sources.