Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II

Description

The open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together with 13 tool papers and 2 case studies, were carefully reviewed and selected from 258 submissions. The papers were organized in the following topical sections: Part I: automata and timed systems; security and hyperproperties; synthesis; model checking; cyber-physical systems and machine learning; probabilistic systems, runtime techniques; dynamical, hybrid, and reactive systems; Part II: logics, decision procedures; and solvers; numerical programs; verification; distributed systems and networks; verification and invariants; and concurrency. Front Matter ....Pages i-xx Front Matter ....Pages 1-1 Satisfiability Checking for Mission-Time LTL (Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier)....Pages 3-22 High-Level Abstractions for Simplifying Extended String Constraints in SMT (Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli)....Pages 23-42 Alternating Automata Modulo First Order Theories (Radu Iosif, Xiao Xu)....Pages 43-63 Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors (Martin Jonáš, Jan Strejček)....Pages 64-73 cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis (Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, Cesare Tinelli)....Pages 74-83 Incremental Determinization for Quantifier Elimination and Functional Synthesis (Markus N. Rabe)....Pages 84-94 Front Matter ....Pages 95-95 Loop Summarization with Rational Vector Addition Systems (Jake Silverman, Zachary Kincaid)....Pages 97-115 Invertibility Conditions for Floating-Point Formulas (Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli)....Pages 116-136 Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (Sicun Gao, James Kapinski, Jyotirmoy Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga et al.)....Pages 137-154 Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler (Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock)....Pages 155-173 Sound Approximation of Programs with Elementary Functions (Eva Darulova, Anastasia Volkova)....Pages 174-183 Front Matter ....Pages 185-185 Formal Verification of Quantum Algorithms Using Quantum Hoare Logic (Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li et al.)....Pages 187-207 SecCSL: Security Concurrent Separation Logic (Gidon Ernst, Toby Murray)....Pages 208-230 Reachability Analysis for AWS-Based Networks (John Backes, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu et al.)....Pages 231-241 Front Matter ....Pages 243-243 Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (Idan Berkovits, Marijana Lazić, Giuliano Losa, Oded Padon, Sharon Shoham)....Pages 245-266 Gradual Consistency Checking (Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi)....Pages 267-285 Checking Robustness Against Snapshot Isolation (Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea)....Pages 286-304 Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement (Nick Giannarakis, Ryan Beckett, Ratul Mahajan, David Walker)....Pages 305-323 On the Complexity of Checking Consistency for Replicated Data Types (Ranadeep Biswas, Michael Emmi, Constantin Enea)....Pages 324-343 Communication-Closed Asynchronous Protocols (Andrei Damian, Cezara Drăgoi, Alexandru Militaru, Josef Widder)....Pages 344-363 Front Matter ....Pages 365-365 Interpolating Strong Induction (Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel)....Pages 367-385 Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Peizun Liu, Thomas Wahl, Akash Lal)....Pages 386-404 Inferring Inductive Invariants from Phase Structures (Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv)....Pages 405-425 Termination of Triangular Integer Loops is Decidable (Florian Frohn, Jürgen Giesl)....Pages 426-444 AliveInLean: A Verified LLVM Peephole Optimization Verifier (Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes)....Pages 445-455 Front Matter ....Pages 457-457 Automated Parameterized Verification of CRDTs (Kartik Nagar, Suresh Jagannathan)....Pages 459-477 What’s Wrong with On-the-Fly Partial Order Reduction (Stephen F. Siegel)....Pages 478-495 Integrating Formal Schedulability Analysis into a Verified OS Kernel (Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao)....Pages 496-514 Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS (Yongwang Zhao, David Sanán)....Pages 515-533 Violat: Generating Tests of Observational Refinement for Concurrent Objects (Michael Emmi, Constantin Enea)....Pages 534-546 Back Matter ....Pages 547-549