LPAR-IWIL 2018: Papers with Abstracts

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 inter- actions 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 detect- ing 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. 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 over ProofWatch and ENIGMA.

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 taken 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 Spasi ́c and Mari ́c. We further discuss the impact of their design decisions on the development of our extension.

Abstract. Metaquery (MQ) is a datamining tool for inferring relations between data items over a relational database. The concept of MQ leads to autonomous discovery of logical rules involving the database tables. A central module of any MQ system is the MQ generator, which automatically generates all possible MQs to be tested against a database. The MQ generator is supposed to work in an efficient manner, while not missing any meaningful MQ. In this paper we present an algorithm for MQ generation that works as a search algorithm in which the states are all possible MQs, and the search tree is pruned whenever possible. Preliminary experiments prove that, indeed, the approach we take leads to a significant reduction in computation resources.

Abstract. In this work, we investigate the inclusion of symmetry breaking in the answer set programming (ASP) framework. The notion of symmetry is widely studied in various domains. Particularly, in the field of constraint programming, where symmetry breaking made a significant improvement in the performances of many constraint solvers. Usually, combinatorial problems contain a lot of symmetries that could render their resolution difficult for the solvers that do not consider them. Indeed, these symmetries guide the solvers in the useless exploration of symmetric and redundant branches of the search tree. The ASP framework is well-known in knowledge representation and reasoning. How- ever, only few works on symmetry in ASP exist. We propose in this paper a new ASP solver based on a novel semantics that we enhance by symmetry breaking. This method with symmetry elimination is implemented and used for the resolution of a large variety of combinatorial problems. The obtained results are very promising and showcase an advantage when using our method in comparison to other known ASP methods.

Abstract. This paper investigates a preliminary application of homotopy type theory in cryptography. It discusses specifying a cryptographic protocol using homotopy type theory which adds the notion of higher inductive type and univalence to Martin-Lo ̈f’s intensional type theory. A higher inductive type specification can act as a front-end mapped to a concrete cryptographic implementation in the universe. By having a higher inductive type front-end, we can encode domain-specific laws of the cryptographic implementation as higher-dimensional paths. The higher inductive type gives us a graphical computational model and can be used to extract functions from underlying concrete implementation. Us- ing this model we can extend types to act as formal certificates guaranteeing on correctness properties of a cryptographic implementation.

Abstract. Halpern-Shoham logic (HS) is a very expressive and elegant formalism for interval temporal reasoning in which the satisfiability problem is undecidable. One of the methods to obtain HS-fragments of lower computational complexity is to adopt the softened (reflexive) seman- tics of the accessibility relations. In the paper we consider disallowing punctual intervals in reflexive semantics. We show that in this case we gain additional expressive power, which over discrete orders of time points results in PSpace-hardness of the Horn fragment of HS without diamond modal operators is and in undecidability of the core fragment of HS.