19. SPIN 2012: Oxford, UK

Invited Contributions

• Thomas Ball, Nikolaj Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes:
  Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. 1-6
  
• Paul Dan Marinescu, Cristian Cadar:
  High-Coverage Symbolic Patch Testing. 7-21
  
• Andrey Rybalchenko:
  Towards Automatic Synthesis of Software Verification Tools. 22
  
• Andreas Zeller:
  Mining Models. 23
  

Model Checking Techniques

• Stefan Leue, Mitra Tabaei Befrouei:
  Counterexample Explanation by Anomaly Detection. 24-42
  
• Sami Evangelista, Lars Michael Kristensen:
  Combining the Sweep-Line Method with the Use of an External-Memory Priority Queue. 43-61
  
• Hao Zheng, Emmanuel Rodriguez, Yingying Zhang, Chris J. Myers:
  A Compositional Minimization Approach for Large Asynchronous Design Verification. 62-79
  

Parallel Model Checking 1

• Alexander Ditter, Milan Ceska, Gerald Lüttgen:
  On Parallel Software Verification Using Boolean Equation Systems. 80-97
  
• Anton Wijs, Dragan Bosnacki:
  Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking. 98-116
  

Case Studies

• Theo C. Ruys, Pim Kars:
  Gossiping Girls Are All Alike. 117-136
  
• Shravan Garlapati, Sandeep K. Shukla:
  Formal Verification of Hierarchically Distributed Agent Based Protection Scheme in Smart Grid. 137-154
  

Parallel Model Checking 2

• Gerard J. Holzmann:
  Parallelizing the Spin Model Checker. 155-171
  
• Ethan Burns, Rong Zhou:
  Parallel Model Checking Using Abstraction. 172-190
  

Model Checking for Concurrency

• Reng Zeng, Zhuo Sun, Su Liu, Xudong He:
  McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking. 191-207
  
• Divjyot Sethi, Muralidhar Talupur, Daniel Schwartz-Narbonne, Sharad Malik:
  Parameterized Model Checking of Fine Grained Concurrency. 208-226
  

Tool Demonstrations

• Jonathan Bogdoll, Alexandre David, Arnd Hartmanns, Holger Hermanns:
  mctau: Bridging the Gap between Modest and UPPAAL. 227-233
  
• Heinz Riener, Görschwin Fey:
  FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation. 234-240
  
• Martin Sulzmann, Axel Zechner:
  Model Checking DSL-Generated C Source Code. 241-247
  
• Jürgen Christ, Jochen Hoenicke, Alexander Nutz:
  SMTInterpol: An Interpolating SMT Solver. 248-254
  
• Yong Jiang, Zongyan Qiu:
  S2N: Model Transformation from SPIN to NuSMV - (Tool Paper). 255-260
  

Last update Fri May 24 19:51:15 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page