Verification, Model Checking, and Abstract Interpretation : 18th International Conference, VMCAI 2017, Paris, France, January 15{u2013}17, 2017, Proceedings

This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017. The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems. Front Matter....Pages I-XVII Bringing LTL Model Checking to Biologists....Pages 1-13 Detecting Strict Aliasing Violations in the Wild....Pages 14-33 Effective Bug Finding in C Programs with Shape and Effect Abstractions....Pages 34-54 Synthesizing Non-Vacuous Systems....Pages 55-72 Static Analysis of Communicating Processes Using Symbolic Transducers....Pages 73-90 Reduction of Workflow Nets for Generalised Soundness Verification....Pages 91-111 Structuring Abstract Interpreters Through State and Value Abstractions....Pages 112-130 Matching Multiplications in Bit-Vector Formulas....Pages 131-150 Independence Abstractions and Models of Concurrency....Pages 151-168 Complete Abstractions and Subclassical Modal Logics....Pages 169-186 Using Abstract Interpretation to Correct Synchronization Faults....Pages 187-208 Property Directed Reachability for Proving Absence of Concurrent Modification Errors....Pages 209-227 Stabilizing Floating-Point Programs Using Provenance Analysis....Pages 228-245 Dynamic Reductions for Model Checking Concurrent Software....Pages 246-265 Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games....Pages 266-287 Counterexample Validation and Interpolation-Based Refinement for Forest Automata....Pages 288-309 Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT....Pages 310-329 Solving Nonlinear Integer Arithmetic with MCSAT....Pages 330-346 Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms....Pages 347-366 Efficient Elimination of Redundancies in Polyhedra by Raytracing....Pages 367-385 Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions....Pages 386-404 Detecting All High-Level Dataraces in an RTOS Kernel....Pages 405-423 Reachability for Dynamic Parametric Processes....Pages 424-441 Conjunctive Abstract Interpretation Using Paramodulation....Pages 442-461 Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic....Pages 462-482 Finding Relevant Templates via the Principal Component Analysis....Pages 483-499 Sound Bit-Precise Numerical Domains....Pages 500-520 IC3 - Flipping the E in ICE....Pages 521-538 Partitioned Memory Models for Program Analysis....Pages 539-558 Back Matter....Pages 559-560