Skip to main content
  • Conference proceedings
  • © 2015

Computer Aided Verification

27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 9206)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): CAV: International Conference on Computer Aided Verification

Conference proceedings info: CAV 2015.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (44 papers)

  1. Front Matter

    Pages I-XXIII
  2. Invited Paper

    1. Front Matter

      Pages 1-1
    2. A Trusted Mechanised Specification of JavaScript: One Year On

      • Philippa Gardner, Gareth Smith, Conrad Watt, Thomas Wood
      Pages 3-10
  3. Model Checking and Refinements

    1. Front Matter

      Pages 11-11
    2. On Automation of CTL* Verification for Infinite-State Systems

      • Byron Cook, Heidy Khlaaf, Nir Piterman
      Pages 13-29
    3. Algorithms for Model Checking HyperLTL and HyperCTL\(^*\)

      • Bernd Finkbeiner, Markus N. Rabe, César Sánchez
      Pages 30-48
    4. Fairness Modulo Theory: A New Approach to LTL Software Model Checking

      • Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, Andreas Podelski
      Pages 49-66
    5. Model Checking Parameterized Asynchronous Shared-Memory Systems

      • Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar
      Pages 67-84
    6. Skipping Refinement

      • Mitesh Jain, Panagiotis Manolios
      Pages 103-119
  4. Quantitative Reasoning

    1. Front Matter

      Pages 121-121
    2. Percentile Queries in Multi-dimensional Markov Decision Processes

      • Mickael Randour, Jean-François Raskin, Ocan Sankur
      Pages 123-139
    3. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs

      • Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis
      Pages 140-157
    4. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

      • Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Andreas Fellner, Jan Křetínský
      Pages 158-177
    5. Symbolic Polytopes for Quantitative Interpolation and Verification

      • Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko
      Pages 178-194
    6. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks

      • Alessandro Abate, Luboš Brim, Milan Češka, Marta Kwiatkowska
      Pages 195-213
    7. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

      • Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes et al.
      Pages 214-231
  5. Software Analysis

    1. Front Matter

      Pages 233-233
    2. 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
      Pages 235-254
    3. Automata-Based Model Counting for String Constraints

      • Abdulbaki Aydin, Lucas Bang, Tevfik Bultan
      Pages 255-272

Other Volumes

  1. Computer Aided Verification

About this book

The two-volume set LNCS 9206 and LNCS 9207 constitutes the refereed proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, held in San Francisco, CA, USA, in July 2015.

The total of 58 full and 11 short papers presented in the proceedings was carefully reviewed and selected from 252 submissions. The papers were organized in topical sections named: model checking and refinements; quantitative reasoning; software analysis; lightning talks; interpolation, IC3/PDR, and Invariants; SMT techniques and applications; HW verification; synthesis; termination; and concurrency.

Editors and Affiliations

  • University of Oxford, Oxford, United Kingdom

    Daniel Kroening

  • Carnegie Mellon University, Moffett Field, USA

    Corina S. Păsăreanu

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access