The last decade has witnessed a growing interest in the use of computational logic methods for program validation and verification. For instance, verification problems for imperative and object oriented languages can be expressed using Constraint Logic Programming (CLP) and related formalisms like Constraint Horn Clauses (CHC).
Both CLP and CHC have been recently proposed as appropriate intermediate languages where program analysis and verification techniques for different programming languages can be defined, proved correct, and implemented. Furthermore, a translation from several programming languages to either CLP or CHC already exist, together with efficient methods for solving verification problems expressed in these formalisms.
The aim of this special issue is to attract high-quality research papers on the interplay between verification techniques and computational logic. Topics of interest include, but are not limited, to the use of CLP, CHC, and related formalisms for program validation and verification. Case studies, system tools and challenging problems in this area are also welcome.
An expression of interest to submit, title and abstract:
October 15 2016 (STRICT)
Full paper: November 15 2016
Submissions must be made in the TPLP format
and handled by the new TPLP submission system:
- Go to http://journals.cambridge.org/action/displayJournal?jid=TLP
- Click the button “Submit Your Article” in the left column (register for an account if you don’t have one)
- After you are logged in click “Author Centre” and then “Click here to submit a new manuscript”.
- Then choose “Original Article”
- Then, fill the required fields and upload the paper. In particular, at the end of the page you’ll see the “Special Issue” option. Select “Computational Logic for Verification”
Universitat Politecnica de Valencia