Model Checking Software

Description

This book constitutes the refereed proceedings of the 25th International Symposium on Model Checking Software, SPIN 2018, held in Malaga, Spain, in June 2018. The 14 papers presented, 1 short paper, and 1 demo-tool paper, were carefully reviewed and selected from 28 submissions. Topics covered include formal verification techniques for automated analysis of software; formal analysis for modeling languages, such as UML/state charts; formal specification languages, temporal logic, design-by-contract; model checking, automated theorem proving, including SAT and SMT; verifying compilers; abstraction and symbolic execution techniques; and much more. Front Matter ....Pages I-XVI Front Matter ....Pages 1-1 Software Model Checking for Mobile Security – Collusion Detection in \(\mathbb {K}\) (Irina Măriuca Asăvoae, Hoang Nga Nguyen, Markus Roggenbach)....Pages 3-25 Efficient Runtime Verification of First-Order Temporal Properties (Klaus Havelund, Doron Peled)....Pages 26-47 Program Verification with Separation Logic (Radu Iosif)....Pages 48-62 Front Matter ....Pages 63-63 Petri Net Reductions for Counting Markings (Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio)....Pages 65-84 Improving Generalization in Software IC3 (Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen)....Pages 85-102 Star-Topology Decoupling in SPIN (Daniel Gnad, Patrick Dubbert, Alberto Lluch Lafuente, Jörg Hoffmann)....Pages 103-114 Joint Forces for Memory Safety Checking (Marek Chalupa, Jan Strejček, Martina Vitovská)....Pages 115-132 Model-Checking HyperLTL for Pushdown Systems (Adrien Pommellet, Tayssir Touili)....Pages 133-152 A Branching Time Variant of CaRet (Jens Oliver Gutsfeld, Markus Müller-Olm, Benedikt Nordhoff)....Pages 153-170 Control Strategies for Off-Line Testing of Timed Systems (Léo Henry, Thierry Jéron, Nicolas Markey)....Pages 171-189 An Extension of TRIANGLE Testbed with Model-Based Testing (Laura Panizo, Almudena Díaz, Bruno García)....Pages 190-195 Local Data Race Freedom with Non-multi-copy Atomicity (Tatsuya Abe)....Pages 196-215 A Comparative Study of Decision Diagrams for Real-Time Model Checking (Omar Al-Bataineh, Mark Reynolds, David Rosenblum)....Pages 216-234 Lazy Reachability Checking for Timed Automata with Discrete Variables (Tamás Tóth, István Majzik)....Pages 235-254 From SysML to Model Checkers via Model Transformation (Martin Kölbl, Stefan Leue, Hargurbir Singh)....Pages 255-274 Genetic Synthesis of Concurrent Code Using Model Checking and Statistical Model Checking (Lei Bu, Doron Peled, Dachuan Shen, Yuan Zhuang)....Pages 275-291 Quantitative Model Checking for a Controller Design (YoungMin Kwon, Eunhee Kim)....Pages 292-307 Modelling Without a Modelling Language (Antti Valmari, Vesa Lappalainen)....Pages 308-327 Context-Updates Analysis and Refinement in Chisel (Irina Măriuca Asăvoae, Mihail Asăvoae, Adrián Riesco)....Pages 328-346 Back Matter ....Pages 347-347