Abstract is missing.
- Verifying Communicating Multi-pushdown Systems via Split-WidthCyriac Aiswarya, Paul Gastin, K. Narayan Kumar. 1-17 [doi]
- Booster: An Acceleration-Based Verification Framework for Array ProgramsFrancesco Alberti, Silvio Ghilardi, Natasha Sharygina. 18-23 [doi]
- A Bounded Model Checker for SPARK ProgramsCláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto. 24-30 [doi]
- Acceleration of Affine Hybrid TransformationsBernard Boigelot, Frédéric Herbreteau, Isabelle Mainz. 31-46 [doi]
- A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing ProtocolTimothy Bourke, Rob J. van Glabbeek, Peter Höfner. 47-63 [doi]
- Quantitative Verification of Weighted Kripke StructuresPatricia Bouyer, Patrick Gardy, Nicolas Markey. 64-80 [doi]
- Formal Safety Assessment via Contract-Based DesignMarco Bozzano, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta. 81-97 [doi]
- Verification of Markov Decision Processes Using Learning AlgorithmsTomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma. 98-114 [doi]
- Test Coverage Estimation Using Threshold AcceptingThao Dang, Noa Shalev. 115-128 [doi]
- On Time with Minimal Expected Cost!Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, Jakob Haahr Taankvist. 129-145 [doi]
- Fast Debugging of PRISM ModelsChristian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. 146-162 [doi]
- ACME: Automata with Counters, Monoids and EquivalenceNathanaël Fijalkow, Denis Kuperberg. 163-167 [doi]
- Modelling and Analysis of Markov Reward AutomataDennis Guck, Mark Timmer, Hassan Hatefi, Enno Ruijters, Mariëlle Stoelinga. 168-184 [doi]
- Extensional Crisis and Proving IdentityAshutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov. 185-200 [doi]
- Deciding Entailments in Inductive Separation Logic with Tree AutomataRadu Iosif, Adam Rogalewicz, Tomás Vojnar. 201-218 [doi]
- Liveness Analysis for Parameterised Boolean Equation SystemsJeroen J. A. Keiren, Wieger Wesselink, Tim A. C. Willemse. 219-234 [doi]
- Rabinizer 3: Safraless Translation of LTL to Small Deterministic AutomataZuzana Komárková, Jan Kretínský. 235-241 [doi]
- PeCAn: Compositional Verification of Petri Nets Made EasyDinh-Thuan Le, Huu-Vu Nguyen, Van Tinh Nguyen, Phuong-Nam Mai, Bao-Trung Pham-Duy, Thanh Tho Quan, Étienne André, Laure Petrucci, Yang Liu. 242-247 [doi]
- The Context-Freeness Problem Is coNP-Complete for Flat Counter SystemsJérôme Leroux, Vincent Penelle, Grégoire Sutre. 248-263 [doi]
- Efficiently and Completely Verifying Synchronized Consistency ModelsYi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, Peng Wu. 264-280 [doi]
- Symmetry Reduction in Infinite Games with Finite BranchingNicolas Markey, Steen Vester. 281-296 [doi]
- Incremental Encoding and Solving of Cardinality ConstraintsSven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker. 297-313 [doi]
- Formal Verification of Skiplists with Arbitrary Many LevelsAlejandro Sánchez, César Sánchez. 314-329 [doi]
- Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock FreedomDivjyot Sethi, Muralidhar Talupur, Sharad Malik. 330-347 [doi]
- A Game-Theoretic Approach to Simulation of Data-Parameterized SystemsOrna Grumberg, Orna Kupferman, Sarai Sheinvald. 348-363 [doi]
- Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate ParametersGuoxin Su, David S. Rosenblum. 364-379 [doi]
- Symbolic Memory with PointersMarek Trtík, Jan Strejcek. 380-395 [doi]
- Trace Abstraction Refinement for Timed AutomataWeifeng Wang, Li Jiao. 396-410 [doi]
- Statistically Sound Verification and Optimization for Complex SystemsYan Zhang, Sriram Sankaranarayanan, Fabio Somenzi. 411-427 [doi]