Automated Technology for Verification and Analysis

14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings

  • Cyrille Artho
  • Axel Legay
  • Doron Peled
Conference proceedings ATVA 2016

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

Also part of the Programming and Software Engineering book sub series (LNPSE, volume 9938)

Table of contents

  1. Front Matter
    Pages I-XI
  2. Keynote

  3. Markov Models, Chains, and Decision Processes

    1. Front Matter
      Pages 11-11
    2. Alessandro Abate, Milan Češka, Marta Kwiatkowska
      Pages 13-31
    3. Tomáš Brázdil, Antonín Kučera, Petr Novotný
      Pages 32-49
    4. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
      Pages 50-67
    5. Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen
      Pages 68-85
  4. Counter Systems, Automata

    1. Front Matter
      Pages 87-87
    2. Florent Avellaneda, Silvano Dal Zilio, Jean-Baptiste Raclet
      Pages 106-121
    3. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault, Laurent Xu
      Pages 122-129
  5. Parallelism, Concurrency

    1. Front Matter
      Pages 139-139
    2. Óscar Martín, Alberto Verdejo, Narciso Martí-Oliet
      Pages 141-156
    3. Bernd Finkbeiner, Helmut Seidl, Christian Müller
      Pages 157-173
    4. Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
      Pages 174-191
    5. Nikola Beneš, Luboš Brim, Martin Demko, Samuel Pastva, David Šafránek
      Pages 192-208
  6. Complexity, Decidability

    1. Front Matter
      Pages 209-209
    2. Denis Kuperberg, Julien Brunel, David Chemouil
      Pages 211-226
    3. Romain Brenguier, Vojtěch Forejt
      Pages 227-243
    4. Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King
      Pages 244-261
    5. Philipp J. Meyer, Michael Luttenberger
      Pages 262-267
  7. Synthesis, Refinement

    1. Front Matter
      Pages 269-269
    2. Bernd Finkbeiner, Hazem Torfah
      Pages 271-286
    3. Shoham Ben-David, Marsha Chechik, Sebastian Uchitel
      Pages 287-303
  8. Optimization, Heuristics, Partial-Order Reductions

    1. Front Matter
      Pages 321-321
    2. Christel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich
      Pages 323-339
    3. Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
      Pages 340-356
    4. Thomas Neele, Anton Wijs, Dragan Bošnački, Jaco van de Pol
      Pages 357-374
    5. Patrick Metzler, Habib Saissi, Péter Bokor, Robin Hesse, Neeraj Suri
      Pages 375-391
  9. Solving Procedures, Model Checking

    1. Front Matter
      Pages 393-393
    2. Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
      Pages 395-411
    3. Hendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff
      Pages 412-427
    4. Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina
      Pages 428-443
    5. David Deininger, Rayna Dimitrova, Rupak Majumdar
      Pages 444-460
  10. Program Analysis

    1. Front Matter
      Pages 461-461
    2. Jinru Hua, Sarfraz Khurshid
      Pages 463-478
    3. Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
      Pages 479-494
    4. Rui Qiu, Corina S. Păsăreanu, Sarfraz Khurshid
      Pages 495-511
    5. Pavel Čadek, Jan Strejček, Marek Trtík
      Pages 512-527
  11. Back Matter
    Pages 529-530

About these proceedings


This book constitutes the proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, held in Chiba, Japan, in October 2016.

The 31 papers presented in this volume were carefully reviewed and selected from 82 submissions. They were organized in topical sections named: keynote; Markov models, chains, and decision processes; counter systems, automata; parallelism, concurrency; complexity, decidability; synthesis, refinement; optimization, heuristics, partial-order reductions; solving procedures, model checking; and program analysis. 


formal modeling hybrid systems model checking optimization program analysis complexity concurrency data center decidability dynamic programming GPGPU markov decision processes parallelism probabilistic model checking reachability analysis software certification static analysis symbolic execution temporal logic verification

Editors and affiliations

  • Cyrille Artho
    • 1
  • Axel Legay
    • 2
  • Doron Peled
    • 3
  1. 1.AIST OsakaJapan
  2. 2.Inria Rennes RennesFrance
  3. 3.Bar Ilan University Ramat GanIsrael

Bibliographic information

Industry Sectors
Chemical Manufacturing
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Energy, Utilities & Environment