Selected Papers of the Conference ''Tools and Algorithms for the Construction and Analysis of Systems'' (TACAS 2013)

Editors: Nir Piterman, Scott A. Smolka

This special issue of the journal Logical Methods in Computer Science (LMCS) contains revised and extended versions of four papers presented at the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), held in Rome, Italy, during the period March 18-21, 2013, as part of the Joint European Conferences on Theory and Practice of Software (ETAPS).

TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The research areas covered by TACAS include, but are not limited to, formal methods, software and hardware specification and verification, static analysis, dynamic analysis, model checking, theorem proving, decision procedures, real-time, hybrid and stochastic systems, communication protocols, programming languages, and software engineering. TACAS provides a venue where common problems, heuristics, algorithms, data structures, and methodologies in these areas can be discussed and explored.

We have invited a total of eight papers to two special issues of the journals LMCS and STTT. The papers were chosen amongst the best papers presented at the conference. We then partitioned these papers according to their relevance to the respective journals. We are grateful to the authors for their contributions, and to the TACAS'13 PC members/reviewers and the referees of this special issue for their thorough and valuable work.

Nir Piterman and Scott Smolka
TACAS 2013 Guest Editors

1. Weighted Pushdown Systems with Indexed Weight Domains

Minamide, Yasuhiko.
The reachability analysis of weighted pushdown systems is a very powerful technique in verification and analysis of recursive programs. Each transition rule of a weighted pushdown system is associated with an element of a bounded semiring representing the weight of the rule. However, we have realized that the restriction of the boundedness is too strict and the formulation of weighted pushdown systems is not general enough for some applications. To generalize weighted pushdown systems, we first introduce the notion of stack signatures that summarize the effect of a computation of a pushdown system and formulate pushdown systems as automata over the monoid of stack signatures. We then generalize weighted pushdown systems by introducing semirings indexed by the monoid and weaken the boundedness to local boundedness.

2. Encoding Monomorphic and Polymorphic Types

Blanchette, Jasmin Christian ; Böhme, Sascha ; Popescu, Andrei ; Smallbone, Nicholas.
Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.

3. On-the-Fly Computation of Bisimilarity Distances

Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim G. ; Mardare, Radu.
We propose a distance between continuous-time Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and on-the-fly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of Desharnais et al. between discrete-time Markov chains as an optimal solution of a linear program that can be solved by using the ellipsoid method. Inspired by their result, we propose a novel linear program characterization to compute the distance in the continuous-time setting. Differently from previous proposals, ours has a number of constraints that is bounded by a polynomial in the size of the CTMC. This, in particular, proves that the distance we propose can be computed in polynomial time. Despite its theoretical importance, the proposed linear program characterization turns out to be inefficient in practice. Nevertheless, driven by the encouraging results of our previous work presented at […]

4. Deriving Probability Density Functions from Probabilistic Functional Programs

Bhat, Sooraj ; Borgström, Johannes ; Gordon, Andrew D. ; Russo, Claudio.
The probability density function of a probability distribution is a fundamental concept in probability theory and a key ingredient in various widely used machine learning methods. However, the necessary framework for compiling probabilistic functional programs to density functions has only recently been developed. In this work, we present a density compiler for a probabilistic language with failure and both discrete and continuous distributions, and provide a proof of its soundness. The compiler greatly reduces the development effort of domain experts, which we demonstrate by solving inference problems from various scientific applications, such as modelling the global carbon cycle, using a standard Markov chain Monte Carlo framework.