By David Wagner (auth.), Patrice Godefroid (eds.)
This publication constitutes the refereed court cases of the twelfth foreign SPIN workshop on version Checking software program, SPIN 2005, held in San Francisco, united states in August 2005.
The 15 revised complete papers offered have been rigorously reviewed and chosen from forty five submissions; moreover there are four instrument presentation papers chosen from 6 submissions. The papers are geared up in topical sections on kingdom illustration and abstraction, facing concurrency, facing advanced information, checking temporal houses, and checking defense and real-time properties.
Read or Download Model Checking Software: 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005. Proceedings PDF
Similar international books
Foreign Federation for info ProcessingThe IFIP sequence publishes state of the art ends up in the sciences and applied sciences of data and conversation. The scope of the sequence contains: foundations of laptop technology; software program concept and perform; schooling; laptop functions in expertise; verbal exchange platforms; platforms modeling and optimization; details platforms; desktops and society; computers know-how; safety and defense in details processing platforms; man made intelligence; and human-computer interplay.
Nuclear physics is almost immediately experiencing a thrust in the direction of basic phy sics questions. Low-energy experiments assist in trying out past trendy stan dard versions of particle physics. the quest for finite neutrino plenty and neutrino oscillations, for proton decay, infrequent and forbidden muon and pion de cays, for an electrical dipole second of the neutron denote many of the efforts to check modern day theories of grand unification (GUTs, SUSYs, Superstrings, .
- Floods, from Defence to Management: Symposium Proceedings of the 3rd International Symposium on Flood Defence, Nijmegen, The Netherlands, 25-27 May 2005
- Proceedings of the 9th International Symposium on Insect-Plant Relationships
- The Trilateral Countries in the International Economy of the 1980s
- Cryptology and Network Security: 8th International Conference, CANS 2009, Kanazawa, Japan, December 12-14, 2009. Proceedings
- Combustion and Heat Transfer in Gas Turbine Systems: Proceedings of an International Propulsion Symposium Held at the College of Aeronautics, Cranfield, April 1969
Extra info for Model Checking Software: 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005. Proceedings
Example text
In the first part we present an advanced overview of Spin [1,4], and illustrate its practical application to logic model checking problems. In the second part of the tutorial we present an overview of a related tool called Modex [2,3]. Modex can be used to extract Spin verification models directly from C source code. It supports the definition of user-defined abstractions, and cleverly exploits the capability in Spin version 4 to include embedded C code inside abstract verification models. We will show how to use Spin and Modex, separately and combined, in an effective way when searching for design errors in distributed software applications.
Fn such that for any other access chain g0 , g1 , . . , gm of the object the following holds: either m > n; or m = n and there is an i < n such that for all 0 ≤ j < i, fj = gj and fi < gi . The bfs access chain of all objects in the heap graph can be constructed by performing a breadth first traversal of the graph that traverses all outgoing edges of a node in the edge label order. Given a heap graph, the bfs access chain of an object is unique. The incremental heap canonicalization algorithm uses this chain to determine the location of objects in the canonical heap.
The main limitation of state caching is the amount of redundant work performed. Indeed, if only stack states are stored, each state s will be explored once for every path leading from the initial state to s, causing an unacceptable blowup in the execution time. It was observed in [9] that the use of partial order methods greatly reduces this problem by limiting the exploration of redundant paths. The main drawback of caching techniques is that the best replacement strategy to adopt and the run time increase heavily depends on the structure of the state space, and is thus hard to predict as observed in [10].