


default search action
27th CAV 2015: San Francisco, CA, USA
- Daniel Kroening

, Corina S. Pasareanu:
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science 9206, Springer 2015, ISBN 978-3-319-21689-8
Invited Paper
- Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood

:
A Trusted Mechanised Specification of JavaScript: One Year On. 3-10
Model Checking and Refinements
- Byron Cook, Heidy Khlaaf, Nir Piterman

:
On Automation of CTL* Verification for Infinite-State Systems. 13-29 - Bernd Finkbeiner, Markus N. Rabe, César Sánchez

:
Algorithms for Model Checking HyperLTL and HyperCTL ^*. 30-48 - Daniel Dietsch, Matthias Heizmann

, Vincent Langenfeld
, Andreas Podelski:
Fairness Modulo Theory: A New Approach to LTL Software Model Checking. 49-66 - Antoine Durand-Gasselin, Javier Esparza

, Pierre Ganty, Rupak Majumdar:
Model Checking Parameterized Asynchronous Shared-Memory Systems. 67-84 - Igor Konnov

, Helmut Veith, Josef Widder
:
SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. 85-102 - Mitesh Jain, Panagiotis Manolios

:
Skipping Refinement. 103-119
Quantitative Reasoning
- Mickael Randour, Jean-François Raskin

, Ocan Sankur:
Percentile Queries in Multi-dimensional Markov Decision Processes. 123-139 - Krishnendu Chatterjee, Rasmus Ibsen-Jensen

, Andreas Pavlogiannis
:
Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. 140-157 - Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský:

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 158-177 - Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko:

Symbolic Polytopes for Quantitative Interpolation and Verification. 178-194 - Alessandro Abate, Lubos Brim

, Milan Ceska
, Marta Z. Kwiatkowska:
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. 195-213 - Christian Dehnert, Sebastian Junges, Nils Jansen

, Florian Corzilius, Matthias Volk
, Harold Bruintjes, Joost-Pieter Katoen
, Erika Ábrahám
:
PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. 214-231
Software Analysis
- Yunhui Zheng, Vijay Ganesh

, Sanu Subramanian, Omer Tripp, Julian Dolby, Xiangyu Zhang:
Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints. 235-254 - Abdulbaki Aydin, Lucas Bang, Tevfik Bultan:

Automata-Based Model Counting for String Constraints. 255-272 - Stijn de Gouw

, Jurriaan Rot, Frank S. de Boer, Richard Bubel, Reiner Hähnle
:
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. 273-289 - Radu Grigore, Stefan Kiefer:

Tree Buffers. 290-306 - Timon Gehr, Dimitar Dimitrov

, Martin T. Vechev:
Learning Commutativity Specifications. 307-323 - Ankush Das

, Shuvendu K. Lahiri, Akash Lal, Yi Li
:
Angelic Verification: Precise Verification Modulo Unknowns. 324-342 - Arie Gurfinkel

, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas:
The SeaHorn Verification Framework. 343-361 - Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel:

Automatic Rootcausing for Program Equivalence Failures in Binaries. 362-379 - K. Rustan M. Leino, Valentin Wüstholz:

Fine-Grained Caching of Verification Results. 380-397 - Rishabh Singh, Sumit Gulwani:

Predicting a Correct Program in Programming by Example. 398-414 - Mendes Oulamara, Arnaud J. Venet

:
Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation. 415-430
Lightning Talks
- Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog:

Adam: Causality-Based Synthesis of Distributed Systems. 433-439 - Shambwaditya Saha, Pranav Garg, P. Madhusudan:

Alchemist: Learning Guarded Affine Functions. 440-446 - Roberto Sebastiani, Patrick Trentin:

OptiMathSAT: A Tool for Optimization Modulo Theories. 447-454 - Burcu Kulahcioglu Ozkan

, Michael Emmi, Serdar Tasiran:
Systematic Asynchrony Bug Exploration for Android Apps. 455-461 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen

, Lukás Holík
, Ahmed Rezine, Philipp Rümmer, Jari Stenman:
Norn: An SMT Solver for String Constraints. 462-469 - Paolo Masci

, Patrick Oladimeji, Yi Zhang
, Paul L. Jones, Paul Curzon
, Harold W. Thimbleby:
PVSio-web 2.0: Joining PVS to HCI. 470-478 - Tomás Babiak, Frantisek Blahoudek

, Alexandre Duret-Lutz
, Joachim Klein
, Jan Kretínský, David Müller, David Parker
, Jan Strejcek
:
The Hanoi Omega-Automata Format. 479-486 - Malte Isberner

, Falk Howar
, Bernhard Steffen:
The Open-Source LearnLib - A Framework for Active Automata Learning. 487-495 - Rupak Majumdar, Zilong Wang:

Bbs: A Phase-Bounded Model Checker for Asynchronous Programs. 496-503 - Ashish Tiwari:

Time-Aware Abstractions in HybridSal. 504-510 - Alex Reinking

, Ruzica Piskac
:
A Type-Directed Approach to Program Repair. 511-517 - Marco Bozzano, Alessandro Cimatti

, Anthony Fernandes Pires, David Jones, Greg Kimberly, T. Petri, R. Robinson, Stefano Tonetta:
Formal Design and Safety Analysis of AIR6110 Wheel Brake System. 518-535 - Parasara Sridhar Duggirala, Chuchu Fan

, Sayan Mitra
, Mahesh Viswanathan:
Meeting a Powertrain Verification Challenge. 536-543 - Jasmin Fisher

, Ali Sinan Köksal, Nir Piterman
, Steven Woodhouse:
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data. 544-560 - Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger:

Empirical Software Metrics for Benchmarking of Verification Tools. 561-579
Interpolation, IC3/PDR, and Invariants
- Aleksandr Karbyshev

, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
:
Property-Directed Inference of Universal Invariants or Proving Their Absence. 583-602 - Marco Bozzano, Alessandro Cimatti

, Alberto Griggio
, Cristian Mattarei
:
Efficient Anytime Techniques for Model-Based Safety Analysis. 603-621 - Dirk Beyer

, Matthias Dangl, Philipp Wendler
:
Boosting k-Induction with Continuously-Refined Invariants. 622-640 - Yakir Vizel, Arie Gurfinkel

, Sharad Malik:
Fast Interpolating BMC. 641-657 - Yu-Fang Chen

, Chih-Duo Hong
, Bow-Yaw Wang, Lijun Zhang:
Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. 658-674

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














