ATVA 2016

ATVA 2016

14th International Symposium on Automated Technology for Verification and Analysis

October 17 - 20, 2016, Chiba, Japan


The purpose of ATVA is to promote research on theoretical and practical aspects of automated analysis, verification and synthesis by providing a forum for interaction between the regional and the international research communities and industry in the field. The previous events were held in Taiwan - 2003-5, Beijing - 2006, Tokyo - 2007, Seoul - 2008, Macao - 2009, Singapore - 2010, Taiwan - 2011, Thiruvananthapuram - 2012, Hanoi – 2013, Sydney – 2014, and Shanghai - 2015.

Booklet / Proceedings

The proceedings of ATVA 2016 are now available as Springer LNCS 9938.

Conference booklet (pdf) with detailed information on ATVA 2016.


ATVA 2016 registration is closed


Main conference

ATVA 2016 will take place at the Mitsui Garden Hotel in Chiba, Japan.

Chiba can be reached from Tokyo/Narita Airport in just 45 minutes by a direct train. That airport has direct flights to most large cities in the world.

Chiba is also 40 minutes away from central Tokyo and close to attractions such as

  • Nokogiri Mountain, which boasts spectacular cliffs and a 30-meter-tall Buddha statue;
  • Tokyo Disney, the largest Disney theme park outside the U.S.;
  • Tokyo SkyTree, the second-largest structure in the world;
  • Asakusa Temple, the largest temple in Tokyo.


Tutorials will be held at Chiba University Nishi-Chiba campus (1 station apart from the hotel).

Travel Information

Travel from Narita Airport (NRT) to Chiba: 50 minutes
By train (every 30 minutes):

  1. JR Narita Line, 40+ min. (7+ stops), to Chiba Station
    Some (local) trains stop more often and take slightly longer
  2. 900 m on foot (10 min.) or by taxi
Note: The Narita Express (NEX, red) train usually skips Chiba station, so please take the Narita Line (blue) instead!

Travel from Haneda Airport (HND) to Chiba: 80 minutes
By bus (every 30 minutes):

  1. Haneda Airport Limousine Bus to Chiba-chuo-eki (45 - 95 min. depending on traffic)
  2. 700 m on foot or by taxi
By train (every 10 minutes):
  1. Keikyu-Kuuko Line (Airport Express) to Shinagawa (20 min.)
  2. Yokosuka Line to Chiba (50 min.), towards Chiba or Narita Airport.
  3. 900 m on foot (10 min.) or by taxi

Travel from elsewhere in Japan: You can check train schedules on this web site: Google Maps also has good traffic information.

Important Dates

May 7, 2016 23:59 AoE Abstract submission deadline
May 13, 2016 23:59 AoE Paper submission deadline
June 15, 2016 Paper acceptance/rejection notification
June 29, 2016 Camera-ready copy deadline
October 17 - 19, 2016 Main conference
October 20, 2016 Tutorials

Invited Speakers for keynotes and tutorials

  • Masahiro Fujita (University of Tokyo, Japan)
    Keynote: Unification of Synthesis and Verification in Topologically Constrained Logic Design.
  • Masahiro Fujita (University of Tokyo, Japan)
    Tutorial: Synthesizing and completely testing hardware based on templates through small numbers of test patterns.
  • Javier Esparza (Technical University Munich, Germany)
    Keynote: From LTL to Limit-Deterministic Automata.
  • Javier Esparza (Technical University Munich, Germany)
    Verification of population protocols.
  • Tevfik Bultan (University of California, Santa Barbara, United States)
    Keynote: Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution.
  • Tevfik Bultan (University of California, Santa Barbara, United States)
    Tutorial: String Analysis for Vulnerability Detection and Repair.
  • Lenore Zuck (University of Illinois at Chicago, United States)
    Uniform verification of parameterized systems.

Accepted Papers

Óscar Martín, Alberto Verdejo and Narciso Martí-Oliet. Synchronous products of rewrite systems
Alexandre Duret-LutzFabrice KordonDenis Poitrenaud and Etienne RenaultHeuristics for Checking Liveness Properties with Partial Order Reductions
Romain Brenguier and Vojtech Forejt. Decidability Results for Multi-objective Stochastic Games
Florent Avellaneda, Silvano Dal Zilio and Jean-Baptiste Raclet. Solving Language Equations using Flanked Automata
Karina Wimmer, Ralf WimmerChristoph Scholl and Bernd BeckerSkolem Functions for DQBF
Julien BrunelDenis Kuperberg and David ChemouilOn Finite Domains in First-Order Linear Temporal Logic
Hendrik Roehm, Jens Oehlerking, Thomas Heinz and Matthias Althoff. STL Model Checking of Continuous and Hybrid Systems
Thomas Neele, Anton Wijs, Dragan Bosnacki and Jaco van de Pol. Partial-Order Reduction for GPU Model Checking
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault and Laurent Xu. Spot 2.0 =E2=80=94 a framework for LTL and omega-automata manipilation
Steven De Oliveira, Saddek Bensalem and Virgile Prevosto. Polynomial invariants by linear algebra
Bernd Finkbeiner and Hazem TorfahSynthesizing Skeletons for Reactive Systems
Alessandro Abate, Milan Ceska and Marta KwiatkowskaApproximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations
Patrick Metzler, Habib Saissi, Péter Bokor, Robin Hesse and Neeraj Suri. Efficient Verification of Program Fragments: Eager POR
Matteo Marescotti, Antti Hyvärinen and Natasha SharyginaClause Sharing and Partitioning for Cloud-Based SMT Solving
Philipp J. Meyer and Michael Luttenberger. Solving Mean-Payoff Games on the GPU
Radu Iosif and Arnaud SangnierHow hard is it to verify flat affine counter systems with the finite monoid property ?
Andrew ReynoldsRadu IosifCristina Serban and Tim KingA Decision Procedure for Separation Logic in SMT
Tomas Brazdil, Antonin Kucera and Petr NovotnýOptimizing the Expected Mean Payoff in Energy Markov Decision Processes
Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva and David Safránek. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems
Truc Nguyen LamBernd FischerSalvatore La Torre and Gennaro ParlatoLazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
Bernd Finkbeiner, Helmut Seidl and Christian Müller. Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents
Tim Quatmann, Christian Dehnert, Nils JansenSebastian Junges and Joost-Pieter KatoenParameter Synthesis for Markov Models: Faster Than Ever
Nils Jansen, Christian Dehnert, Benjamin Lucien KaminskiJoost-Pieter Katoen and Lukas Westhofen. Bounded Model Checking for Probabilistic Programs
Rui Qiu, Corina Pasareanu and Sarfraz Khurshid. Certified Symbolic Execution
Shoham Ben-David, Marsha Chechik and Sebastian Uchitel. Observational Refinement and Merge for Disjunctive MTSs
Xin Li and Naoki KobayashiEquivalence-Based Abstraction Refinement for muHORS Model Checking
Salomon Sickert and Jan Kretinsky. MoChiBA: Probabilistic LTL Model Checking using limit-deterministic Büchi Automata
Jinru Hua and Sarfraz Khurshid. A Sketching-Based Approach for Debugging Using Test Cases
David Deininger, Rayna Dimitrova and Rupak MajumdarSymbolic Model Checking for Factored Probabilistic Models
Pavel Cadek, Jan Strejcek and Marek Trtík. Tighter Loop Bound Analysis
Christel Baier, Hermann de Meer, Sascha Klüppelholz, Florian Niedermeier and Sascha WunderlichGreener Bits: Formal Analysis of Demand Response


Programme Committee Co-Chairs

  • Cyrille Artho (AIST, Japan)
  • Axel Legay (Inria Rennes, France)
  • Doron Peled (Bar Ilan University, Israel)

Publicity Chair

  • Takashi Kitamura (AIST, Japan)

Local Chairs

  • Mitsuharu Yamamoto (Chiba University, Japan)
  • Yoshinori Tanabe (Tsurumi University, Japan)

Programme Committee

  • Toshiaki Aoki
  • Cyrille Artho
  • Christel Baier
  • Armin Biere
  • Tevfik Bultan
  • Franck Cassez
  • Krishnendu Chaterjee
  • Allesandro Cimatti
  • Rance Cleaveland
  • Deepak D'Souza
  • Allen Emerson
  • Bernd Finkbeiner
  • Radu Grosu
  • Klaus Havelund
  • Marieke Huisman
  • Ralf Huuck
  • Moonzoo Kim
  • Marta Kwiatkowska
  • Kim Larsen
  • Axel Legay
  • Tiziana Margaria
  • Madhavan Mukund
  • Anca Muscholl
  • Doron Peled
  • Andreas Podelski
  • Geguang Pu
  • Sven Schewe
  • Oleg Sokolsky
  • Marielle Stoelinga
  • Bow-Yaw Wang
  • Chao Wang
  • Farn Wang
  • Wang Yi
  • Naijun Zhan
  • Lijun Zhang
  • Huibiao Zhu

Call for papers



ATVA 2016 solicits high quality submissions in areas related to the theory and practice of automated analysis and verification of hardware and software systems. Topics of interest include, but are not limited to:

  • Formalisms for modeling hardware, software and embedded systems
  • Specification and verification of finite-state, infinite-state and parameterized system
  • Program analysis and software verification
  • Analysis and verification of hardware circuits, systems-on-chip and embedded systems
  • Analysis of real-time, hybrid, priced/weighted and probabilistic systems
  • Deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification
  • Analytical techniques for safety, security, and dependability
  • Testing and runtime antalysis based on verification technology
  • Analysis and verification of parallel and concurrent hardware/software systems
  • Verification in industrial practice
  • Applications and case studies

Theory papers should preferably be motivated by practical problems, and applications should be based on sound theory and should solve problems of practical interest.


ATVA invites research contributions in two categories:

  • Regular research papers (with 16 pages page limit, including references)
  • Tool papers (with 5 pages page limit, not counting references)

Contributions must be written in English and in LNCS format, and must present original research that is unpublished and not submitted elsewhere (conferences or journals). The proceedings of ATVA 2016 will be published by Springer as a volume in the series of Lecture Notes in Computer Science (LNCS).

PDF versions of the papers should be submitted to EasyChair.

Proofs and details omitted due to space constraints may be put in an appendix. Any such additional material will be read by reviewers/program committee members at their discretion. Authors are therefore urged to include details necessary for evaluation of the technical merit of their work within the prescribed page limits.

Tool papers must include information about a URL from where the tool can be downloaded or accessed on-line for evaluation. The URL must also contain a set of examples, and a user's manual that describes usage of the tool through examples. In case the tool needs to be downloaded and installed, the URL must also contain a document clearly giving instructions for installation of the tool on Linux/Windows/MacOS.

Accepted papers in both categories will be published by Springer as a LNCS volume. At least one author of each accepted paper must also register for the conference and present the paper.

Workshop Proposals

ATVA 2016 invites submissions for workshop proposals on topics of interest to the ATVA series. The workshops will be either half day or one full day. The workshops will be scheduled on October 20 and 21, 2016. Please send proposals by email to the ATVA contact address


ATVA 2016 gratefully acknowledges the support from the following sponsors:

Gold sponsors:

Silver sponsors: