Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
svarm [2010/03/19 13:07] vkuncak |
svarm [2010/08/16 12:16] (current) vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Synthesis, Verification, and Analysis of Rich Models (SVARM) ====== | ====== Synthesis, Verification, and Analysis of Rich Models (SVARM) ====== | ||
- | **S**ynthesis, **V**erification, and **A**nalysis of **R**ich **M**odels **(SVARM)** will take place July 20-21 in Edinburgh, UK as part of [[http://www.floc-conference.org/|FLoC 2010]]. The event is affiliated with two FLoC conferences: | + | [[:svarm11|SVARM 2011]] at ETAPS 2011 |
- | * [[http://www.floc-conference.org/IJCAR-cfp.html|IJCAR 2010]] | + | |
- | * [[http://www.floc-conference.org/CAV.html|CAV 2010]] | + | |
- | The event will be simultaneously a meeting for all work groups of the [[:|Rich Model Toolkit Initiative]] (http://richmodels.org) | + | |
- | The event explores directions and techniques for making automated reasoning (including analysis and synthesis) applicable | + | [[:svarm10|SVARM 2010]] at FLoC 2010 |
- | 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. | + | |
- | **Invited Talks**: | ||
- | * **[[http://www.csl.sri.com/users/shankar/|Natarajan Shankar]]: Inference Architectures for Satisfiability Modulo Theories** | ||
- | * **[[http://formal.iti.kit.edu/english/team_beckert.php|Bernhard Beckert]]: Formal Verification of System Software** | ||
- | |||
- | **Further selected presentations:** | ||
- | * over 10 presentations by the members of the **[[:|Rich Model Toolkit]]** initiative | ||
- | |||
- | The event is now open to **additional abstract submissions from the scientific community** until 23 April 2010: | ||
- | * [[http://www.easychair.org/conferences/?conf=svarm2010|CLICK HERE TO SUBMIT YOUR ABSTRACT]] | ||
- | |||
- | Important dates: | ||
- | * April 23: Abstract Submission Deadline | ||
- | * April 30: Notification. Program Published Online | ||
- | * July 20-21: camera-ready version of talks to be presented to the audience :) | ||
- | |||
- | The submitted abstracts will be selected for presentation based on the originality of summarized results, expected presentation quality, and the likelihood of initiating discussion at SVARM. | ||
- | |||
- | The focus of the event is on presentations and discussions; there will be neither electronic nor paper proceedings before the event.((The FLoC USB stick promises to be great fun, but you will not find us there.)) | ||
- | |||
- | ===== 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. | ||
- | |||
- | ===== Program Committee ===== | ||
- | |||
- | * Roderick Bloem (TU Graz, Austria) | ||
- | * Armin Biere (Johannes Kepler University, Linz, Austria) | ||
- | * Maria Paola Bonacina (Università degli Studi di Verona, Italy) | ||
- | * Enric Rodriguez Carbonell (TU Catalonia, Spain) | ||
- | * Silvia Ghilezan (University of Novi Sad, Serbia) | ||
- | * Ian Horrocks (University of Oxford, UK) | ||
- | * Paul Jackson (University of Edinburgh, UK) | ||
- | * Predrag Janičić (University of Belgrade, Serbia) | ||
- | * Viktor Kuncak (EPFL, Switzerland) | ||
- | * Marius Minea (Politehnica University of Timisoara, Romania) | ||
- | * Ilkka Niemelä (Helsinki University of Technology, Finland) | ||
- | * Tobias Nipkow (TU Munich, Germany) | ||
- | * Alexander Rabinovich (Tel-Aviv University, Israel) | ||
- | * Stefan Ratschan (Academy of Sciences, Czech Republic) | ||
- | * Andrey Rybalchenko (MPI-SWS, Germany) | ||
- | * Cesar Sanchez (IMDEA-Software, Spain) | ||
- | * Natasha Sharygina (University of Lugano, Switzerland) | ||
- | * Tomáš Vojnar (Brno Univ. of Technology, Czech Republic) | ||
- | |||
- | ===== Program and Conference Chairs ===== | ||
- | |||
- | * [[http://homepages.inf.ed.ac.uk/pbj/|Paul Jackson]] | ||
- | * [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]] | ||
- | * [[http://www.fit.vutbr.cz/~vojnar/|Tomas Vojnar]] | ||
- | |||
- | Publicity Chair: **[[http://icwww.epfl.ch/~piskac/|Ruzica Piskac]]** | ||
- | |||
- | {{:ic0901-e.pdf|Description of the COST Action IC0901}} | ||
- | |||
- | ===== Abstract Submission ===== | ||
- | |||
- | Abstract submission is open until 15 April 2010 through EasyChair: | ||
- | * [[http://www.easychair.org/conferences/?conf=svarm2010|CLICK HERE TO SUBMIT YOUR ABSTRACT]] | ||