Table of Contents
Synthesis, Verification, and Analysis of Rich Models (SVARM) 2011
Synthesis, Verification, and Analysis of Rich Models (SVARM 2011) will take place April 1-3, 2011, as part of ETAPS 2011.
Invited speakers:
- Thomas A. Henzinger: Quantitative Reactive Models, Friday, April 1st, 2pm
- George Candea: S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems, Saturday, April 2nd, 2pm
- Darko Marinov: Systematic Software Testing Using Test Abstractions, Sunday, April 3rd, 9am
The event is supported by the COST Action IC0901, but the participation is open to all registered participants. The presentations are by invitation.
Participants from COST Action will receive special registration instructions, for other participants the registration proceeds as for other ETAPS workshops.
In any case, the registration will be through the ETAPS web site.
The event 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.
Scope of the Event
Researchers have recently developed a number of useful tools for automated analysis of particular classes of models of computer systems:
- software vendors are using static analyses supported by automated theorem provers and constraint solvers to prevent software crashes;
- hardware manufacturers are using SAT solvers,model checkers, and theorem provers to identify and correct errors that could have enormous financial consequences;
- description logic reasoners analyze relationships between tens of thousands of terms in medical ontologies and verify their consistency;
- aircraft manufacturers and space agencies are using analysis tools based on abstract interpretation to eliminate errors in aircraft control software.
Despite these successes, today’s automated analysis methods are not widespread in engineering practice. Among the factors contributing to this state of affairs are the limitations of the tools themselves: insufficient automation, specialized input formats, and no support for high-level synthesis. Another factor is the lack of standards of quality that would easy tool interoperability and give formally certified computer system a competitive advantage over systems without formal assurance guarantees.
Example 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 high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.
Contacts
Chairs:
For program committee, please see http://richmodels.org
Description of the COST Action IC0901
The focus of the event is on presentations and discussions; there will be neither electronic nor paper proceedings before the event.