ABSTRACT. In the classical {\em synthesis\/} problem, we are given an LTL formula $\psi$ over sets of input and output signals, and we synthesize a system $\T$ that {\em realizes}~$\psi$: with every input sequences $x$, the system associates an output sequence $\T(x)$ such that the generated computation $x \otimes \T(x)$ satisfies $\psi$. In practice, the requirement to satisfy the specification in all environments is often too strong, and it is common to add assumptions on the environment. We introduce and study a new type of relaxation on this requirement. In \emph{optimal synthesis}, the system is required to generate a satisfying computation only if one exists. Formally, an input sequence $x$ is \emph{hopeful} if there exists some output sequence $y$ such that the computation $x \otimes y$ satisfies $\psi$, and a system optimally-realizes $\psi$ if it generates a computation that satisfies $\psi$ on all hopeful input sequences. Optimal synthesis is particularly relevant when the notion of correctness is {\em multi-valued} (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing {\em autonomous systems}, which interact with unexpected environments and are often only expected to do their best.

We study optimal synthesis in Boolean and high-quality settings. In both, we suggest and solve various definitions of optimal synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, optimal synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that optimally realize their specifications by monitors that provide satisfaction information. In the high-quality setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.

ABSTRACT. We present TarTar, an automatic repair analysis tool that, given a timed diagnostic trace (TDT) obtained during the model checking of a timed automaton model, suggests possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. The proposed repairs are guaranteed to eliminate executability of the given TDT, while preserving the overall functional behavior of the system. We give insights into the design and architecture of TarTar, and show that it can successfully repair 69% of the seeded errors in system models taken from a diverse suite of case studies.

ABSTRACT. Modern operating systems allow user-space applications to submit code for kernel execution through the use of in-kernel domain specific languages (DSLs). Applications use these DSLs to customize system policies and add new functionality. For performance, the kernel executes them via just-in-time (JIT) compilation. The correctness of these JITs is crucial for the security of the kernel: bugs in in-kernel JITs have led to numerous critical issues and patches. This paper presents JitSynth, the first tool for synthesizing verified JITs for in-kernel DSLs. JitSynth takes as input interpreters for the source DSL and the target instruction set architecture. Given these interpreters, and a mapping from source to target states, JitSynth synthesizes a verified JIT compiler from the source to the target. Our key idea is to formulate this synthesis problem as one of synthesizing a per-instruction compiler for abstract register machines. Our core technical contribution is a new compiler metasketch that enables JitSynth to efficiently explore the resulting synthesis search space. To evaluate JitSynth, we use it to synthesize a JIT from eBPF to RISC-V and compare to a recently developed Linux JIT. The synthesized JIT avoids all known bugs in the Linux JIT, with an average slowdown of 1.82× in the performance of the generated code. We also use JitSynth to synthesize competitive JITs for two additional source-target pairs. The results show that JitSynth offers a promising new way to develop verified JITs for in-kernel DSLs.

ABSTRACT. In this paper, we present a new program synthesis algorithm based on reinforcement learning. Given an initial policy (i.e. statistical model) trained off-line, our method uses this policy to guide its search and gradually improves it by leveraging feedback obtained from a deductive reasoning engine. Specifically, we formulate program synthesis as a reinforcement learning problem and propose a new variant of the policy gradient algorithm that can incorporate feedback from a deduction engine into the underlying statistical model. The benefit of this approach is two-fold: First, it combines the power of deductive and statistical reasoning in a unified framework. Second, it leverages deduction not only to prune the search space but also to guide search. We have implemented the proposed approach in a tool called Concord and experimentally evaluate it on synthesis tasks studied in prior work. Our comparison against several baselines and two existing synthesis tools shows the advantages of our proposed approach. In particular, Concord solves 15% more benchmarks compared to Neo, a state-of-the-art synthesis tool, while improving synthesis time by 8.71x on benchmarks that can be solved by both tools.

ABSTRACT. We identify a decidable synthesis problem for a class of pro- grams of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted func- tions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a pow- erful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs and show the problem to be decidable, identify- ing its precise complexity, and also study several variants of the problem.

ABSTRACT. We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.

ABSTRACT. We describe a technique for systematic testing of multi-threaded programs. We combine Quasi-Optimal Partial-Order Reduction (POR), a state-of-the-art POR that handles interleaving non-determinism, with symbolic execution to handle data non-determinism. Our technique iteratively and exhaustively finds all executions of the program. It represents program executions using a partial orders and finds the next execution using an underlying unfolding semantics. We avoid the exploration of redundant program traces using cutoff events.

We implemented our technique as an extension of KLEE and evaluated it on a set of large multi-threaded C programs. Our experiments found several previously undiscovered bugs and undefined behaviors in memcached and GNU sort, showing that the new method is capable of finding bugs in industrial-size benchmarks.

ABSTRACT. Linearizability is the de facto correctness criterion for concurrent abstract data type implementations. Violation of linearizability is witnessed by an error trace in which the outputs of individual operations do not match sequential executions of the same operations. Extensive work has been done in proving linearizability of concurrent {\sc adt}'s or discovering linearizability bugs in them. Little work has been done in trying to provide useful hints to the programmer when a violation of linearizability is discovered by a tester tool. In this paper, we propose an approach that identifies the root causes of linearizability errors in the form of code blocks whose atomicity is required to restore linearizability. The key insight of this paper is that the problem can be reduced to a simpler algorithmic problem of identifying minimal root causes of conflict serializability violation in an error trace combined with a heuristic for identifying which of these are more likely to be the true root cause of non-linearizability. We propose theoretical results outlining this reduction, and an algorithm to solve the simpler problem. We have implemented our approach and carried out several experiments on realistic concurrent ADTs showing its efficiency.

ABSTRACT. This work is concerned with fault localization for automated program repair.

We define a novel concept of a must location set. Intuitively, such a set includes at least one program location from every repair for a bug. Thus, it is impossible to fix the bug without changing at least one location from this set. A fault localization technique is considered a must algorithm if it returns a must location set for every buggy program and every bug in the program. We show that some traditional fault localization techniques are not must.

We observe that the notion of must fault localization depends on the chosen repair scheme, which identifies the changes that can be applied to program statements as part of a repair. We develop a new algorithm for fault localization and prove that it is must with respect to schemes commonly used in automated program repair.

We incorporate the new fault localization technique into an existing mutation-based program repair algorithm. We exploit it in order to prune the search space when a buggy mutated program has been generated.

Our experimental results show that must fault localization is able to significantly speed-up the repair process, without losing any of the potential repairs.

ABSTRACT. Witness validation is an important technique to increase trust in verification results, by making descriptions of error paths (violation witnesses) and important parts of the correctness proof (correctness wit- nesses) available in an exchangable format. This way, the verification result can be validated independently from the verification. The problem is that there are unfortunately not many tools for witness-based validation of verification results available. We contribute to closing this gap with the approach of validation via verification, which is a way to automatically construct a set of validators from a set of existing verification engines. The idea is to take as input a specification, a program, and a verification witness, and produce a new specification and an instrumented version of the original program such that the instrumented program satisfies the new specification if the witness is useful to confirm the result of the verification. Then, an existing verifier can be used to validate the previously computed result (as witnessed by the verification witness) via an ordinary verifica- tion task. We have implemented our approach in the validator MetaVal , and it was successfully used in SV-COMP 2020 and confirmed 3 653 vio- lation witnesses and 16 376 correctness witnesses. The SV-COMP results show that MetaVal improves the effectiveness (167 uniquely confirmed violation witnesses and 833 uniquely confirmed correctness witnesses) of the overall validation process, on a large benchmark set. All components and experimental data are publicly available.

ABSTRACT. Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. In a CMDP, the controller possesses a certain amount of a critical resource, such as electric power. Each action of the controller can consume some amount of the resource. Resource replenishment is only possible in special reload states, in which the resource level can be reloaded up to the full capacity of the system. The task of the controller is to prevent resource exhaustion, i.e. ensure that the available amount of the resource stays non-negative, while ensuring an additional linear-time property. We study the complexity of strategy synthesis in consumption MDPs with almost-sure Büchi objectives. We show that the problem can solved in polynomial time. We implement our algorithm, and show that it can efficiently solve CMDPs modelling real-world scenarios.

ABSTRACT. We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives.  Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in $\np \cap \conp$, matching the current known bound for single objectives; and  in general the decision problem is $\pspace$-hard and can be solved in $\nexptime \cap \conexptime$. We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.

ABSTRACT. Markov decision processes are widely used for planning and verification in settings that combine controllable or adversarial choices with probabilistic behaviour. The standard analysis algorithm, value iteration, only provides lower bounds on infinite-horizon probabilities and rewards. Two "sound" variations, which also deliver an upper bound, have recently appeared. In this paper, we present a new sound approach that leverages value iteration's ability to usually deliver good lower bounds: we obtain a lower bound via standard value iteration, use the result to "guess" an upper bound, and prove the latter's correctness. We present this 'optimistic value iteration' approach for computing reachability probabilities as well as expected rewards. It is easy to implement and performs well, as we show via an extensive experimental evaluation.

ABSTRACT. IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Alongside the theoretical underpinnings, we present a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation. Experiments show that our prototype is competitive with the state-of-the-art on some selected benchmarks.

ABSTRACT. We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. Firstly, concurrent stochastic games bring more realistic modelling of agents interacting in a concurrent fashion. Secondly, equilibria-based properties provide a means to analyse games in which competing or collaborating players are driven by distinct objectives. Thirdly, a real-time extension of (turn-based) stochastic games facilitates verification and strategy synthesis for systems where timing is a crucial aspect. This paper describes the advances made in the tool's modelling language, property specification language and model checking engines in order to implement this new functionality. We also summarise the performance and scalability of the tool, and describe a selection of case studies, ranging from security protocols to robot coordination, which highlight the benefits of the new features.

Artifact: http://prismmodelchecker.org/downloads/cav20pg3.ova Artifact SHA1 checksum: 475aa32bb73e53fc2b9411a0c3cfb568390def7d Artifact VM info: http://prismmodelchecker.org/downloads/cav20pg3-vm.txt