Skip to main content
SpringerLink
Log in
Book cover

Computer Aided Verification

22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings

  • Conference proceedings
  • © 2010

Overview

Editors:
  1. Tayssir Touili

    1. LIAFA, CNRS and University Paris Diderot, Paris Cedex 13, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Byron Cook

    1. Microsoft Research, Cambridge, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Paul Jackson

    1. School of Informatics, University of Edinburgh, Edinburgh, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • State-of-the-art research
  • Fast-track conference proceedings
  • Unique visibility

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

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

Included in the following conference series:

Conference proceedings info: CAV 2010.

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

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.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

Licence this eBook for your library

Institutional subscriptions

Table of contents (58 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Talks

    1. Policy Monitoring in First-Order Temporal Logic

      • David Basin, Felix Klaedtke, Samuel Müller
      Pages 1-18

    2. Retrofitting Legacy Code for Security

      • Somesh Jha
      Pages 19-19

    3. Quantitative Information Flow: From Theory to Practice?

      • Pasquale Malacaria
      Pages 20-22

    4. Memory Management in Concurrent Algorithms

      • Maged M. Michael
      Pages 23-23

  3. Invited Tutorials

    1. ABC: An Academic Industrial-Strength Verification Tool

      • Robert Brayton, Alan Mishchenko
      Pages 24-40

    2. There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code

      • Thomas Reps, Junghee Lim, Aditya Thakur, Gogul Balakrishnan, Akash Lal
      Pages 41-56

    3. Constraint Solving for Program Verification: Theory and Practice by Example

      • Andrey Rybalchenko
      Pages 57-71

  4. Session 1. Software Model Checking

    1. Invariant Synthesis for Programs Manipulating Lists with Unbounded Data

      • Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu
      Pages 72-88

    2. Termination Analysis with Compositional Transition Invariants

      • Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
      Pages 89-103

    3. Lazy Annotation for Program Testing and Verification

      • Kenneth L. McMillan
      Pages 104-118

    4. The Static Driver Verifier Research Platform

      • Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg
      Pages 119-122

    5. Dsolve: Safety Verification via Liquid Types

      • Ming Kawaguchi, Patrick M. Rondon, Ranjit Jhala
      Pages 123-126

    6. Contessa: Concurrency Testing Augmented with Symbolic Analysis

      • Sudipta Kundu, Malay K. Ganai, Chao Wang
      Pages 127-131

  5. Session 2. Model Checking and Automata

    1. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing

      • Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr et al.
      Pages 132-147

    2. Efficient Emptiness Check for Timed Büchi Automata

      • Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
      Pages 148-161

  6. Session 3. Tools

    1. Merit: An Interpolating Model-Checker

      • Nicolas Caniart
      Pages 162-166

    2. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems

      • Alexandre Donzé
      Pages 167-170

    3. Jtlv: A Framework for Developing Verification Algorithms

      • Amir Pnueli, Yaniv Sa’ar, Lenore D. Zuck
      Pages 171-174

    4. Petruchio: From Dynamic Networks to Nets

      • Roland Meyer, Tim Strazny
      Pages 175-179
Back to top

Other volumes

  1. Computer Aided Verification

Keywords

Editors and Affiliations

  • LIAFA, CNRS and University Paris Diderot, Paris Cedex 13, France

    Tayssir Touili

  • Microsoft Research, Cambridge, UK

    Byron Cook

  • School of Informatics, University of Edinburgh, Edinburgh, UK

    Paul Jackson

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation