ABSTRACT. I will first give a brief overview of the research projects that are taking place in the RiSE group at MSR in Redmond. The focus will be on those projects that are related to the core topic of the workshop: applications of logical inference. I will talk more in detail about some of the projects that I am more familiar with.

ABSTRACT. In this tool paper we present Harrsh - a tool for unified reasoning about symbolic-heap separation logic. Harrsh supports the analysis of robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Harrsh makes use of heap automata, which offer a generic approach to reasoning about robustness properties. We report on experimental results for several robustness properties from the literature and compare against satisfiability checkers participating in a recent competition. We conclude that a generic approach to checking robustness is feasible and promising for the extension to further properties of interest.

ABSTRACT. As an ingredient for a verified DPLL(T) solver, it is crucial to have a theory solver that has an incremental interface and provides unsatisfiable cores. To this end, we extend the Isabelle/HOL formalization of the simplex algorithm by Spasic and Maric. We further discuss the impact of their design decisions on the development of our extension.

ABSTRACT. Watchlist (also hint list) is a technique that allows lemmas from related proofs to guide a saturation-style proof search for a new conjecture. ProofWatch is a recent watchlist-style method that loads many previous proofs inside the ATP, maintains their completion ratios during the proof search and focuses the search by following the most completed proofs. In this work, we start to use the dynamically changing vector of proof completion ratios as additional information about the saturation-style proof state for statistical machine learning methods that evaluate the generated clauses. In particular, we add the proof completion vectors to ENIGMA (efficient learning-based inference guiding machine) and evaluate the new method on the MPTP Challenge benchmark, showing moderate improvement in E's performance.

ABSTRACT. The problem of Cloud resource provisioning for component-based applications is very important. It consists in the allocation of virtual machines (VMs) from various Cloud Providers (CPs), to a set of applications such that the constraints induced by the interactions between components and by the components hardware/software requirements are satisfied and the performance objectives are optimized (e.g. costs are minimized). It can be formulated as a constrained optimization problem and tackled by state-of-the-art optimization modulo theories (OMT) tools. The performance of the OMT tools is highly dependent on the way the problem is formalized as this determines the size of the search space. In the case when the number of VMs offers is large, a naive encoding which does not exploit the symmetries of the underlying problem leads to a huge search space making the optimization problem intractable. We overcame this issue by reducing the search space by using: (1) a heuristic which exploits the particularities of the application by detecting cliques in the conflict graph of the application components fixing all components of the clique with the largest number of component instances, and (2) a lex-leader method for breaking variable symmetry where the canonical solution fulfills an order based on either the number of components deployed on VMs, or on the VMs price.

As the result, the running time of the optimization problem improves considerably and the optimization problem scales up to hundreds of VM offers. We also observed that by combining the heuristic with the lex-leader method we obtained better computational results than by using them separately, suggesting the fact that symmetry breaking constraints have the advantage of interacting well with the search heuristic being used.

ABSTRACT. Answer Set Programming (ASP) is a successful method for solving a range of real-world applications. Despite the availability of fast ASP solvers, the task of computing answer sets demands a very large computational power, since the problem tackled is high in the polynomial hierarchy. A speed-up in answer set computation may be gained, if the program can be split into two disjoint parts, bottom and top. Thus, the bottom part is evaluated independently of the top part, and the results of the bottom part evaluation are used to simplify the top part. Lifschitz and Turned have introduced the concept of a splitting set, i.e., a set of atoms that define the splitting.

In this paper, we address two issues regarding splitting. First, we show that the problem of computing a splitting set with some desirable properties can be reduced to a classic Search Problem and solved in polynomial time. Second, we show that the definition of splitting sets can be adjusted to allow splitting of a broader class of programs.