Venues / CAV /

CAV 2015

70 papers

A Trusted Mechanised Specification of JavaScript: One Year On · Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood
A Type-Directed Approach to Program Repair · Alex Reinking, Ruzica Piskac
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation · Mendes Oulamara, Arnaud J. Venet
Adam: Causality-Based Synthesis of Distributed Systems · Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks · Alessandro Abate, Lubos Brim, Milan Ceska, Marta Z. Kwiatkowska
Adaptive Concretization for Parallel Program Synthesis · Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, Jeffrey S. Foster
Alchemist: Learning Guarded Affine Functions · Shambwaditya Saha, Pranav Garg, P. Madhusudan
Algorithms for Model Checking HyperLTL and HyperCTL ^* · Bernd Finkbeiner, Markus N. Rabe, César Sánchez
An Axiomatic Specification for Sequential Memory Models · William Mansky, Dmitri Garbuzov, Steve Zdancewic
Angelic Verification: Precise Verification Modulo Unknowns · Ankush Das, Shuvendu K. Lahiri, Akash Lal, Yi Li
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems · Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, John C. Eidson
Automata-Based Model Counting for String Constraints · Abdulbaki Aydin, Lucas Bang, Tevfik Bultan
Automated and Modular Refinement Reasoning for Concurrent Programs · Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran
Automatic Completion of Distributed Protocols with Symmetry · Rajeev Alur, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, Abhishek Udupa
Automatic Rootcausing for Program Equivalence Failures in Binaries · Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel
Automatic Verification of Stability and Safety for Delay Differential Equations · Liang Zou, Martin Fränzle, Naijun Zhan, Peter Nazier Mosaad
Bbs: A Phase-Bounded Model Checker for Asynchronous Programs · Rupak Majumdar, Zilong Wang
Boosting k-Induction with Continuously-Refined Invariants · Dirk Beyer, Matthias Dangl, Philipp Wendler
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions · Amir M. Ben-Amram, Samir Genaim
Conflict-Driven Conditional Termination · Vijay D'Silva, Caterina Urban
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes · Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation · Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT · Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
Cutting the Mix · Jürgen Christ, Jochen Hoenicke
Deciding Local Theory Extensions via E-matching · Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
Deductive Program Repair · Etienne Kneuss, Manos Koukoutos, Viktor Kuncak
Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints · Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Julian Dolby, Xiangyu Zhang
Efficient Anytime Techniques for Model-Based Safety Analysis · Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Cristian Mattarei
Empirical Software Metrics for Benchmarking of Verification Tools · Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Fairness Modulo Theory: A New Approach to LTL Software Model Checking · Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, Andreas Podelski
Fast Interpolating BMC · Yakir Vizel, Arie Gurfinkel, Sharad Malik
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs · Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing · Amit Erez, Alexander Nadel
Fine-Grained Caching of Verification Results · K. Rustan M. Leino, Valentin Wüstholz
Formal Design and Safety Analysis of AIR6110 Wheel Brake System · Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, David Jones, Greg Kimberly, T. Petri + 2 more
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis · Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta + 1 more
Learning Commutativity Specifications · Timon Gehr, Dimitar Dimitrov, Martin T. Vechev
Measuring with Timed Patterns · Thomas Ferrère, Oded Maler, Dejan Nickovic, Dogan Ulus
Meeting a Powertrain Verification Challenge · Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, Mahesh Viswanathan
Model Checking Parameterized Asynchronous Shared-Memory Systems · Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar
Modular Deductive Verification of Multiprocessor Hardware Designs · Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave
Norn: An SMT Solver for String Constraints · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer + 1 more
On Automation of CTL* Verification for Infinite-State Systems · Byron Cook, Heidy Khlaaf, Nir Piterman
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case · Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, Reiner Hähnle
OptiMathSAT: A Tool for Optimization Modulo Theories · Roberto Sebastiani, Patrick Trentin
PROPhESY: A PRObabilistic ParamEter SYnthesis Tool · Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes + 2 more
PVSio-web 2.0: Joining PVS to HCI · Paolo Masci, Patrick Oladimeji, Yi Zhang, Paul L. Jones, Paul Curzon, Harold W. Thimbleby
Pareto Curves of Multidimensional Mean-Payoff Games · Romain Brenguier, Jean-François Raskin
Percentile Queries in Multi-dimensional Markov Decision Processes · Mickael Randour, Jean-François Raskin, Ocan Sankur
Poling: SMT Aided Linearizability Proofs · He Zhu, Gustavo Petri, Suresh Jagannathan
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs · Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
Predicting a Correct Program in Programming by Example · Rishabh Singh, Sumit Gulwani
Property-Directed Inference of Universal Invariants or Proving Their Absence · Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Quantifying Conformance Using the Skorokhod Metric · Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms · Igor Konnov, Helmut Veith, Josef Widder
Skipping Refinement · Mitesh Jain, Panagiotis Manolios
Symbolic Polytopes for Quantitative Interpolation and Verification · Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko
Synthesis Through Unification · Rajeev Alur, Pavol Cerný, Arjun Radhakrishna
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data · Jasmin Fisher, Ali Sinan Köksal, Nir Piterman, Steven Woodhouse
Systematic Asynchrony Bug Exploration for Android Apps · Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran
The Hanoi Omega-Automata Format · Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretínský, David Müller + 2 more
The Inez Mathematical Programming Modulo Theories Framework · Panagiotis Manolios, Jorge Pais, Vasilis Papavasileiou
The Open-Source LearnLib - A Framework for Active Automata Learning · Malte Isberner, Falk Howar, Bernhard Steffen
The SeaHorn Verification Framework · Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas
Time Robustness in MTL and Expressivity in Hybrid System Falsification · Takumi Akazaki, Ichiro Hasuo
Time-Aware Abstractions in HybridSal · Ashish Tiwari
Tree Buffers · Radu Grigore, Stefan Kiefer
Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets · Fahiem Bacchus, George Katsirelos
Verifying Linearizability of Intel® Software Guard Extensions · Rebekah Leslie-Hurd, Dror Caspi, Matthew Fernandez
Word-Level Symbolic Trajectory Evaluation · Supratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani + 1 more