Guest editors: Bernd Finkbeiner and Cesar Sanchez
Submission deadline: 15-Jan-2014 31-Jan-2014
This special issue is devoted to the results obtained in the context of the COST Action Richmodel Toolkit IC0901 (see http://richmodels.epfl.ch/). 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 acta@informatik.uni-oldenburg.de with subject "Special Issue on Richmodels" and comply with author guidelines of Acta Informatica (see http://www.springer.com/computer/theoretical+computer+science/journal/236).