2017 Int. Spin Symposium on Model Checking Software

Invited Talks

  • Byron Cook (Amazon Web Services), Automated Formal Reasoning about Amazon Web Services
  • Domagoj Babic (Google), SunDew - Systematic Automated Security Testing
  • Gerard Holzmann (Nimble Research), Cobra: Fast Structural Code Checking
Research Papers

  • [PDF] D.Ratiu and A. Ulrich. Increasing Usability of Spin-based C Code Verification Using a Harness Definition Language
  • [PDF] W. Oortwijn, T.van Dijk and J. van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability
  • [PDF] J. Hua and S. Khurshid. Sketch4J: Execution-Driven Sketching for Java
  • [PDF] J. Fearnley, S. Jain, S. Schewe, F. Stephan and D. Wojtczak. An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space
  • [PDF] L. Wagner, D. Greve and A. Gacek. SIMPAL: A Compositional Reasoning Framework for Imperative Programs
  • [PDF] P. Fiterau-Brostean, F. Vaandrager, E. Poll, J. de Ruiter, T. Lenaerts and P. Verleg. Model Learning and Model Checking of SSH Implementations
  • [PDF] M. Kokologiannakis and K. Sagonas. Stateless Model Checking of the Linux Kernel's Hierarchical Read-Copy-Update (Tree RCU)
  • [PDF] V. Bloemen, A. Duret-Lutz and J. van de Pol. Explicit State Model Checking with Generalized Büchi and Rabin Automata
  • [PDF] S. Pinisetty, P. Roop, S. Smyth, S. Tripakis and R. von Hanxleden. Runtime enforcement of reactive systems using synchronous enforcers
  • [PDF] T. Geffroy, J. Leroux and G. Sutre. Backward Coverability with Pruning for Lossy Channel Systems
  • [PDF] N. Dini, C. Yelen and S. Khurshid. Optimizing Parallel Korat Using Invalid Ranges
  • [PDF] P. Mellati, E. Khamespanah and R. Khosravi. LeeTL: LTL with Quantifications Over Model Objects
  • [PDF] M. Renard, A. Rollet and Y. Falcone. Runtime Enforcement Using Büchi Games
  • [PDF] M. Antonio F. Gabaldon, C. Rocha and S. Balachandran. Verification-driven Development of Icarous Based on Automatic Reachability Analysis
  • [PDF] H. Botha, O. Tkachuk, B. Van Der Merwe and W. Visser. Addressing Challenges In Obtaining High Coverage When Model Checking Android Applications
  • [PDF] L. Panizo, A. Salmerón, M. Del Mar Gallardo and P. Merino. Guided Test Case Generation for Mobile Apps in the TRIANGLE Project
  • [PDF] B. Loring, D. Mitchell and J. Kinder. ExpoSE: Practical Symbolic Execution of Standalone JavaScript
  • [PDF] I. Husien, N. Berthier and S. Schewe. A Hot Method for Synthesising Cool Controllers
  • [PDF] H. Vu Nguyen and T. Touili. CARET Model Checking for Malware Detection
  • [PDF] M.M. Bersani, M. Erascu, F. Marconi, S. Ghilardi and M. Rossi. Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories
  • [PDF] G. Li, P. Gjøl Jensen, K. Guldstrand Larsen, A. Legay and D. Bøgsted Poulsen. Practical Controller Synthesis for MTL_{0,\infty}

Spin Homepage
Spin Symposia