Pub. Date:
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

by Jaco van der Pol, Michael Weber


Current price is , Original price is $89.99. You
Select a Purchase Option (2010)
  • purchase options
    $60.66 $89.99 Save 33% Current price is $60.66, Original price is $89.99. You Save 33%.
  • purchase options

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

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews