English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Directed Model Checking with Distance-Preserving Abstractions

Dräge, K., Finkbeiner, B., & Podelski, A. (2006). Directed Model Checking with Distance-Preserving Abstractions. In Model checking software : 13th International SPIN Workshop (pp. 19-34). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Dräge, Klaus, Author
Finkbeiner, Bernd, Author
Podelski, Andreas1, Author           
Valmari, Antti, Editor
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and in the total runtime.

Details

show
hide
Language(s): eng - English
 Dates: 2007-04-262006
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 314399
Other: Local-ID: C1256104005ECAFC-1DD5A496410B7F92C125729E0034DA77-Podelski2006d
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Vienna, Austria
Start-/End Date: 2006-03-30

Legal Case

show

Project information

show

Source 1

show
hide
Title: Model checking software : 13th International SPIN Workshop
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 19 - 34 Identifier: ISBN: 978-3-540-33102-5

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 3925 Sequence Number: - Start / End Page: - Identifier: -