Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II

Description

This open access two-volume set LNCS 10980 and 10981 constitutes the refereed proceedings of the 30th International Conference on Computer Aided Verification, CAV 2018, held in Oxford, UK, in July 2018. The 52 full and 13 tool papers presented together with 3 invited papers and 2 tutorials were carefully reviewed and selected from 215 submissions. The papers cover a wide range of topics and techniques, from algorithmic and logical foundations of verification to practical applications in distributed, networked, cyber-physical, and autonomous systems. They are organized in topical sections on model checking, program analysis using polyhedra, synthesis, learning, runtime verification, hybrid and timed systems, tools, probabilistic systems, static analysis, theory and security, SAT, SMT and decisions procedures, concurrency, and CPS, hardware, industrial applications. Front Matter ....Pages I-XX Front Matter ....Pages 1-1 Let this Graph Be Your Witness! (Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll)....Pages 3-11 MaxSMT-Based Type Inference for Python 3 (Mostafa Hassan, Caterina Urban, Marco Eilers, Peter Müller)....Pages 12-19 The JKind Model Checker (Andrew Gacek, John Backes, Mike Whalen, Lucas Wagner, Elaheh Ghassabani)....Pages 20-27 The DEEPSEC Prover (Vincent Cheval, Steve Kremer, Itsaka Rakotonirina)....Pages 28-36 SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability (Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi)....Pages 37-44 StringFuzz: A Fuzzer for String Solvers (Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, Vijay Ganesh)....Pages 45-51 Front Matter ....Pages 53-53 Permission Inference for Array Programs (Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller)....Pages 55-74 Program Analysis Is Harder Than Verification: A Computability Perspective (Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato)....Pages 75-95 Front Matter ....Pages 97-97 Automata vs Linear-Programming Discounted-Sum Inclusion (Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi)....Pages 99-116 Model Checking Indistinguishability of Randomized Security Protocols (Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan)....Pages 117-135 Lazy Self-composition for Security Verification (Weikun Yang, Yakir Vizel, Pramod Subramanyan, Aarti Gupta, Sharad Malik)....Pages 136-156 SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks (Jun Zhang, Pengfei Gao, Fu Song, Chao Wang)....Pages 157-177 Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, Viktor Toman)....Pages 178-197 Attracting Tangles to Solve Parity Games (Tom van Dijk)....Pages 198-215 Front Matter ....Pages 217-217 Delta-Decision Procedures for Exists-Forall Problems over the Reals (Soonho Kong, Armando Solar-Lezama, Sicun Gao)....Pages 219-235 Solving Quantified Bit-Vectors Using Invertibility Conditions (Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli)....Pages 236-255 Understanding and Extending Incremental Determinization for 2QBF (Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia)....Pages 256-274 The Proof Complexity of SMT Solvers (Robert Robere, Antonina Kolokolova, Vijay Ganesh)....Pages 275-293 Model Generation for Quantified Formulas: A Taint-Based Approach (Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet)....Pages 294-313 Front Matter ....Pages 315-315 Partial Order Aware Concurrency Sampling (Xinhao Yuan, Junfeng Yang, Ronghui Gu)....Pages 317-335 Reasoning About TSO Programs Using Reduction and Abstraction (Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran)....Pages 336-353 Quasi-Optimal Partial Order Reduction (Huyen T. T. Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, Laure Petrucci)....Pages 354-371 On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony (Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer)....Pages 372-391 Constrained Dynamic Partial Order Reduction (Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio)....Pages 392-410 Front Matter ....Pages 411-411 Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (Mark Tullsen, Lee Pike, Nathan Collins, Aaron Tomb)....Pages 413-429 Continuous Formal Verification of Amazon s2n (Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh et al.)....Pages 430-446 Symbolic Liveness Analysis of Real-World Software (Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, Klaus Wehrle)....Pages 447-466 Model Checking Boot Code from AWS Data Centers (Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle)....Pages 467-486 Android Stack Machine (Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan)....Pages 487-504 Formally Verified Montgomery Multiplication (Christoph Walther)....Pages 505-522 Inner and Outer Approximating Flowpipes for Delay Differential Equations (Eric Goubault, Sylvie Putot, Lorenz Sahlmann)....Pages 523-541 Back Matter ....Pages 543-545