Accepted Papers

The CAV 2018 proceedings are Open Access:

  1. Part 1
  2. Part 2

The proceedings contain the following papers:

  1. Eric Goubault, Sylvie Putot and Lorenz Sahlman. Inner and Outer Approximating Flowpipes for Delay Differential Equations
  2. Anna Becchi and Enea Zaffanella. A Direct Encoding for NNC Polyhedra
  3. Christoph Walther. Formally Verified Montgomery Multiplication
  4. Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir and Vijay Ganesh. StringFuzz: A Fuzzer for String Solvers
  5. Tom van Dijk. Attracting Tangles to Solve Parity Games
  6. Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan. Android Stack Systems
  7. Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio. Constrained Dynamic Partial Order Reduction
  8. Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier and Moshe Vardi. SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
  9. George Argyros and Loris D'Antoni. The Learnability of Symbolic Automata
  10. Xinyu Wang, Greg Anderson, Isil Dillig and Ken McMillan. Learning Abstractions for Program Synthesis
  11. Qinheping Hu and Loris D'Antoni. Syntax Guided Synthesis with Quantitative Syntactic Objectives
  12. Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee and Viktor Toman. Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
  13. Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar. ADAC: Automated Design of Approximate Circuits
  14. Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck. A Counting Semantics for Monitoring LTL Specifications over Finite Traces
  15. Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
  16. Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato. Program Analysis is Harder than Verification: A Computability Perspective
  17. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig and Mark R. Tuttle. Model Checking Boot Code from AWS Data Centers
  18. Jun Zhang, Pengfei Gao, Fu Song and Chao Wang. SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
  19. Michael Blondin, Javier Esparza and Stefan Jaax. Peregrine: A Tool for the Analysis of Population Protocols
  20. Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle. Symbolic Liveness Analysis of Real-World Software
  21. Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet. Model Generation for Quantified Formulas: A Taint-Based Approach
  22. Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar. Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
  23. Kenneth McMillan. Eager Abstraction for Symbolic Model Checking
  24. Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh Viswanathan. Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
  25. Weikun Yang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta and Sharad Malik. Lazy Self-Composition for Security Verification
  26. Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel and Marek Trtik. JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
  27. Qiyi Tang and Franck van Breugel. Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
  28. Hui Kong, Ezio Bartocci and Tom Henzinger. Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
  29. Lauren Pick, Grigory Fedyukovich and Aarti Gupta. Exploiting Synchrony and Symmetry in Relational Verification
  30. Matthew Bauer, Rohit Chadha, Mahesh Viswanathan and Prasad Sistla. Model checking indistinguishability of randomized security protocols
  31. Aws Albarghouthi and Justin Hsu. Constraint-Based Synthesis of Coupling Proofs
  32. Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer. On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
  33. Robert Robere, Antonina Kolokolova and Vijay Ganesh. The Proof Complexity of SMT Solvers
  34. Josiah Dodds, Andrey Chudnov, Aaron Tomb, Stephen Magill, Nathan Collins, Edwin Westbrook, Byron Cook, Serdar Tasiran, Colm MacCarthaigh, Eric Mertens, Eric Mullen and Brian Huffman. Continuous formal verification of Amazon s2n
  35. Suguman Bansal, Swarat Chaudhuri and Moshe Vardi. Automata vs Linear-Programming Discounted-Sum Inclusion
  36. Markus N. Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. Seshia. Understanding and Extending Incremental Determinization for 2QBF
  37. Marco Eilers and Peter Müller. Nagini: A Static Verifier for Python
  38. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Solving Quantified Bit-Vectors using Invertibility Conditions
  39. Weichao Zhou and Wenchao Li. Safety-Aware Apprenticeship Learning
  40. Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia and Naijun Zhan. Monitoring CTMCs By Multi-Clock Timed Automata
  41. Andrew Gacek, John Backes, Michael Whalen, Lucas Wagner and Elaheh Ghassabani. The JKind Model Checker
  42. Daniel J. Fremont and Sanjit A. Seshia. Randomized Reactive Synthesis
  43. Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas Noll. Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
  44. Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin Biere. BTOR2, BtorMC and Boolector 3.0
  45. Mark Tullsen, Nathan Collins, Lee Pike and Aaron Tomb. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
  46. Michael Emmi and Constantin Enea. Monitoring Weak Consistency
  47. Tim Quatmann and Joost-Pieter Katoen. Sound Value Iteration
  48. Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci. Quasi-Optimal Partial Order Reduction
  49. Hazem Torfah, Bernd Finkbeiner and Christopher Hahn. Model Checking Quantitative Hyperproperties
  50. Bernd Finkbeiner, Leander Tentrup, Marvin Stenger, Philip Lukert and Christopher Hahn. Synthesizing Reactive Systems from Hyperproperties
  51. Grigory Fedyukovich, Yueling Zhang and Aarti Gupta. Syntax-Guided Termination Analysis
  52. Suha Orhun Mutluergil, Constantin Enea, Ahmed Bouajjani and Serdar Tasiran. Reasoning About TSO Programs Using Reduction and Abstraction
  53. Philipp J. Meyer, Salomon Sickert and Michael Luttenberger. Strix: Explicit Reactive Synthesis Strikes Back!
  54. Edon Kelmendi, Julia Krämer, Jan Kretinsky and Maximilian Weininger. Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
  55. Jan Kretinsky, Tobias Meggendorfer and Salomon Sickert. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
  56. Xinhao Yuan and Junfeng Yang. Partial Order Aware Concurrency Sampling
  57. Mostafa Hassan, Caterina Urban, Marco Eilers and Peter Müller. MaxSMT-Based Type Inference for Python 3
  58. Jérôme Dohrau, Alexander J Summers, Caterina Urban, Severin Münger and Peter Müller. Permission Inference for Array Programs
  59. Soonho Kong, Armando Solar-Lezama and Sicun Gao. Solving Exists-Forall Problems over the Reals
  60. Yuki Satake and Hiroshi Unno. Propositional Dynamic Logic for Higher-Order Functional Programs
  61. Goran Frehse, Mirco Giacobbe and Thomas Henzinger. Spacetime Interpolants
  62. Gagandeep Singh, Markus Püschel and Martin Vechev. Fast Numerical Program Analysis with Reinforcement Learning
  63. Alessandro Abate, Cristina David, Pascal Kesseli, Kroening Daniel and Elizabeth Polgreen. Synthesis Modulo Theories
  64. S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah. What’s hard about Boolean Functional Synthesis?