This is an old revision of the document!

Call For Articles: Acta Informatica

Special Issue on COST Action Rich Model Toolkit

Guest editors: Bernd Finkbeiner and Cesar Sanchez

Submission deadline: 15-Jan-2014

This special issue is devoted to the results obtained in the context of the COST Action Richmodel Toolkit IC0901 (see This initiative has consisted on exploring directions and techniques for making automated reasoning (including analysis and synthesis) applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers.

Selected topics of interest include:

- Decision procedures. Decision procedures for new classes of

constraints. SAT and SMT implementation and certification. Encoding
synthesis and analysis problems into SMT. Description logics and
scalable reasoning about knowledge bases.

- Transition system analysis. Abstraction-based approaches and

refinement for verification of infinite-state
systems. Constraint-based program analysis. Data-flow analysis for
complex domains. Extracting transition systems from programming
languages and bytecodes.

- High-level synthesis. New algorithms for synthesis from high-level

specifications. Extending decision procedures to perform synthesis
tasks. Connections between invariant generation and code synthesis.

Submitted papers should contain theoretical result, for example a provably sound verification method or proven correct algorithm.

Submission to this special issue is *not* restricted to only participants and invited experts that took part in the activities of the action. Instead, submission if open to all researchers.

We expect original articles (typically 20-30 pages), which present high-quality contributions that have not been previously published in a journal and are not concurrently submitted to any other peer reviewed venue. Extended versions of contributions previously published in proceedings need to contain significant new material and should be accompanied by a short description of the extension.

Submissions should be sent to

with subject “Special Issue on Richmodels” and comply with author guidelines of Acta Informatica (see