Skip to main content
SpringerLink
Log in
Book cover

Automated Technology for Verification and Analysis

13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings

  • Conference proceedings
  • © 2015

Overview

Editors:
  1. Bernd Finkbeiner

    1. Universität des Saarlandes, Saarbrücken, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Geguang Pu

    1. East China Normal University, Shanghai, China

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Lijun Zhang

    1. Chinese Academy of Sciences, Beijing, China

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: ATVA 2015.

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 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

Licence this eBook for your library

Institutional subscriptions

Table of contents (35 papers)

  1. Front Matter

    Pages I-XIII
    Download chapter PDF

  2. Probabilistic Programming: A True Verification Challenge

    • Joost-Pieter Katoen
    Pages 1-3

  3. Machines Reasoning About Machines: 2015

    • J Strother Moore
    Pages 4-13

  4. Using SMT for Solving Fragments of Parameterised Boolean Equation Systems

    • Ruud P. J. Koolen, Tim A. C. Willemse, Hans Zantema
    Pages 14-30

  5. Unfolding-Based Process Discovery

    • Hernán Ponce-de-León, César Rodríguez, Josep Carmona, Keijo Heljanko, Stefan Haar
    Pages 31-47

  6. Improving Interpolants for Linear Arithmetic

    • Ernst Althaus, Björn Beber, Joschka Kupilas, Christoph Scholl
    Pages 48-63

  7. A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

    • Thibaut Girka, David Mentré, Yann Régis-Gianas
    Pages 64-79

  8. On Automated Lemma Generation for Separation Logic with Inductive Definitions

    • Constantin Enea, Mihaela Sighireanu, Zhilin Wu
    Pages 80-96

  9. Severity Levels of Inconsistent Code

    • Martin Schäf, Ashish Tiwari
    Pages 97-113

  10. Learning the Language of Error

    • Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig
    Pages 114-130

  11. Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage

    • Arnd Hartmanns, Holger Hermanns
    Pages 131-147

  12. Model Checking Failure-Prone Open Systems Using Probabilistic Automata

    • Yue Ben, A. Prasad Sistla
    Pages 148-165

  13. Optimal Continuous Time Markov Decisions

    • Yuliya Butkova, Hassan Hatefi, Holger Hermanns, Jan Krčál
    Pages 166-182

  14. Spanning the Spectrum from Safety to Liveness

    • Rachel Faran, Orna Kupferman
    Pages 183-200

  15. Marimba: A Tool for Verifying Properties of Hidden Markov Models

    • Noé Hernández, Kerstin Eder, Evgeni Magid, Jesús Savage, David A. Rosenblueth
    Pages 201-206

  16. ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols

    • Yongjian Li, Jun Pang, Yi Lv, Dongrui Fan, Shen Cao, Kaiqiang Duan
    Pages 207-213

  17. ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks

    • Andrzej Mizera, Jun Pang, Qixia Yuan
    Pages 214-220

  18. EviCheck: Digital Evidence for Android

    • Mohamed Nassim Seghir, David Aspinall
    Pages 221-227

  19. Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant Schedules

    • Vladimir Herdt, Hoang M. Le, Daniel Große, Rolf Drechsler
    Pages 228-233

  20. A Contextual Equivalence Checker for IMJ*

    • Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos
    Pages 234-240
Back to top

Other volumes

  1. Automated Technology for Verification and Analysis

Keywords

About this book

This book constitutes the proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015, held in Shanghai, China, in October  2015.

The 27 revised papers presented together with 6 tool papers in this volume were carefully reviewed and selected from 95 submissions. They show current research on theoretical and practical aspects of automated analysis, verification and synthesis by providing an international forum for interaction among the researchers in academia and industry.

Editors and Affiliations

  • Universität des Saarlandes, Saarbrücken, Germany

    Bernd Finkbeiner

  • East China Normal University, Shanghai, China

    Geguang Pu

  • Chinese Academy of Sciences, Beijing, China

    Lijun Zhang

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation