ABSTRACT. The fundamental maximum-flow problem gets as input a flow network with a source vertex and a target vertex, and searches for a maximal flow from the source to the target. We consider several extensions to the problem, corresponding to rich settings in which the problem is applied. The extensions are well studied in the context of formal verification and the algorithmic problem of model checking, but are new to classical graph-theory problems, and in particular to the maximum-flow problem. The extensions we study include (1) labeled networks, where the edges of the network are labeled by letters from some alphabet, and flow is restricted to travel only along paths that satisfy a given specification, (2) network games, where the vertices of the network are partitioned among selfish players, each directing flow that arrives to vertices she owns, aiming to maximize the flow that reaches her target, and (3) hierarchical networks, which are succinctly represented, and where the goal is to find a maximum flow by reasoning about the succinct representation.

ABSTRACT. We consider an extension of the two-variable, first-order logic with counting quantifiers and arbitrary many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

ABSTRACT. We give a new proof that the axioms of left-handed Kleene algebra are complete with respect to language containments. This proof is significantly simpler than both the proof of Boffa (which relies on Krob's completeness result), and the more recent proof of Kozen and Silva. Our proof builds on a recent non-wellfounded sequent calculus which makes it possible to explicitly compute the invariants required for left-handed Kleene algebra.

ABSTRACT. Building a verified proof assistant entails implementing and mechanizing the concept of a library, as well as adding support for standard manipulations on it. In this work we develop such mechanism for the Nuprl proof assistant, and integrate it into the formalization of Nuprl’s theory in Coq. We formally verify that standard operations on the library preserve its validity. This is a key property for any interactive theorem prover, since it ensures consistency. Some unique features of Nuprl, such as the presence of undefined abstractions, make the proof of this property nontrivial. Thus, e.g., to achieve monotonicity the semantics of sequents had to be refined. On a broader view, this work provides a backend for a verified version of Nuprl. We use it, in turn, to develop a tool that converts proofs exported from the Nuprl proof assistant into proofs in the Coq formalization of Nuprl’s meta-theory, so as to be verified.

ABSTRACT. We introduce and study {\em alternating reachability games with tolls} (ARGTs). An ARGT is a multi-player game played on a directed graph. Each player has a source vertex and a set of target vertices. The vertices of the graph are partitioned among the players. Thus, each player owns a subset of the vertices. In the beginning of the game, each player places a token on her source vertex. Whenever a token reaches a vertex $v$, the owner of the token pays a toll to the owner of vertex $v$, who directs the token to one of the successors of $v$. The objective of each player combines a {\em reachability\/} objective with a {\em minimal-cost maximal-profit\/} objective. For the first, the token of the player needs to reach one of her target vertices. For the second, the player aims at decreasing the toll she pays to other players and increasing the toll paid to her due to visits in vertices she owns. ARGTs model settings in which the vertices are owned by entities who also use the network; for example, communication networks in which service providers own the routers and send messages. ARGTs also offer an extension of rational synthesis with rewards to actions. To the best of our knowledge, this model is the first to combine behavioral and revenue objectives.

We study different instances of the game, distinguishing between various network topologies and various levels of overlap among the reachability objectives of the players. We analyze the {\em stability\/} of ARGTs, characterizing instances for which a Nash equilibrium is guaranteed to exist, and studying its inefficiency. We solve the problems of finding {\em optimal strategies\/} for the players and for the society as a whole, and we study the {\em repair\/} of ARGTs that are unstable or suffer from a high price of stability.

ABSTRACT. Erlang is a dynamically typed concurrent functional language of increasing interest in industry and academia. Official Erlang distributions come equipped with Dialyzer, a useful static analysis tool able to anticipate runtime errors by inferring so-called success types, which are overapproximations to the real semantics of expressions. However, Dialyzer exhibits two main weaknesses: on the practical side, its ability to deal with functions that are typically polymorphic is rather poor; and on the theoretical side, a fully developed theory for its underlying type system --comparable to, say, Hindley-Milner system-- does not seem to exist, something that we consider a regrettable circumstance. This work presents a type derivation system to obtain polymorphic success types for Erlang programs, along with correctness results with respect to a suitable semantics for the language.

ABSTRACT. We propose the notion of a Parse Condition---a logical condition that is satisfiable if and only if a given string w can be successfully parsed using a grammar G. Further, we propose an algorithm for building an SMT encoding of such a parse condition for LL(1) grammars and demonstrate its utility by building two applications over it: automated repair of syntax errors in Tiger programs and automated parser synthesis to automatically synthesize LL(1) parsers. We implement our ideas into a tool, Cyclops, that is able to successfully repair 80% of our benchmarks (675 buggy Tiger programs), clocking an average of 30 seconds per repair and synthesize parsers for interesting languages from examples. Like verification conditions (encoding a program in logic) have found widespread applications in program analysis, we believe that Parse Conditions can serve as a foundation for interesting applications in syntax analysis.

ABSTRACT. We present a framework to analyze and verify programs containing loops by using a first-order language of so-called extended expressions. This language can express both functional and temporal properties of loops. We prove soundness and completeness of our framework and use our approach to automate the tasks of partial correctness verification, termination analysis and invariant generation. For doing so, we express the loop semantics as a set of first-order properties over extended expressions and use theorem provers and/or SMT solvers to reason about these properties. Our approach supports full first-order reasoning, including proving program properties with alternation of quantifiers. Our work is implemented in the tool QuIt and successfully evaluated on benchmarks coming from software verification.

ABSTRACT. This article introduces a novel system for deriving upper bounds on the heap-space requirements of functional programs with garbage collection. The space cost model is based on a perfect garbage collector that immediately deallocates memory cells when they become unreachable. Heap-space bounds are derived using type-based automatic amortized resource analysis (AARA), a template-based technique that efficiently reduces bound inference to linear programming. The first technical contribution of the work is a new operational cost semantics that models a perfect garbage collector. The second technical contribution is an extension of AARA to take into account automatic deallocation. A key observation is that deallocation of a perfect collector can be modeled with destructive pattern matching if data structures are used in a linear way. However, the analysis uses destructive pattern matching to accurately model deallocation even if data is shared. The soundness of the extended AARA with respect to the new cost semantics is proven in two parts via an intermediate linear cost semantics. The analysis and the cost semantics have been implemented as an extension to Resource Aware ML (RaML). An experimental evaluation shows that the system is able to derive tight symbolic heap-space bounds for common algorithms. Often the bounds are asymptotic improvements over bounds that RaML derives without taking into account garbage collection.

ABSTRACT. Linear tree constraints are given by pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. Satisfiability of such constraints is at least as hard as solving the Skolem-Mahler-Lech problem. We provide an interesting subcase, for which we prove that satisfiability is decidable. Our decision procedure is based on intricate arguments using automata and combinatorics of words.

Our subcase allows to construct an inference mechanism for resource bounds of object oriented Java-like programs: actual resource bounds can be read off from solutions of tree constraints. So far, only the case of degenerated tree constraints (i.e. lists) was known to be decidable which, however, is insufficient to generally solve the given resource analysis problem. The present paper therefore provides a generalisation to trees of higher degree in order to cover the entire range of constraints encountered by resource analysis.

ABSTRACT. We provide an in-depth study of the knowledge-theoretic aspects of communication in so-called gossip protocols. Pairs of agents communicate by means of calls in order to spread information (so-called secrets) within the group. Depending on the nature of such calls knowledge spreads in different ways within the group. Systematizing existing literature, we identify 18 different types of communication, and model their epistemic effects through corresponding indistinguishability relations. We then provide a classification of these relations and show its usefulness for an epistemic analysis in presence of different communication types. Finally, we explain how to formalise the assumption that the agents have common knowledge of a distributed epistemic gossip protocol.