Prolog for Verification, Analysis and Transformation Tools
Michael Leuschel (University of D\"usseldorf)
TL;DR
This paper explores the application of Prolog in developing verification, analysis, and transformation tools, highlighting key features and providing practical guidelines based on experience with tools like ProB, ECCE, and LOGEN.
Contribution
It offers an assessment of Prolog's features for verification and analysis tools and provides guidelines for effective use, especially in handling negation.
Findings
Prolog is effective for verification and analysis tools.
Key Prolog features facilitate handling negation.
Guidelines improve tool development using Prolog.
Abstract
This article examines the use of the Prolog language for writing verification, analysis and transformation tools. Guided by experience in teaching and the development of verification tools like ProB or specialisation tools like ECCE and LOGEN, the article presents an assessment of various aspects of Prolog and provides guidelines for using them. The article shows the usefulness of a few key Prolog features. In particular, it discusses how to deal with negation at the level of the object programs being verified or analysed.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.