ABSTRACT. We will present a set of parallel algorithms for parameter synthesis in parametrised dynamical systems from temporal logic specifications. The problem is for a dynamical system represented in terms of a finite-state transition system with parametrised transition relation to synthesise parameter values satisfying the given specification. Technically, the method is based on model checking algorithms adapted to such kind of transition systems. Additionally, we will address a specific subproblem of parameter synthesis targeting identification of attractors in systems dynamics. To that end, a novel parallel algorithm for detection of strongly connected components in a parameterised system will be presented. We will show that the underlying algorithms can gain advantages from efficient symbolic representations of sets of parameter valuations. To demonstrate the method, we will describe applications to models representing dynamics of biological systems with complex non-linear behaviour.

ABSTRACT. There has been an increasing interest in recent years towards the development of efficient solvers for Answer Set Programming (ASP) and towards the application of ASP to solve increasing more challenging problems. In particular, several recent efforts have explored the issue of scalability of ASP solvers when addressing the challenges caused by the need to ground the program before resolution. This paper offers an alternative solution to this challenge, focused on the use of distributed programming techniques to reason about ASP programs whose grounding would be prohibitive for mainstream ASP solvers. The work builds on the work proposed by Konczak et al. in 2004, which proposed a characterization of answer set solving as a form of non-standard graph coloring. The paper expands this characterization to include syntactic extensions used in modern ASP (e.g., choice rules, weight constraints). We present an implementation of the solver using a distributed programming framework specifically designed to manipulate very large graphs, as provided by Apache Spark, which in turn builds on the MapReduce programming framework. Finally, we provide a few preliminary results obtained from the first prototype implementation of this approach.

ABSTRACT. Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools.

Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination.

Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.

ABSTRACT. Paramount to the viability of a parallel architecture is the correct implementation of its memory consistency model (MCM). Although tools exist for verifying consistency models at several design levels, a problematic verification gap exists between checking an abstract microarchitectural specification of a consistency model and verifying that the actual processor RTL implements it correctly. This paper presents RTLCheck, a methodology and tool for narrowing the microarchitecture/RTL MCM verification gap. Given a set of microarchitectural axioms about MCM behavior, an RTL design, and user-provided mappings to assist in connecting the two, RTLCheck automatically generates the SystemVerilog Assertions (SVA) needed to verify that the implementation satisfies the microarchitectural specification for a given litmus test program. When combined with existing automated MCM verification tools, RTLCheck enables test-based full-stack MCM verification from high-level languages to RTL. We evaluate RTLCheck on a multicore version of the RISC-V V-scale processor, and discover a bug in its memory implementation. Once the bug is fixed, we verify that the multicore V-scale implementation satisfies sequential consistency across 56 litmus tests. The JasperGold property verifier finds com- plete proofs for 89% of our properties, and can find bounded proofs for the remaining properties.

ABSTRACT. ABSTRACT. In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TOPO. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1,000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart-, branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.

As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

ABSTRACT. Details will follow shortly.

ABSTRACT. For multi-core computers, an important paradigm for parallel execution is task-based or fork-join parallelism. Typically this is implemented using work-stealing. This paradigm is a good fit for algorithms that contain recursion, but is also suitable in other contexts, for example the load-balancing of parallel computations on arrays. We apply work-stealing in several verification contexts. We parallelize operations on binary decision diagrams and on verification tools that use binary decision diagrams, where we apply work-stealing both on the low level of the individual operations and on the higher level of the search algorithms. We parallelize parity game solvers in the following two ways. We use work-stealing to parallelize backward search for attractor computation. We also use work-stealing to parallelize all steps of the strategy improvement algorithm. In these applications, using work-stealing is necessary but not sufficient to obtain a good performance. We must also avoid locking techniques and instead use lock-free techniques for scalable performance. We use lock-free techniques not only for the parallelized algorithms but also to implement the scalable work-stealing framework Lace with high multi-core scaling.

ABSTRACT. Parity games are abstract infinite-duration two-player games, widely studied in computer science. Several solution algorithms have been proposed and also implemented in the community tool of choice called PGSolver, which has declared the Zielonka Recursive (ZR) algorithm the best performing on randomly generated games. With the aim of scaling and solving wider classes of parity games, several improvements and optimizations have been proposed over the existing algorithms. However, no one has yet explored the benefit of using the full computational power of which even common modern multicore processors are capable of. This is even more surprisingly by considering that most of the advanced algorithms in PGSolver are sequential. In this work we introduce and implement, on a multicore architecture, a parallel version of the Attractor algorithm, that is the main kernel of the ZR algorithm. This choice follows our investigation that more of the 99% of the execution time of the ZR algorithm is spent in this module.