[TYPES/announce] First CFP: Special Issue of the Journal of Automated Reasoning on Interpolation Techniques for Program Verification and Synthesis

Andrey Rybalchenko rybal at in.tum.de
Wed Jul 2 17:49:34 EDT 2014


                        Special Issue of 
              The Journal of Automated Reasoning
                                  on 
Interpolation Techniques for Program Verification and Synthesis


                     CALL FOR PAPERS


BACKGROUND AND SCOPE

Craig interpolation is a key ingridient in modern program verification
and synthesis tools. It can guide the construction of auxiliary
assertions required by the verification/synthesis methods by
considering infeasibility proofs of certain progam paths.
Craig interpolation enjoys an elegant theoretical foundations and is
supported by a variety of efficient algorithms.

This special issue aims at providing a snapshot of the
state of the art of the subject today and the most promising research
directions. Examples of suitable topics are:

- Interpolating decision procedures
- Proof-theoretic approaches to interpolation
- Proof systems and calculi for interpolation
- Proof transformation techniques
- Inductive proofs
- Logical abduction
- Interpolation techniques based on constraint solving, linear programming...
- Alternative techniques for interpolation
- Interpolation theorems (for theories and extensions, non-classical
 logic, ...)
- Interpolation-based/inductive invariant generation
- Program analysis and verification
- Tools for interpolation
- Applications of Craig interpolation (verification, synthesis, 
 automated reasoning, ...)
- Forgetting, variable elimination and uniform interpolation
- Complexity results and limitations


SUBMISSION

Papers (no longer than 30 pages) should be formatted according to
JAR's author guidelines and submitted via EasyChair at
https://www.easychair.org/conferences/?conf=jarinterpolation2014.


DEADLINE

September 30, 2014


EDITORS

Daniel Kroening, Oxford University
Andrey Rybalchenko, Microsoft Research


INQUIRIES

For further information send an email to rybal at microsoft.com.


More information about the Types-announce mailing list