Model Checking Software

✍ Scribed by María del Mar Gallardo, Pedro Merino

• Publisher: Springer International Publishing
• Year: 2018
• Tongue: English
• Leaves: 361
• Series: Lecture Notes in Computer Science 10869
• Edition: 1st ed.
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

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

✦ Subjects

Computer Science; Software Engineering; Programming Languages, Compilers, Interpreters; Simulation and Modeling; Mathematical Logic and Formal Languages; Algorithm Analysis and Problem Complexity; Logics and Meanings of Programs