Accepted Papers

CAV 2015 Long Papers

  1. Amit Erez and Alexander Nadel. Finding Bounded Path in Graph using SMT for Automatic Clock Routing
  2. Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, David Jones, Greg Kimberly, Tyler Petri, Richard Robinson and Stefano Tonetta. Formal Design and Safety Analysis of AIR6110 Wheel Brake System
  3. Aleksandr Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. Property-Directed Inference of Universal Invariants or Proving Their Absence
  4. Shuvendu Lahiri, Rohit Sinha and Chris Hawblitzel. Automatic Rootcausing for Program Equivalence Failures in Binaries
  5. Ankush Das, Shuvendu Lahiri, Akash Lal and Yi Li. Angelic Verification: Precise Verification Modulo Unknowns
  6. Klaus von Gleissenthall, Boris Köpf and Andrey Rybalchenko. Symbolic Polytopes for Quantitative Interpolation and Verification
  7. Steven Woodhouse, Nir Piterman, Ali Sinan Köksal and Jasmin Fisher. Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
  8. Temesghen Kahsai, Jorge A Navas, Arie Gurfinkel and Anvesh Komuravelli. The SeaHorn Verification Framework
  9. Byron Cook, Heidy Khlaaf and Nir Piterman. On Automation of CTL* Verification for Infinite-State Systems
  10. Panagiotis Manolios, Vasilis Papavasileiou and Jorge Pais. The Inez Mathematical Programming Modulo Theories Framework
  11. Panagiotis Manolios and Mitesh Jain. Skipping Refinement
  12. Chris Hawblitzel, Erez Petrank, Shaz Qadeer and Serdar Tasiran. Automated and modular refinement reasoning for concurrent programs
  13. Mickael Randour, Jean-Francois Raskin and Ocan Sankur. Percentile Queries in Multi-Dimensional Markov Decision Processes
  14. Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno and Naoki Kobayashi. Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs
  15. Romain Brenguier and Jean-Francois Raskin. Pareto Curves of Multidimensional Mean-Payoff Games
  16. Thomas Ferrere, Oded Maler, Dejan Nickovic and Dogan Ulus. Measuring with Timed Patterns
  17. Krishnendu Chatterjee, Rasmus Ibsen-Jensen and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs
  18. Liang Zou, Martin Fränzle, Naijun Zhan and Peter Nazier Mosaad. Automatic Stability and Safety Verification for Delay Differential Equations
  19. Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli and Clark Barrett. Counterexample Guided Quantifier Instantiation for Synthesis in SMT
  20. Tomas Brazdil, Krishnendu Chatterjee, Martin Chmelík, Andreas Fellner and Jan Kretinsky. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes
  21. Mendes Oulamara and Arnaud J. Venet. Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
  22. Stijn de Gouw, Jurriaan Rot, Frank De Boer, Richard Bubel and Reiner Haehnle. OpenJDK’s java.utils.Collection.sort() is broken: The Good, the Bad and the Worst Case
  23. Takumi Akazaki and Ichiro Hasuo. Time Robustness in MTL and Expressivity in Hybrid System Falsification
  24. Juergen Christ and Jochen Hoenicke. Cutting the Mix
  25. Bernd Finkbeiner, Markus N. Rabe and Cesar Sanchez. Algorithms for Model Checking HyperLTL and HyperCTL*
  26. Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang and Lijun Zhang. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
  27. Pavol Cerny, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
  28. Etienne Kneuss, Manos Koukoutos and Viktor Kuncak. Deductive Program Repair
  29. Rajeev Alur, Pavol Cerny and Arjun Radhakrishna. Synthesis through Unification
  30. Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen and Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool
  31. Radu Grigore and Stefan Kiefer. Tree Buffers
  32. Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama and Jeffrey S. Foster. Adaptive Concretization for Parallel Program Synthesis
  33. Vijay D’Silva and Caterina Urban. Conflict-Driven Abstract Interpretation for Conditional Termination
  34. Amir Ben-Amram and Samir Genaim. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
  35. William Mansky, Dmitri Garbuzov and Steve Zdancewic. An Axiomatic Specification for Sequential Memory Models
  36. Fahiem Bacchus and George Katsirelos. Using Minimal Correction Sets to more Efficiently compute Minimal Unsatisfiable Sets
  37. Rebekah Leslie-Hurd, Dror Caspi and Matthew Fernandez. Verifying Linearizability of Intel Software Guard Extensions
  38. Igor Konnov, Helmut Veith and Josef Widder. SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
  39. Rishabh Singh and Sumit Gulwani. Predicting a Correct Program in Programming By Example
  40. Alessandro Abate, Milan Ceska, Lubos Brim and Marta Kwiatkowska. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks
  41. Rustan Leino and Valentin Wüstholz. Fine-grained Caching of Verification Results
  42. Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett and Thomas Wies. Deciding Local Theory Extensions via E-matching
  43. He Zhu, Gustavo Petri and Suresh Jagannathan. Poling: SMT Aided Linearizability Proofs
  44. Rajeev Alur, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis and Abhishek Udupa. Automatic Completion of Distributed Protocols with Symmetry
  45. Jyotirmoy Deshmukh, Rupak Majumdar and Vinayak Prabhu. Quantifying System Conformance using the Skorokhod Metric
  46. Timon Gehr, Dimitar Dimitrov and Martin Vechev. Learning Commutativity Specifications
  47. Abdulbaki Aydin, Lucas Bang and Tevfik Bultan. Automata-based Model Counting for String Constraints
  48. Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra and Mahesh Viswanathan. Verifying Temporal Properties of Powertrain Control Systems in Automobiles
  49. Ankush Desai, David Broman, John Eidson, Shaz Qadeer and Sanjit A. Seshia. Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
  50. Yakir Vizel, Arie Gurfinkel and Sharad Malik. Fast Interpolating BMC
  51. Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Julian Dolby and Xiangyu Zhang. Effective Search-space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints
  52. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty and Rupak Majumdar. Model Checking Parameterized Asynchronous Shared-Memory Systems
  53. Supratik Chakraborty, Zurab Khasidashvili, Carl Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani and Rakesh Mistry. Word-level Symbolic Trajectory Evaluation
  54. Yulia Demyanova, Thomas Pani, Helmut Veith and Florian Zuleger. Empirical Software Metrics for Benchmarking of Verification Tools
  55. Marco Bozzano, Alessandro Cimatti, Alberto Griggio and Cristian Mattarei. Efficient Anytime Techniques for Model-Based Safety Analysis
  56. Dirk Beyer, Matthias Dangl and Philipp Wendler. Boosting k-Induction with Continuously-Refined Invariants – Effective and Efficient Tool Implementation –
  57. Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld and Andreas Podelski. Fairness Modulo Theory: A New Approach to LTL Software Model Checking
  58. Muralidaran Vijayaraghavan, Adam Chlipala, Arvind Arvind and Nirav Dave. Modular Deductive Verification of Multiprocessor Hardware Designs

 CAV 2015 Short Papers

  1. Bernd Finkbeiner, Manuel Gieseking and Ernst-Rüdiger Olderog. ADAM: Causality-Based Synthesis of Distributed Systems
  2. Shambwaditya Saha, Pranav Garg and Madhusudan Parthasarathy. Alchemist: Learning Guarded Affine Functions
  3. Roberto Sebastiani and Patrick Trentin. OptiMathSAT: A Tool for Optimization Modulo Theories
  4. Burcu Kulahcioglu Ozkan, Michael Emmi and Serdar Tasiran. Systematic Asynchrony Bug Exploration for Android Apps
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Lukas Holik, Philipp Ruemmer, Jari Stenman, Ahmed Rezine and Yu-Fang Chen. Norn: a solver for string constraints
  6. Paolo Masci, Patrick Oladimeji, Yi Zhang, Paul Jones, Paul Curzon and Harold Thimbleby. PVSio-web 2.0: Joining PVS to Human-Computer Interaction
  7. Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker and Jan Strejcek. The Hanoi Omega-Automata Format
  8. Malte Isberner, Falk Howar and Bernhard Steffen. The Open-Source LearnLib: A Framework for Active Automata Learning
  9. Rupak Majumdar and Zilong Wang. BBS: A Phase-Bounded Model Checker for Asynchronous Programs
  10. Ashish Tiwari. Time-Aware Abstractions in HybridSal
  11. Alex Reinking and Ruzica Piskac. A Type-Directed Approach to Program Repair