ABSTRACT. An autarky for a formula in propositional logic is a truth assignment that satisfies every clause it touches, i.e., every clause for which the autarky assigns at least one variable. In this paper, we present how conditional autarkies, a generalization of autarkies, give rise to novel preprocessing techniques for SAT solving. We show that conditional autarkies correspond to a new type of redundant clauses, termed globallyblocked clauses, and that the elimination of these clauses can simulate existing circuit-simplification techniques on the CNF level.

ABSTRACT. One of the main challenges in the analysis of probabilistic programs is to compute invariant properties that summarise loop behaviours. Automation of invariant generation is still at its infancy and most of the times targets only expected values of the program variables, which is insufficient to recover the full probabilistic program behaviour. We present a method to automatically generate moment-based invariants of a subclass of probabilistic programs, called Prob-solvable loops, with polynomial assignments over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values or variances, of program variables. We successfully evaluated our work on several examples where full automation for computing higher-order moments and invariants over program variables was not yet possible.

ABSTRACT. We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. This has led to an improvement of the running times as well as accuracy of the framework. We have demonstrated the competitiveness of the entire framework on benchmarks from the literature.

ABSTRACT. In this paper, we present a fully automated approach for synthesizing fast numerical kernels with guaranteed error bounds. The kernels we target contain elementary functions such as sine and logarithm, which are widely used in scientific computing, embedded as well as machine-learning programs. However, standard library implementations of these functions are often overly accurate and therefore unnecessarily expensive. Our approach trades superfluous accuracy against performance by approximating elementary function calls by polynomials and by implementing arithmetic operations in low-precision fixed-point arithmetic. Our algorithm soundly distributes and guarantees an overall error budget specified by the user. The evaluation on benchmarks from different domains shows significant performance improvements of 2.23x on average compared to state-of-the-art implementations of such kernel functions.

ABSTRACT. In this work, we present multiple new optimizations and heuristics for the determinization of Büchi automata that exploit a number of semantic and structural properties, most of which may be applied together with any determinization procedure. We built a prototype implementation where all the presented heuristics can be freely combined and evaluated them, comparing our implementation with the state-of-the-art tool spot on multiple data sets with different characteristics. Our results show that the proposed optimizations and heuristics can in some cases significantly decrease the size of the resulting deterministic automaton.

ABSTRACT. Omega-automata play a key role in verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two characteristics: the accepting condition and the determinism (e.g., deterministic or nondeterministic) of an automaton. These characteristics play a crucial role in applications of automata theory. For example, certain accepting conditions can be handled more efficiently than others by dedicated tools and algorithms. Furthermore, some applications, such as synthesis and probabilistic model checking, require that properties are represented as some type of deterministic omega-automata. However, properties cannot always be represented by automata with the desired accepting condition and determinism.

In this paper we study the problem of approximating linear-time properties by automata in a given class. Our approximation is based on preserving the language up to a user-defined precision given in terms of the size of the finite lasso representation of infinite executions that are preserved. We study the state-complexity of different types of approximating automata, and provide constructions for the approximation within different automata classes, for example, for approximating a given automaton by one with a simpler accepting condition.

ABSTRACT. Register automata are one of the most studied automata models over infinite alphabets with applications in learning, systems modelling and program verification. We present an equivalence checker for deterministic register automata, called DEQ, based on a recent polynomial-time algorithm that employs group-theoretic techniques to achieve succinct representations of the search space. We compare the performance of our tool to other available implementations, notably the learning library RALib and nominal frameworks LOIS and NLambda.

ABSTRACT. The paper presents a new tool ltl3tela translating LTL to deterministic or nondeterministic transition-based Emerson-Lei automata (TELA). The tool combines algorithms of Spot library, a new translation of LTL to TELA via alternating automata, a pattern-based automata reduction method, and few other heuristics. Experimental evaluation shows that ltl3tela can produce deterministic automata that are, on average, noticeably smaller than deterministic TELA produced by state-of-the-art translators Delag, Rabinizer 4, and Spot. For nondeterministic automata, the improvement over Spot is smaller, but still measurable.

ABSTRACT. The manual implementation of distributed systems is an error-prone task because of the asynchronous interplay of components and the environment. Bounded synthesis automatically generates an implementation for the specification of the distributed system if one exists. So far, bounded synthesis for distributed systems does not utilize their asynchronous nature. Instead, concurrent behavior of components is encoded by all interleavings and only then checked against the specification. We close this gap by identifying true concurrency in synthesis of asynchronous distributed systems represented as Petri games. This defines when several interleavings can be subsumed by one true concurrent trace. Thereby, fewer and shorter verification problems have to be solved in each iteration of the bounded synthesis algorithm. For Petri games, experimental results show that our implementation using true concurrency outperforms the implementation based on checking all interleavings.

ABSTRACT. We present an approach to synthesize glue code for graphical user interfaces. Such code starts computation and I/O threads in response to user interface events and changes the state of the interface according to the interaction scheme envisioned by the UI designer.

Our approach combines several ideas that work best in combination. For instance, by translating all specification parts to universal very-weak (UVW) automata and building a game from them, we obtain a natural order over the positions in the game that enable us to prune it substantially while constructing the game graph. Furthermore, we present an approach to compute kind strategies that constrain the environment as little as possible and hence make the UIs as responsive as possible. The use of UVWs gives rise to a simple formalization of this idea.

We apply our approach to a case study with an Android application and show experimentally that previous synthesis tools are unable to handle the specification.

ABSTRACT. We propose ''semantic labelling'' as a novel ingredient for solving games in the context of LTL synthesis. It exploits recent advances in the automata-based approach, yielding more information for each state of the generated parity game than the game graph can capture. We utilize this extra information to improve standard approaches as follows. (i) Compared to strategy iteration (SI) with random initial strategy, a more informed initialization often yields a winning strategy directly without any computation. (ii) This initialization makes SI also yield smaller solutions. (iii) While Q-learning on the game graph turns out not too efficient, Q-learning with the semantic information becomes competitive to SI. Since already the simplest heuristics achieve significant improvements the experimental results demonstrate the utility of semantic labelling. This extra information opens the door to more advanced learning approaches both for initialization and improvement of strategies.

ABSTRACT. We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class of properties includes information flow policies like noninterference and observational determinism. The repair problem is to find, for a given Kripke structure, a substructure that satisfies a given specification. We show that the repair problem is decidable for HyperLTL specifications and finite-state Kripke structures. We provide a detailed complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures.