Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science Book 9207)

The two-volume set LNCS 9206 and LNCS 9207 constitutes the refereed proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, held in San Francisco, CA, USA, in July 2015. The total of 58 full and 11 short papers presented in the proceedings was carefully reviewed and selected from 252 submissions. The papers were organized in topical sections named: model checking and refinements; quantitative reasoning; software analysis; lightning talks; interpolation, IC3/PDR, and Invariants; SMT techniques and applications; HW verification; synthesis; termination; and concurrency. Front Matter....Pages I-XVIII Front Matter....Pages 1-1 Finding Bounded Path in Graph Using SMT for Automatic Clock Routing....Pages 3-19 Cutting the Mix....Pages 20-36 The Inez Mathematical Programming Modulo Theories Framework....Pages 37-52 Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets....Pages 53-69 Deciding Local Theory Extensions via E-matching....Pages 70-86 Front Matter....Pages 87-105 Modular Deductive Verification of Multiprocessor Hardware Designs....Pages 107-107 Word-Level Symbolic Trajectory Evaluation....Pages 109-127 Verifying Linearizability of Intel® Software Guard Extensions....Pages 128-143 Front Matter....Pages 144-160 Synthesis Through Unification....Pages 161-161 From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis....Pages 163-179 Counterexample-Guided Quantifier Instantiation for Synthesis in SMT....Pages 180-197 Deductive Program Repair....Pages 198-216 Quantifying Conformance Using the Skorokhod Metric....Pages 217-233 Pareto Curves of Multidimensional Mean-Payoff Games....Pages 234-250 Front Matter....Pages 251-267 Conflict-Driven Conditional Termination....Pages 269-269 Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs....Pages 271-286 Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions....Pages 287-303 Measuring with Timed Patterns....Pages 304-321 Automatic Verification of Stability and Safety for Delay Differential Equations....Pages 322-337 Front Matter....Pages 338-355 Time Robustness in MTL and Expressivity in Hybrid System Falsification....Pages 269-269 Front Matter....Pages 356-374 Adaptive Concretization for Parallel Program Synthesis....Pages 375-375 Automatic Completion of Distributed Protocols with Symmetry....Pages 377-394 An Axiomatic Specification for Sequential Memory Models....Pages 395-412 Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems....Pages 413-428 Automated and Modular Refinement Reasoning for Concurrent Programs....Pages 429-448 Back Matter....Pages 449-465 ....Pages 467-469