This initiative explores 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.
A Sample of Topics of Interest:
Standardization of expressive languages. Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for automated reasoning, verification, analysis, synthesis.
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 highlevel specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.
Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer Systems
Official pages:
Upcoming Action IC0901 meetings:
-
-
WG2+3 Meeting will be held with
FMCAD 2010, October 18-19, 2010
Past meetings:
About COST: http://www.cost.esf.org/
Rich Model Toolkit Mailing List (for broad technical discussions):
Management Committee Mailing List (for decision making and Action logistics):
Both lists have domain epfl.ch
URL for configuration and archive:
From countries participating under the COST European Cooperation:
Additional experts: