License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06081.2
URN: urn:nbn:de:0030-drops-7973
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/797/
Go to the corresponding Portal

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

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

pdf-format:
06081.SWM.ExtAbstract.797.pdf (0.09 MB)

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.

BibTeX - Entry

@InProceedings{abdulla_et_al:DagSemProc.06081.2,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/797},
  URN =		{urn:nbn:de:0030-drops-7973},
  doi =		{10.4230/DagSemProc.06081.2},
  annote =	{Keywords: Infinite-state systems, model checking, program analysis, software verification}
}

Keywords: Infinite-state systems, model checking, program analysis, software verification
Collection: 06081 - Software Verification: Infinite-State Model Checking and Static Program Analysis
Issue Date: 2006
Date of publication: 09.11.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI