Theory and Practice of Logic Programming

SPECIAL ISSUE ON COMPUTATIONAL LOGIC FOR VERIFICATION

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.

SUBMISSION DEADLINE

An expression of interest to submit, title and abstract (to gvidal@dsic.upv.es): October 15, 2016 (STRICT)

Full paper: December 18, 2016

SUBMISSION FORMAT

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"
• Finally, fill in 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"

GUEST EDITOR

Germán Vidal
Universitat Politècnica de València

---