Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings / Edition 1

Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings / Edition 1

ISBN-10:
3642161634
ISBN-13:
9783642161636
Pub. Date:
12/09/2010
Publisher:
Springer Berlin Heidelberg
ISBN-10:
3642161634
ISBN-13:
9783642161636
Pub. Date:
12/09/2010
Publisher:
Springer Berlin Heidelberg
Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings / Edition 1

Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, Proceedings / Edition 1

Paperback

$54.99
Current price is , Original price is $54.99. You
$54.99 
  • SHIP THIS ITEM
    Qualifies for Free Shipping
  • PICK UP IN STORE
    Check Availability at Nearby Stores

Overview

This book constitutes the refereed proceedings of the 17th International
SPIN workshop on Model Checking Software, SPIN 2010, held at the
University of Twente, in Enschede, The Netherlands, in September 2010.

The 13 revised full papers presented together with 2 tool papers and 3
invited talks were carefully reviewed and selected from 33 submissions.
The papers are organized in topical sections on satisfiability modulo theories for model checking, model checking in context (simulation,
testing, UML), implementation and performance of model checking, LTL and Büchi automata, extensions to infinite-state systems, and concurrent software.


Product Details

ISBN-13: 9783642161636
Publisher: Springer Berlin Heidelberg
Publication date: 12/09/2010
Series: Lecture Notes in Computer Science , #6349
Edition description: 2010
Pages: 263
Product dimensions: 6.10(w) x 9.30(h) x 0.70(d)

Table of Contents

Satisfiability Modulo Theories for Model Checking

SMT-Based Software Model Checking (Invited Talk) Alessandro Cimatti 1

Symbolic Object Code Analysis Jan Tobias Mühlberg Gerald Lüttgen 4

Model Checking in Context

Experimental Comparison of Concolic and Random Testing for Java Card Applets Kari Kähkönen Roland Kindermann Keijo Heljanko Ilkka Niemelä 22

Combining SPIN with ns-2 for Protocol Optimization Pedro Merino Alberto Salmerón 40

Automatic Generation of Model Checking Scripts Based on Environment Modeling Kenro Yatake Toshiaki Aoki 58

Implementation and Performance of Model Checking

Model Checking: Cleared for Take Off (Invited Talk) Darren Cofer 76

Context-Enhanced Directed Model Checking Martin Wehrle Sebastian Kupferschmid 88

Efficient Explicit-State Model Checking on General Purpose Graphics Processors Stefan Edelkamp Damian Sulewski 106

The SpinJa Model Checker (Tool Presentation) Marc de Jonge Theo C. Ruys 124

LTL and Büchi Automata

On the Virtue of Patience: Minimizing Büchi Automata Rüdiger Ehlers Bernd Finkbeiner 129

Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance Maja Pešic Dragan Bošnacki Wil M.P. van der Aalst 146

Nevertrace Claims for Model Checking Zhe Chen Gilles Motet 162

Infinite State Models

A False History of True Concurrency: From Petri to Tools (Invited Talk) Javier Esparza 180

Analysing Mu-Calculus Properties of Pushdown Systems (Tool Presentation) Matthew Hague C.-H. Luke Ong 187

Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains Georgel Calin Pepijn Crouzen Pedro R. D'Argenio E. Moritz Hahn Lijun Zhang 193

An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models Alexander Linden Pierre Wolper 212

Concurrent Software

Context-Bounded Translations for Concurrent Software: An Empirical Evaluation Naghmeh Ghafari Alan J. Hu Zvonimir Rakamaric 227

One Stack to Run Them All: Reducing Concurrent Analysis to Sequential Analysis under Priority Scheduling Nicholas Kidd Suresh Jagannathan Jan Vitek 245

Author Index 263

From the B&N Reads Blog

Customer Reviews