


default search action
14th ATVA 2016: Chiba, Japan
- Cyrille Artho, Axel Legay, Doron Peled:

Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Lecture Notes in Computer Science 9938, 2016, ISBN 978-3-319-46519-7
Keynote
- Masahiro Fujita:

Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns. 3-10
Markov Models, Chains, and Decision Processes
- Alessandro Abate, Milan Ceska

, Marta Kwiatkowska:
Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. 13-31 - Tomás Brázdil, Antonín Kucera

, Petr Novotný
:
Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. 32-49 - Tim Quatmann

, Christian Dehnert, Nils Jansen
, Sebastian Junges, Joost-Pieter Katoen:
Parameter Synthesis for Markov Models: Faster Than Ever. 50-67 - Nils Jansen

, Christian Dehnert, Benjamin Lucien Kaminski
, Joost-Pieter Katoen, Lukas Westhofen
:
Bounded Model Checking for Probabilistic Programs. 68-85
Counter Systems, Automata
- Radu Iosif, Arnaud Sangnier

:
How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? 89-105 - Florent Avellaneda, Silvano Dal-Zilio

, Jean-Baptiste Raclet:
Solving Language Equations Using Flanked Automata. 106-121 - Alexandre Duret-Lutz

, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault
, Laurent Xu:
Spot 2.0 - A Framework for LTL and \omega -Automata Manipulation. 122-129 - Salomon Sickert

, Jan Kretínský:
MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata. 130-137
Parallelism, Concurrency
- Óscar Martín

, Alberto Verdejo
, Narciso Martí-Oliet
:
Synchronous Products of Rewrite Systems. 141-156 - Bernd Finkbeiner, Helmut Seidl, Christian Müller:

Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. 157-173 - Truc L. Nguyen, Bernd Fischer

, Salvatore La Torre, Gennaro Parlato
:
Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. 174-191 - Nikola Benes

, Lubos Brim
, Martin Demko, Samuel Pastva
, David Safránek
:
Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems. 192-208
Complexity, Decidability
- Denis Kuperberg, Julien Brunel, David Chemouil

:
On Finite Domains in First-Order Linear Temporal Logic. 211-226 - Romain Brenguier, Vojtech Forejt:

Decidability Results for Multi-objective Stochastic Games. 227-243 - Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King:

A Decision Procedure for Separation Logic in SMT. 244-261 - Philipp J. Meyer

, Michael Luttenberger:
Solving Mean-Payoff Games on the GPU. 262-267
Synthesis, Refinement
- Bernd Finkbeiner, Hazem Torfah

:
Synthesizing Skeletons for Reactive Systems. 271-286 - Shoham Ben-David, Marsha Chechik, Sebastián Uchitel

:
Observational Refinement and Merge for Disjunctive MTSs. 287-303 - Xin Li, Naoki Kobayashi

:
Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. 304-320
Optimization, Heuristics, Partial-Order Reductions
- Christel Baier

, Sascha Klüppelholz
, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich:
Greener Bits: Formal Analysis of Demand Response. 323-339 - Alexandre Duret-Lutz

, Fabrice Kordon, Denis Poitrenaud, Etienne Renault
:
Heuristics for Checking Liveness Properties with Partial Order Reductions. 340-356 - Thomas Neele

, Anton Wijs
, Dragan Bosnacki, Jaco van de Pol:
Partial-Order Reduction for GPU Model Checking. 357-374 - Patrick Metzler, Habib Saissi, Péter Bokor, Robin Hesse, Neeraj Suri

:
Efficient Verification of Program Fragments: Eager POR. 375-391
Solving Procedures, Model Checking
- Karina Wimmer, Ralf Wimmer

, Christoph Scholl, Bernd Becker
:
Skolem Functions for DQBF. 395-411 - Hendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff:

STL Model Checking of Continuous and Hybrid Systems. 412-427 - Matteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina

:
Clause Sharing and Partitioning for Cloud-Based SMT Solving. 428-443 - David Deininger, Rayna Dimitrova, Rupak Majumdar:

Symbolic Model Checking for Factored Probabilistic Models. 444-460
Program Analysis
- Jinru Hua, Sarfraz Khurshid:

A Sketching-Based Approach for Debugging Using Test Cases. 463-478 - Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

:
Polynomial Invariants by Linear Algebra. 479-494 - Rui Qiu, Corina S. Pasareanu, Sarfraz Khurshid:

Certified Symbolic Execution. 495-511 - Pavel Cadek, Jan Strejcek

, Marek Trtík:
Tighter Loop Bound Analysis. 512-527

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














