LPAR-22: Papers with Abstracts

Abstract. Emission cleaning in modern cars is controlled by embedded software. In this context, the diesel emission scandal has made it apparent that the automotive industry is susceptible to fraudulent behaviour, implemented and effectuated by that control software. Mass effects make the individual controllers altogether have statistically significant adverse effects on people’s health. This paper surveys recent work on the use of rigorous formal techniques to attack this problem. It starts off with an introduction into the dimension and facets of the problem from a software technology perspective. It then details approaches to use (i) model checking for the white-box analysis of the embedded software, (ii) model- based black-box testing to detect fraudulent behaviour under standardized conditions, and (iii) synthesis of runtime monitors for real driving emissions of cars in-the-wild. All these efforts aim at finding ways to eventually ban the problem of doped software, that is, of software that surreptitiously alters its behaviour in certain circumstances – against the interest of the owner or of society.

Abstract. In the traditional maximum-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow into outgoing edges. The problem has been extensively used in order to optimize the performance of networks in numerous application areas. The definition of the problem corresponds to a setting in which the authority has control on all vertices of the network. Today’s computing environment involves parties that should be considered adversarial. We survey recent studies on flow games, which capture settings in which the vertices of the network are owned by different and selfish entities. We start with the case of two players, max (the authority), which aims at maximizing the flow, and min (the hostile environment), which aims at minimizing the flow. We argue that such flow games capture many modern settings, such as partially- controlled pipe or road systems or hybrid software-defined communication networks. We then continue to the special case where all vertices are owned by min. This case captures evacuation scenarios, where the goal is to maximize the flow that is guaranteed to travel in the most unfortunate routing decisions. Finally, we study the general case, of multiple players, each with her own target vertex. In all settings, we study the problems of finding the maximal flows, optimal strategies for the players, as well as stability and equilibrium inefficiency in the case of multi-player games. We discuss additional variants and their applications, and point to several interesting open problems.

Abstract. Complex Event Processing (CEP) systems have appeared in abundance during the last two decades. Their purpose is to detect in real–time interesting patterns upon a stream of events and to inform an analyst for the occurrence of such patterns in a timely manner. However, there is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CEP engine. We present Wayeb, a tool that attempts to address the issue of Complex Event Forecasting. Wayeb employs symbolic automata as a computational model for pattern detection and Markov chains for deriving a probabilistic description of a symbolic automaton.

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.

Abstract. SMT-based program verification can achieve high precision using bit-precise models or combinations of different theories. Often such approaches suffer from problems related to scalability due to the complexity of the underlying decision procedures. Precision is traded for performance by increasing the abstraction level of the model. As the level of abstraction increases, missing important details of the program model becomes problematic. In this paper we address this problem with an incremental verification approach that alternates precision of the program modules on demand. The idea is to model a program using the lightest possible (i.e., less expensive) theories that suffice to verify the desired property. To this end, we employ safe over-approximations for the program based on both function summaries and light-weight SMT theories. If during verification it turns out that the precision is too low, our approach lazily strengthens all affected summaries or the theory through an iterative refinement procedure. The resulting summarization framework provides a natural and light-weight approach for carrying information between different theories. An experimental evaluation with a bounded model checker for C on a wide range of benchmarks demonstrates that our approach scales well, often effortlessly solving instances where the state-of-the-art model checker CBMC runs out of time or memory.

Abstract. Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics two decades ago, motivated by applications in the Classic system. Shortly afterwards, a polynomial-time matching algorithm was developed for the DL FL0. However, this algorithm cannot deal with general TBoxes (i.e., finite sets of general concept inclusions). Here we show that matching in FL0 w.r.t. general TBoxes is in ExpTime, which is the best possible complexity for this problem since already subsumption w.r.t. general TBoxes is ExpTime-hard in FL0. We also show that, w.r.t. a restricted form of TBoxes, the complexity of matching in FL0 can be lowered to PSpace.

Abstract. First-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more or less obvious. One of the most prominent examples is first-order G ̈odel logic. Lyndon interpolation is a strengthening of the interpolation property in the sense that propositional variables or predicate symbols are only allowed to occur positively (negatively) in the interpolant if they occur positively (negatively) on both sides of the implication. Note that Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail. In this paper we provide general derivability conditions for a first-order logic to admit Lyndon interpolation for the prenex ⊃ prenex fragment and apply the arguments to the prenex ⊃ prenex fragment of first-order Go ̈del logic.

Abstract. Linear tree constraints are given by pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. Satisfiablity 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 satisfiablity 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. In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i.e., one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches.
In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evalu- ation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.

Abstract. There are various types of automata on infinite words, differing in their acceptance conditions. The most classic ones are weak, Bu ̈chi, co-Bu ̈chi, parity, Rabin, Streett, and Muller. This is opposed to the case of automata on finite words, in which there is only one standard type. The natural question is why—Why not a single type? Why these particular types? Shall we further look into additional types?
For answering these questions, we clarify the succinctness of the different automata types and the size blowup involved in performing boolean operations on them. To this end, we show that unifying or intersecting deterministic automata of the classic ω-regular- complete types, namely parity, Rabin, Streett, and Muller, involves an exponential size blowup.
We argue that there are good reasons for the classic types, mainly in the case of nondeterministic and alternating automata. They admit good size and complexity bounds with respect to succinctness, boolean operations, and decision procedures, and they are closely connected to various logics.
Yet, we also argue that there is place for additional types, especially in the case of deterministic automata. In particular, generalized-Rabin, which was recently introduced, as well as a disjunction of Streett conditions, which we call hyper-Rabin, where the latter further generalizes the former, are interesting to consider. They may be exponentially more succinct than the classic types, they allow for union and intersection with only a quadratic size blowup, and their nonemptiness can be checked in polynomial time.

Abstract. The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximately solves an NP-hard problem. The algorithm has several applications in number theory, computer algebra and cryptography.
Recently, the first mechanized soundness proof of the LLL algorithm has been developed in Isabelle/HOL. However, this proof did not include a formal statement of the algorithm’s complexity. Furthermore, the resulting implementation was inefficient in practice.
We address both of these shortcomings in this paper. First, we prove the correctness of a more efficient implementation of the LLL algorithm that uses only integer computations. Second, we formally prove statements on the polynomial running-time.

Abstract. In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formula. To avoid combinatorial explosion, the Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, the polarity of the sub-formula Φ is taken into account leading to conditional constraints of the form y → Φ, or Φ → y, where y is a fresh propositional variable. In the case where Φ represents a cardinality constraint, such translation leads to conditional cardinality constraints subject of the present paper. We first show that when all the clauses encoding the cardinality constraint are augmented with an additional new variable, most of the well-known encodings cease to maintain the generalized arc-consistency property. Then, we consider some of these encodings and show how they can be extended to recover such important property. An experimental validation is conducted on a SAT-based pattern mining application, where such conditional cardinality constraints are a cornerstone, showing the relevance of our proposed approach.

Abstract. In this paper we introduce a prioritized default logic. We build this logic modularly from Standard Deontic Logic by the addition of default rules and priorities among them. Our main aim is to provide a logical framework to reason about scenarios where prescriptive and descriptive statements coexist and may be incomplete and contradictory. We motivate and illustrate the technical elements of our work with the use of examples (classical, and coming from software engineering). In addition, we present sound, complete, and terminating (with loop check) tableau-based proof calculi for credulous and sceptical reasoning in our logic.

Abstract. We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily 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. Solving parity games, which are equivalent to modal μ-calculus model checking, is a central algorithmic problem in formal methods, with applications in reactive synthesis, program repair, verification of branching-time properties, etc. Besides the standard compu- tation model with the explicit representation of games, another important theoretical model of computation is that of set-based symbolic algorithms. Set-based symbolic algorithms use basic set operations and one-step predecessor operations on the implicit description of games, rather than the explicit representation. The significance of symbolic algorithms is that they provide scalable algorithms for large finite-state systems, as well as for infinite-state systems with finite quotient. Consider parity games on graphs with n vertices and parity conditions with d priorities. While there is a rich literature of explicit algorithms for parity games, the main results for set-based symbolic algorithms are as follows: (a) the basic algorithm that requires O(nd) symbolic operations and O(d) symbolic space; and (b) an improved algorithm that requires O(nd/3+1) symbolic operations and O(n) symbolic space. In this work, our contributions are as follows: (1) We present a black-box set-based symbolic algorithm based on the explicit progress measure algorithm. Two important consequences of our algorithm are as follows: (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially many symbolic operations and O(n) symbolic space; and (b) any future improvement in progress measure based explicit algorithms immediately imply an efficiency improvement in our set-based symbolic algorithm for parity games. (2) We present a set-based symbolic algorithm that requires quasi-polynomially many symbolic operations and O(d · log n) symbolic space. Moreover, for the important special case of d ≤ log n, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.

Abstract. In 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic setting. We investigate Abramsky’s models from the point of view of the model theory of λ-calculus, focusing on the purely linear and affine fragments of Abramsky’s Combinatory Algebras.
Our approach stems from realizing a structural analogy, which had not been hitherto pointed out in the literature, between the partial involution interpreting a combinator and the principal type of that term, with respect to a simple types discipline for λ-calculus. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction (GoI).
Our approach provides immediately an answer to the open problem, raised by Abram- sky, of characterising those finitely describable partial involutions which are denotations of combinators, in the purely affine fragment. We prove also that the (purely) linear combinatory algebra of partial involutions is a (purely) linear λ-algebra, albeit not a combinatory model, while the (purely) affine combinatory algebra is not. In order to check the complex equations involved in the definition of affine λ-algebra, we implement in Erlang the compilation of λ-terms as involutions, and their execution.

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. Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more complex controls such as aggressive maneuvering or performing fuel-efficient controls. Another approach called optimal control is capable of computing such difficult trajectories but lacks the ability to adapt to dynamic changes in the environment. In both cases, the control was designed offline, relying on more or less complex algorithms to find the appropriate parameters. More recent kinds of approaches such as Linear Model-Predictive Control (MPC) rely on the online use of convex optimization to compute the best control at each sample time. In these settings optimization algorithms are specialized for the specific control problem and embed on the device.
This paper proposes to revisit the code generation of an interior point method (IPM) algorithm, an efficient family of convex optimization, focusing on the proof of its implementation at code level. Our approach relies on the code specialization phase to produce additional annotations formalizing the intended specification of the algorithm. Deductive methods are then used to prove automatically the validity of these assertions. Since the algorithm is complex, additional lemmas are also produced, allowing the complete proof to be checked by SMT solvers only.
This work is the first to address the effective formal proof of an IPM algorithm. The approach could also be generalized more systematically to code generation frameworks, producing proof certificate along the code, for numerical intensive software.

Abstract. We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

Abstract. The weak completion semantics is an integrated and computational cognitive theory which is based on normal logic programs,three-valued Lukasiewicz logic, weak completion, and skeptical abduction. It has been successfully applied – among others – to the suppression task, the selection task, and to human syllogistic reasoning. In order to solve ethical decision problems like – for example – trolley problems, we need to extend the weak completion semantics to deal with actions and causality. To this end we consider normal logic programs and a set E of equations as in the fluent calculus. We formally show that normal logic programs with equality admit a least E-model under the weak completion semantics and that this E-model can be computed as the least fixed point of an associated semantic operator. We show that the operator is not continuous in general, but is continuous if the logic program is a propositional, a finite-ground, or a finite datalog program and the Herbrand E-universe is finite. Finally, we show that the weak completion semantics with equality can solve a variety of ethical decision problems like the bystander case, the footbridge case, and the loop case by computing the least E-model and reasoning with respect to this E-model. The reasoning process involves counterfactuals which is necessary to model the different ethical dilemmas.

Abstract. The computational bottleneck in model-checking applications is the blow-up involved in the translation of systems to their mathematical model. This blow up is especially painful in systems with variables over an infinite domain, and in composite systems described by means of their underlying components. We introduce and study linear temporal logic with arithmetic (LTLA, for short), where formulas include variables that take values in Z, and in which linear arithmetic over these values is supported. We develop an automata-theoretic approach for reasoning about LTLA formulas and use it in order to solve, in PSPACE, the satisfiability problem for the existential fragment of LTLA and the model-checking problem for its universal fragment. We show that these results are tight, as a single universally- quantified variable makes the satisfiability problem for LTLA undecidable.
In addition to reasoning about systems with variables over Z, we suggest applications of LTLA in reasoning about hierarchical systems, which consist of subsystems that can call each other in a hierarchical manner. We use the values in Z in order to describe the nesting depth of components in the system. A naive model-checking algorithm for hierarchical systems flattens them, which involves an exponential blow up. We suggest a model-checking algorithm that avoids the flattening and avoids a blow up in the number of components.

Abstract. The theory of arrays has a central place in software verification due to its ability to model memory or data structures. Yet, this theory is known to be hard to solve in both theory and practice, especially in the case of very long formulas coming from unrolling-based verification methods. Standard simplification techniques à la read-over-write suffer from two main drawbacks: they do not scale on very long sequences of stores and they miss many simplification opportunities because of a crude syntactic (dis-)equality reasoning. We propose a new approach to array formula simplification based on a new dedicated data structure together with original simplifications and low-cost reasoning. The technique is efficient, scalable and it yields significant simplification. The impact on formula resolution is always positive, and it can be dramatic on some specific classes of problems of interest, e.g. very long formula or binary-level symbolic execution. While currently implemented as a preprocessing, the approach would benefit from a deeper integration in an array solver.

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. We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Abstract. The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.

Abstract. In this paper we develop a cyclic proof system for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions are quantifier-free formulae of first order logic. The proof system consists of a small set of inference rules, inspired by a top-down language inclusion algorithm for tree automata [9]. We show the proof system to be sound, in general, and complete, under certain semantic restrictions involving the set of constraints in the inductive system. Moreover, we investigate the computational complexity of checking these restrictions, when the function symbols in the logic are given the canonical Herbrand interpretation.

Abstract. Finite model finders represent a powerful tool for deciding problems with the finite model property, such as the Bernays-Sch ̈onfinkel fragment (EPR). Further, finite model finders provide useful information for counter-satisfiable conjectures. The paper investigates several novel techniques in a finite model-finder based on the translation to SAT, referred to as the MACE-style approach. The approach we propose is driven by counterexample abstraction refinement (CEGAR), which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF).
One weakness of CEGAR-based approaches is that certain amount of luck is required in order to guess the right model, because the solver always operates on incomplete information about the formula. To tackle this issue, we propose to enhance the model finder with a machine learning algorithm to improve the likelihood that the right model is encountered. The implemented prototype based on the presented ideas shows highly promising results.

Abstract. A complementary technique to decision-diagram-based model checking is SAT-based bounded model checking (BMC), which reduces the model checking problem to a propositional satisfiability problem so that the corresponding formula is satisfiable iff a counterexample or witness exists. Due to the branching time nature of computation tree logic (CTL), BMC for the universal fragment of CTL (ACTL) considers a counterexample in a bounded model as a set of bounded paths. Since the existential fragment of CTL (ECTL) is dual to ACTL, and ACTL formulas are often negated to obtain ECTL ones in practice, we focus on BMC for ECTL and propose an improved translation that generates a possibly smaller propositional formula by reducing the number of bounded paths to be considered in a witness. Experimental results show that the formulas generated by our approach are often easier for a SAT solver to answer. In addition, we propose a simple modification to the translation so that it is also defined for models with deadlock states.

Abstract. In general, deciding satisfiability of quantified bit-vector formulas becomes harder with increasing maximal allowed bit-width of variables and constants. However, this does not have to be the case for formulas that come from practical applications. For example, software bugs often do not depend on the specific bit-width of the program variables and would manifest themselves also with much lower bit-widths. We experimentally evaluate this thesis and show that satisfiability of the vast majority of quantified bit-vector formulas from the smt-lib repository remains the same even after reducing bit-widths of variables to a very small number. This observation may serve as a starting-point for development of heuristics or other techniques that can improve performance of smt solvers for quantified bit-vector formulas.

Abstract. We introduce and study 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 reachability objective with a 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 stability of ARGTs, characterizing instances for which a Nash equilibrium is guaranteed to exist, and studying its inefficiency. We also analyze the problems of finding optimal strategies for the players and for the society as a whole.

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. The inherent complexity of parallel computing makes development, resource monitor- ing, and debugging for parallel constraint-solving-based applications difficult. This paper presents SMTS, a framework for parallelizing sequential constraint solving algorithms and running them in distributed computing environments. The design (i) is based on a gen- eral parallelization technique that supports recursively combining algorithm portfolios and divide-and-conquer with the exchange of learned information, (ii) provides monitoring by visually inspecting the parallel execution steps, and (iii) supports interactive guidance of the algorithm through a web interface. We report positive experiences on instantiating the framework for one SMT solver and one IC3 solver, debugging parallel executions, and visualizing solving, structure, and learned clauses of SMT instances.

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. 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 meta-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 study the semantics of propositional interference-based proof systems such as DRAT and DPR. These are characterized by modifying a CNF formula in ways that preserve satisfiability but not necessarily logical truth. We propose an extension of propositional logic called overwrite logic with a new construct which captures the meta-level reasoning behind interferences. We analyze this new logic from the point of view of expressivity and complexity, showing that while greater expressivity is achieved, the satisfiability problem for overwrite logic is essentially as hard as SAT, and can be reduced in a way that is well-behaved for modern SAT solvers. We also show that DRAT and DPR proofs can be seen as overwrite logic proofs which preserve logical truth. This much stronger invariant than the mere satisfiability preservation maintained by the traditional view gives us better understanding on these practically important proof systems. Finally, we showcase this better understanding by finding intrinsic limitations in interference-based proof systems.

Abstract. Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidabil- ity and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Represen- tation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that, in the absence of equality, satisfiability in TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.

Abstract. Uniform sampling has drawn diverse applications in programming languages and software engineering, like in constrained-random verification (CRV), constrained-fuzzing and bug synthesis. The effectiveness of these applications depend on the uniformity of test stimuli generated from a given set of constraints. Despite significant progress over the past few years, the performance of the state of the art techniques still falls short of those of heuristic methods employed in the industry which sacrifice either uniformity or scalability when generating stimuli.
In this paper, we propose a new approach to the uniform generation that builds on recent progress in knowledge compilation. The primary contribution of this paper is marrying knowledge compilation with uniform sampling: our algorithm, KUS, employs the state-of-the-art knowledge compilers to first compile constraints into d-DNNF form, and then, generates samples by making two passes over the compiled representation.
We show that KUS is able to significantly outperform existing state-of-the-art algorithms, SPUR and UniGen2, by up to 3 orders of magnitude in terms of runtime while achieving a geometric speedup of 1.7× and 8.3× over SPUR and UniGen2 respectively. Also, KUS achieves a lower PAR-21 score, around 0.82× that of SPUR and 0.38× that of UniGen2. Furthermore, KUS achieves speedups of up to 3 orders of magnitude for incremental sampling. The distribution generated by KUS is statistically indistinguishable from that generated by an ideal uniform sampler. Moreover, KUS is almost oblivious to the number of samples requested.

Abstract. In this work, 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 parse conditions 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 from examples. 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. The paper describes a practical software tool for the verification of integer arithmetic circuits. It covers different types of integer multipliers, fused add-multiply circuits, and constant dividers - in general, circuits whose computation can be represented as a polynomial. The verification uses an algebraic model of the circuit and is accomplished by rewriting the polynomial of the binary encoding of the primary outputs (output signature), using the polynomial models of the logic gates, into a polynomial over the primary inputs (input signature). The resulting polynomial represents arithmetic function implemented by the circuit and hence can be used to extract functional specification from its gate-level implementation. The rewriting uses an efficient And-Inverter Graph (AIG) representation to enable extraction of the essential arithmetic components of the circuit. The tool is integrated with the popular ABC system. Its efficiency is illustrated with impressive results for integer multipliers, fused add-multiply circuits, and divide-by-constant circuits. The entire verification system is offered in an open source ABC environment together with an extensive set of benchmarks.