Differences

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

@@ Line 1: / Line 1: @@
+====== Synthesis, Verification, and Analysis of Rich Models (SVARM) 2010 ======
+^ [[svarm:program|SVARM Program]] ^
+[[http://www.floc-conference.org/registration.html|Registration is through FLoC Registation]]
+**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]] ^