Skip to main content
  • Conference proceedings
  • © 2013

Tools and Algorithms for the Construction and Analysis of Systems

19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings

  • Up-to-date results in tools and algorithms for the construction and analysis of systems
  • Fast-track conference proceedings
  • State-of-the-art research

Conference proceedings info: TACAS 2013.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (53 papers)

  1. Front Matter

  2. Markov Chains

    1. On-the-Fly Exact Computation of Bisimilarity Distances

      • Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare
      Pages 1-15
    2. The Quest for Minimal Quotients for Probabilistic Automata

      • Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang
      Pages 16-31
    3. LTL Model Checking of Interval Markov Chains

      • Michael Benedikt, Rastislav Lenhardt, James Worrell
      Pages 32-46
  3. Termination

    1. Ramsey vs. Lexicographic Termination Proving

      • Byron Cook, Abigail See, Florian Zuleger
      Pages 47-61
    2. Structural Counter Abstraction

      • Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey
      Pages 62-77
  4. Quantifier Elimination

    1. Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

      • Ajith K. John, Supratik Chakraborty
      Pages 78-92
  5. SAT/SMT

    1. The MathSAT5 SMT Solver

      • Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
      Pages 93-107
    2. Formula Preprocessing in MUS Extraction

      • Anton Belov, Matti Järvisalo, Joao Marques-Silva
      Pages 108-123
    3. Proof Tree Preserving Interpolation

      • Jürgen Christ, Jochen Hoenicke, Alexander Nutz
      Pages 124-138
    4. Asynchronous Multi-core Incremental SAT Solving

      • Siert Wieringa, Keijo Heljanko
      Pages 139-153
  6. Games and Synthesis

    1. Model-Checking Iterated Games

      • Chung-Hao Huang, Sven Schewe, Farn Wang
      Pages 154-168
    2. Synthesis from LTL Specifications with Mean-Payoff Objectives

      • Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin
      Pages 169-184
    3. PRISM-games: A Model Checker for Stochastic Multi-Player Games

      • Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, Aistis Simaitis
      Pages 185-191
  7. Process Algebra

    1. An Overview of the mCRL2 Toolset and Its Recent Advances

      • Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink et al.
      Pages 199-213
  8. Pushdown Systems Boolean/Integer Programs

    1. Analysis of Boolean Programs

      • Patrice Godefroid, Mihalis Yannakakis
      Pages 214-229
    2. Underapproximation of Procedure Summaries for Integer Programs

      • Pierre Ganty, Radu Iosif, Filip Konečný
      Pages 245-259
  9. Runtime Verification and Model Checking

    1. Runtime Verification Based on Register Automata

      • Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos
      Pages 260-276

Other Volumes

  1. Tools and Algorithms for the Construction and Analysis of Systems

About this book

This book constitutes the proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held in Rome, Italy, in March 2013. The 42 papers presented in this volume were carefully reviewed and selected from 172 submissions. They are organized in topical sections named: Markov chains; termination; SAT/SMT; games and synthesis; process algebra; pushdown; runtime verification and model checking; concurrency; learning and abduction; timed automata; security and access control; frontiers (graphics and quantum); functional programs and types; tool demonstrations; explicit-state model checking; Büchi automata; and competition on software verification.

Editors and Affiliations

  • Department of Computer Science, University of Leicester, Leicester, UK

    Nir Piterman

  • Department of Computer Science, State University of New York at Stony Brook, Stony Brook, USA

    Scott A. Smolka

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access