Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
svarm [2010/04/04 12:54]
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) ======
  
-[[svarm-cfp.txt|Call for Abstracts in Text Format]]+[[:svarm11|SVARM 2011]] at ETAPS 2011
  
-**S**ynthesis,​ **V**erification,​ and **A**nalysis of **R**ich **M**odels **(SVARM)**((SVARM could also be taken to mean: Synthesis, Verification,​ and Automated Reasoning Methods)) 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:​ +[[:svarm10|SVARM 2010]] ​at FLoC 2010
-  * [[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** +
- +
-**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. +
- +
-===== 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]]+