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.