Differences

This shows you the differences between two versions of the page.

--- svarm [2010/05/21 18:31]
vkuncak
+++ svarm [2010/08/16 12:16] (current)
vkuncak
@@ Line 1: / Line 1: @@
 ====== Synthesis, Verification, and Analysis of Rich Models (SVARM) ======
-^ [[svarm:program|SVARM Program]] ^
+[[:svarm11|SVARM 2011]] at ETAPS 2011
-[[http://www.floc-conference.org/registration.html|Registration is through FLoC Registation]]
+[[:svarm10|SVARM 2010]] at FLoC 2010
-**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:
-  * [[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
-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**
-^ [[svarm:program|SVARM Program]] ^
-Abstract submission is now closed ([[svarm-cfp.txt|Call for Abstracts in Text Format]])
-===== 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]]
-Local organization: [[http://homepages.inf.ed.ac.uk/pbj/|Paul Jackson]]
-{{:ic0901-e.pdf|Description of the COST Action IC0901}}
-Important dates:
-  * April 23: Abstract Submission Deadline (CLOSED)
-  * April 30: Notification. Program Published Online
-  * July 20-21: camera-ready version of talks to be presented to the audience :)
-The focus of the event is on presentations and discussions; there will be neither electronic nor paper proceedings before the event.
-^ [[svarm:program|SVARM Program]] ^