Posted by 
By Patrice Godefroid (auth.), Corina S. Păsăreanu (eds.)
This ebook constitutes the refereed court cases of the sixteenth foreign SPIN workshop on version Checking software program, SPIN 2009, held in Grenoble, France, in June 2009.
The 15 revised complete papers provided including three instrument papers and four invited talks have been conscientiously reviewed and chosen from forty-one submissions. The papers conceal theoretical and algorithmic foundations in addition to instruments for software program version checking via addressing theoretical advances and empirical reviews concerning state-space and direction exploration options, as carried out in software program verification tools.
Read Online or Download Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings PDF
Best international conferences and symposiums books
NGITS2002 used to be the ? fth workshop of its sort, selling papers that debate new applied sciences in details platforms. Following the luck of the 4 p- vious workshops (1993, 1995, 1997, and 1999), the ? fth NGITS Workshop happened on June 24–25, 2002, within the historic urban of Caesarea. in accordance with the decision for Papers, 22 papers have been submitted.
The4thInternationalWorkshoponKnowledgeDiscoveryinInductiveDatabases (KDID 2005) was once held in Porto, Portugal, on October three, 2005 together with the sixteenth ecu convention on computer studying and the ninth eu convention on ideas and perform of information Discovery in Databases. Ever because the commence of the ?
RuleML 2005 was once the ? rst foreign convention on ideas and rule markup languages for the Semantic net, held at the side of the foreign Semantic net C- ference (ISWC) at Galway, eire. With the good fortune of the RuleML workshop sequence got here the necessity for prolonged examine and functions subject matters prepared in a convention structure.
The yearly international financial institution convention on improvement Economics (ABCDE) brings jointly the world's most interesting improvement thinkers to provide their views and ideas. in recent times, a parallel, moment convention has been held in Europe with an analogous aim of increasing the move of rules among thinkers, practitioners, and policymakers within the box of foreign improvement.
Additional info for Model Checking Software: 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings
Example text
Compact hash tables using bidirectional linear probing. IEEE Trans. Computers 33(9), 828–834 (1984) 8. : An optimal bloom filter replacement. In: Proceedings of the 16th ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 823–829. SIAM, Philadelphia (2005) 9. : Reliable hashing without collision detection. In: 5th International Conference on Computer Aided Verification, pp. 59–70 (1993) 10. : Partial order reduction of the state space. In: First SPIN Workshop, Montr`eal, Quebec (1995) 11. : Improving spin’s partial-order reduction for breadth-first search.
Array rstart is copied to the global memory variable rstartGPU. To specify the number of blocks and the size of a block CUDA supports additional parameters in front of the kernel (<<< number of blocks, block size >>>). Here the grid is defined with n/BlockSize + 1 blocks2 , and a fixed BlockSize. After the multiplication and comparison step on the GPU the Terminate variable is copied back and checked. This copy statement serves also as a synchronization barrier, since the CPU program waits until all the threads of the GPU kernel have terminated before copying the variable from the GPU global memory.
Finally, each thread checks if another iteration is needed and consequently sets the variable TerminateGPU to false. Concurrent writes are resolved by the GPU memory controller. The implementation in Algorithm 2. matches the one for bounded-until (U≤k ), except that bounded-until has a fixed upper bound on the number of iterations, while for until a termination criterion applies. 5 Experiments All experiments were done on a PC with an AMD Athlon(tm) 64 X2 Dual Core Processor 3800+ with 4 GB of RAM; the operating system is 64-bit SUSE 11 with 44 D.