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

Link to this comparison view

Both sides previous revision Previous revision
svarm [2010/05/21 18:31]
svarm [2010/08/16 12:16] (current)
Line 1: Line 1:
 ====== Synthesis, Verification,​ and Analysis of Rich Models (SVARM) ====== ====== 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 
-  * 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]] ^