Document Open Access Logo

06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm



PDF
Thumbnail PDF

File

DagSemProc.06081.2.pdf
  • Filesize: 93 kB
  • 5 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
Ahmed Bouajjani
Markus Müller-Olm

Cite AsGet BibTex

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)
https://doi.org/10.4230/DagSemProc.06081.2

Abstract

{\em Software systems} are present at the very heart of many daily-life applications, such as in communication (telephony and mobile Internet), transportation, energy, health, etc. Such systems are very often {\em critical}\/ in the sense that their failure can have considerable human/economical consequences. In order to ensure reliability, development methods must include {\em algorithmic analysis and verification techniques} which allow (1) to detect automatically defective behaviors of the system and to analyze their source, and (2) to check that every component of a system conforms to its specification. Two important and quite active research communities are particularly concerned with this challenge: the community of computer-aided verification, especially the community of (infinite-state) model checking, and the community of static program analysis. From 19.02.06 to 24.02.06, 51 researchers from these two communities met at the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' in order to improve and deepen the mutual understanding of the developed technologies and to trigger collaborations. During the seminar which was held at the International Conference and Research Center (IBFI), Schloss Dagstuhl, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper.
Keywords
  • Infinite-state systems
  • model checking
  • program analysis
  • software verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail