دانلود کتاب Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings

فهرست مطالب :

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