Welcome to the Joint SVARM & VERIFY Workshop 2012!
Verification has developed into a flourishing research field attracting researchers with different backgrounds, ranging from computation/proof theory, deductive systems, and model checking to hardware/software analysis and software engineering. With this joint workshop we want to bring together researchers from these fields to discuss topics on verification of computer systems as well as underlying theoretical foundations. The workshop combines the already established workshops SVARM and VERIFY, which will be described in what follows.
The Joint SVARM & VERIFY 2012 Workshop will offer:
- A substantial number of invited talks that review new results and give systematic overview of more established ones.
- Presentations of regular papers (6-15 pages in Springer LNCS format; 20 min. presentation plus 10 min. discussion) as well as discussion papers (3-15 pages; 10-15 min. for presentation, including discussion).
- Brief announcements (5-15min) of recent results.
- A demo session for tools for analysis and synthesis of systems.
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.
The workshop 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.
Relationship to the COST Action IC0901: SVARM is part of the Work Group meeting of the ESF COST Action IC0901 "Rich Model Toolkit—An Infrastructure for Reliable Computer Systems". The information about this activity is at http://richmodels.org.
The formal verification of critical information systems has a long tradition as one of the main areas of application for automated theorem proving. Nevertheless, the area is of still growing importance as the number of computers affecting everyday life and the complexity of these systems are both increasing. The purpose of the VERIFY workshop series is to discuss problems arising during the formal modeling and verification of information systems and to investigate suitable solutions. Possible perspectives include those of automated theorem proving, tool support, system engineering, and applications.
The VERIFY workshop series aims at bringing together people who are interested in the development of safety-critical and security-critical systems, in formal methods, in the development of automated theorem-proving techniques, and in the development of tool support. Practical experiences gained in realistic verification tasks are of interest to the automated theorem-proving community, and new theorem-proving techniques should be transferred into practice. The overall objective of the VERIFY workshops is to identify open problems and to discuss possible solutions under the theme
What are the verification problems? What are the deduction techniques?