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 Constrained 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 (to email@example.com): October 15, 2016 (STRICT)
Full paper: December 18, 2016
Submissions must be made in the TPLP format and handled by the new TPLP submission system: