Abstract is missing.
- Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test PatternsMasahiro Fujita. 3-10 [doi]
- Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive AggregationsAlessandro Abate, Milan Ceska, Marta Kwiatkowska. 13-31 [doi]
- Optimizing the Expected Mean Payoff in Energy Markov Decision ProcessesTomás Brázdil, Antonín Kucera, Petr Novotný. 32-49 [doi]
- Parameter Synthesis for Markov Models: Faster Than EverTim Quatmann, Christian Dehnert, Nils Jansen 0001, Sebastian Junges, Joost-Pieter Katoen. 50-67 [doi]
- Bounded Model Checking for Probabilistic ProgramsNils Jansen 0001, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. 68-85 [doi]
- How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?Radu Iosif, Arnaud Sangnier. 89-105 [doi]
- Solving Language Equations Using Flanked AutomataFlorent Avellaneda, Silvano Dal-Zilio, Jean-Baptiste Raclet. 106-121 [doi]
- Spot 2.0 - A Framework for LTL and \omega -Automata ManipulationAlexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, Laurent Xu. 122-129 [doi]
- MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi AutomataSalomon Sickert, Jan Kretínský. 130-137 [doi]
- Synchronous Products of Rewrite SystemsÓscar Martín, Alberto Verdejo, Narciso Martí-Oliet. 141-156 [doi]
- Specifying and Verifying Secrecy in Workflows with Arbitrarily Many AgentsBernd Finkbeiner, Helmut Seidl, Christian Müller 0001. 157-173 [doi]
- Lazy Sequentialization for the Safety Verification of Unbounded Concurrent ProgramsTruc L. Nguyen, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 174-191 [doi]
- Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine SystemsNikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek. 192-208 [doi]
- On Finite Domains in First-Order Linear Temporal LogicDenis Kuperberg, Julien Brunel, David Chemouil. 211-226 [doi]
- Decidability Results for Multi-objective Stochastic GamesRomain Brenguier, Vojtech Forejt. 227-243 [doi]
- A Decision Procedure for Separation Logic in SMTAndrew Reynolds, Radu Iosif, Cristina Serban, Tim King 0001. 244-261 [doi]
- Solving Mean-Payoff Games on the GPUPhilipp J. Meyer, Michael Luttenberger. 262-267 [doi]
- Synthesizing Skeletons for Reactive SystemsBernd Finkbeiner, Hazem Torfah. 271-286 [doi]
- Observational Refinement and Merge for Disjunctive MTSsShoham Ben-David, Marsha Chechik, Sebastián Uchitel. 287-303 [doi]
- Equivalence-Based Abstraction Refinement for \mu HORS Model CheckingXin Li, Naoki Kobayashi 0001. 304-320 [doi]
- Greener Bits: Formal Analysis of Demand ResponseChristel Baier, Sascha Klüppelholz, Hermann de Meer, Florian Niedermeier, Sascha Wunderlich. 323-339 [doi]
- Heuristics for Checking Liveness Properties with Partial Order ReductionsAlexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault. 340-356 [doi]
- Partial-Order Reduction for GPU Model CheckingThomas Neele, Anton Wijs, Dragan Bosnacki, Jaco van de Pol. 357-374 [doi]
- Efficient Verification of Program Fragments: Eager PORPatrick Metzler, Habib Saissi, Péter Bokor, Robin Hesse, Neeraj Suri. 375-391 [doi]
- Skolem Functions for DQBFKarina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker. 395-411 [doi]
- STL Model Checking of Continuous and Hybrid SystemsHendrik Roehm, Jens Oehlerking, Thomas Heinz, Matthias Althoff. 412-427 [doi]
- Clause Sharing and Partitioning for Cloud-Based SMT SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina. 428-443 [doi]
- Symbolic Model Checking for Factored Probabilistic ModelsDavid Deininger, Rayna Dimitrova, Rupak Majumdar. 444-460 [doi]
- A Sketching-Based Approach for Debugging Using Test CasesJinru Hua, Sarfraz Khurshid. 463-478 [doi]
- Polynomial Invariants by Linear AlgebraSteven de Oliveira, Saddek Bensalem, Virgile Prevosto. 479-494 [doi]
- Certified Symbolic ExecutionRui Qiu, Corina S. Pasareanu, Sarfraz Khurshid. 495-511 [doi]
- Tighter Loop Bound AnalysisPavel Cadek, Jan Strejcek, Marek Trtík. 512-527 [doi]