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

Link to this comparison view

svarm10 [2010/08/16 11:55] (current)
vkuncak created
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
 +  * 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]] ^