ABSTRACT. In this paper, we study the parameter synthesis problem for probabilistic hyperproperties. A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. We, in particular, solve the following problem: given a probabilistic hyperproperty and discrete-time Markov chain with parametric transition probabilities, compute regions of parameter configurations that instantiate the Markov chain to satisfy the hyperproperty, and regions that lead to violation. We solve this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance.

ABSTRACT. Logic-based approaches to AI have the advantage that their behaviour can in principle be explained by providing their users with proofs for the derived consequences. However, if such proofs get very large, then it may be hard to understand a consequence even if the individual derivation steps are easy to comprehend. This motivates our interest in finding small proofs for Description Logic (DL) entailments. Instead of concentrating on a specific DL and proof calculus for this DL, we introduce a general framework in which proofs are represented as labeled, directed hypergraphs whose hyperedges correspond to single sound derivation steps.

On the theoretical side, we investigate the complexity of deciding whether a certain consequence has a proof of size at most n along the following orthogonal dimensions: (i) the underlying proof system is polynomial or exponential; (ii) proofs may or may not reuse already derived consequences; and (iii) the number $n$ is represented in unary or binary. We have determined the exact worst-case complexity of this decision problem for all but one of the possible combinations of these options.

On the practical side, we have developed and implemented an approach for generating proofs for expressive DLs based on the non-standard inference forgetting. We have evaluated this approach on a set of realistic ontologies and compared the proofs with proofs generated by the DL reasoner ELK, finding that forgetting-based proofs are often better w.r.t. different measures of proof complexity.

ABSTRACT. We introduce a Curry-Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested rules for classical disjunctive tautologies (1-depth intermediate proofs). The resulting calculus, we call it $\lama$, is a strongly normalizing parallel extension of the simply typed lambda-calculus. Although simple, the $\lama$ reduction rules can model arbitrary process network topologies, and encode interesting parallel programs ranging from numeric computation to algorithms on graphs.

ABSTRACT. In this paper we propose a number of powerful logics for information sharing and acts of publicly or privately accessing other agents' information databases. The static base of our logics builds on the already existing work in epistemic logic, in particular on the concepts of distributed knowledge and common knowledge. We assume that information is distributed in a number of information sources or `sites' (e.g. files, folders, data sets, websites, databases etc) at a given time. Each source can itself be thought of as being associated with an agent, either because it is actually the knowledge base of a real agent (natural or artificial), or simply because we think of the source itself as an abstract or virtual `agent' (possessing exactly the information that is locally stored at that site). Distributed knowledge of a group is the sum total of all (that follows from) the information possessed by any of the agents in the group, while common knowledge is only the information possessed in common by these agents. Distributed knowledge can be `actualized' or `resolved', i.e. converted into common knowledge, by full communication within the group. We axiomatize a new concept of ``common distributed knowledge" within a family of (sub)groups of agents, that lies somewhere in between the two, and can be actualized into full common knowledge by much less communication (namely, only within each subgroup). We also consider an extension of this logic with comparative epistemic assertions for individuals (``agent $b$ knows everything known to agent $c$") or groups (``group $B$ has distributed knowledge of everything known to group $C$").

On this static base, we built communication logics obtained by adding various dynamic operators for information sharing, public or private accessing etc. An agent may gain access to a number of sources, after which it can be assumed to instantly `read' all the information stored at that site, i.e. it `learns' everything that was known by the source agent. The `reading' agent gains access to a source either because it is granted such access by the source agent itself (by ``sharing" her database, in which case it is natural to assume that the source `knows' it is being accessed), or because it somehow succeeded to illegally gain such access via e.g. hacking, in which case typically the source doesn't know it's being accessed (although sometimes it does get to know it, either because the hacker publicizes all the stolen information, or because somehow the source agents is able to detect the hacking). So a reading action can be public (when it is common knowledge that it occurs) or secret, or semi-public (visible only to some agents). Multiple agents may simultaneously access multiple sources. After each such reading action, each reading agent knows everything that was known by its source agents.

We completely axiomatize several of these logics, prove their decidability, and end with a few open questions.

ABSTRACT. Given an unsatisfiable Boolean Formula F in CNF, i.e. a set of clauses, one is often interested in identifying Maximal Satisfiable Subsets (MSSes) of F or, equivalently, in the complements of MSSes called Minimal Correction Subsets (MCSes). Since MSSes (MCSes) find applications in many domains, e.g. diagnosis, ontologies debugging, or axiom pinpointing, there have been proposed several MSS enumeration algorithms. Unfortunately, finding even a single MSS is often very hard since it naturally subsumes repeatedly solving the satisfiability problem. Moreover, there can be up to exponentially many MSSes, thus their complete enumeration is often practically intractable. Therefore, the algorithms tend to identify as many MSSes as possible within a given time limit. In this work, we present a novel MSS enumeration algorithm called RIME. Compared to existing algorithms, RIME is much more frugal in the number of performed satisfiability checks which we witness via an experimental comparison. Moreover, we witness that RIME is several times faster than existing algorithms.

ABSTRACT. We present a system that utilizes machine learning for proof search in the Coq theorem prover. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs in the form of tactic scripts. This is done by learning from previous tactic scripts, and how they are applied to proof states. An evaluation of our system was performed on the Coq Standard Library. In its current state, our predictor can identify the correct tactic to be applied on a goal 23.5% of the time. Our proof searcher can fully automatically prove 39.3% of the lemmas in the library.

ABSTRACT. This paper presents a novel algorithm for automatically learning recursive shape predicates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.

ABSTRACT. We generalize the definition of an Induction Model given by L. Henkin (1960). The main goal of the paper is to study reduction and equivalence between these Induction Models. We give a formal definition for these concepts and then prove a criterion which can be used to check when one Induction Model can be reduced to or is equivalent to another Induction Model.

We also look at the base cases and generating functions which can give us an Induction Model. There are three cases which we look at depending on the structure of the generating functions (arbitrary, additive, multiplicative).

ABSTRACT. The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.

ABSTRACT. Based our formal framework for CDCL (conflict-driven clause learning) using the proof assistant Isabelle\slash HOL, we verify an extension of CDCL computing cost-minimal models called OCDCL. It is based on branch and bound and computes models of minimal cost with respect to total valuations. The verification starts by developing a framework for CDCL with branch and bound, called \CDCLBaB{}, which is then instantiated to get OCDCL. We then apply our formalization to three different applications. Firstly, through the dual rail encoding, we reduce the search for cost-optimal models with respect to partial valuations to searching for total cost-optimal models, as derived by OCDCL. Secondly, we instantiate OCDCL to solve MAX-SAT, and, thirdly, \CDCLBaB{} to compute a set of covering models. A large part of the original CDCL verification framework could be reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of CDCL with branch and bound, and its application to an optimizing CDCL calculus and the first solution that computes cost-optimal models with respect to partial valuations.

ABSTRACT. The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modules and the HOL4 library is achieved by the choice of tree neural networks (TNNs) as machine learning models and the internal use of HOL4 terms to represent tree structures of TNNs. Recursive improvement is possible when a task is expressed as a search problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm guided by a TNN can be used to explore the search space and produce better examples for training the next TNN. As an illustration, term synthesis tasks on combinators and Diophantine equations are specified and learned. The success rate on test sets generated for each task is respectively 65% and 78.5%. These results are compared with state-of-the-art ATPs on combinators and set a precedent for statistically guided synthesis of Diophantine equations.

ABSTRACT. NACRE, for Nogood And Clause Reasoning Engine, is a constraint solver written in C++. It is based on a modular architecture designed to work with generic constraints while implementing several state-of-the-art search methods and heuristics. Interestingly, its data structures have been carefully designed to play around nogoods and clauses, making it suitable for implementing learning strategies. NACRE was submitted to the CSP MiniTrack of the 2018 and 2019 XCSP3 competitions where it took the first place. This paper gives a general description of NACRE as a framework. We present its kernel, the available search algorithms, and the default settings (notably, used for XCSP3 competitions), which makes NACRE efficient in practice when used as a black-box solver.

ABSTRACT. Deep neural networks (DNNs) are revolutionizing the way complex systems are designed, developed and maintained. As part of the life cycle of DNN-based systems, there is often a need to modify a DNN in subtle ways that affect certain aspects of its behavior, while leaving other aspects of its behavior unchanged (e.g., if a bug is discovered and needs to be fixed, without altering other functionality). Unfortunately, retraining a DNN is often difficult and expensive, and may produce a new DNN that is quite different from the original. We leverage recent advances in DNN verification and propose a technique for modifying a DNN according to certain requirements, in a way that is provably minimal, does not require any retraining, and is thus less likely to affect other aspects of the DNN’s behavior. Using a proof-of-concept implementation, we demonstrate the usefulness and potential of our approach in addressing two real-world needs: (i) measuring the resilience of DNN watermarking schemes; and (ii) bug repair in already-trained DNNs.

ABSTRACT. In the last years, several works were concerned with identifying classes of programs where termination is decidable. We consider triangular weakly non-linear loops (twn-loops) over a ring Z ≤ S ≤ R_A , where R_A is the set of all real algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that termination of such loops is decidable for S = R_A and non-termination is semi-decidable for S = Z and S = Q.

In this paper, we show that the halting problem is decidable for twn-loops over any ring Z ≤ S ≤ R_A. In contrast to the termination problem, where termination on all inputs is considered, the halting problem is concerned with termination on a given input. This allows us to compute witnesses for non-termination.

Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f( || (x_1, ..., x_d) || ), where || · || denotes the 1-norm. As a corollary, we obtain that the runtime of a terminating triangular linear loop over Z is at most linear.

ABSTRACT. We study light-weight techniques for preprocessing of WSkS formulae in an automata-based decision procedure as implemented, e.g., in MONA. The techniques we use are based on antiprenexing, i.e., pushing quantifiers deeper into a formula. Intuitively, this tries to alleviate the explosion in the size of the constructed automata by making it happen sooner on smaller automata (and have the automata minimization reduce the output). The formula transformations that we use to implement antiprenexing may, however, be applied in different ways and extent and, if used in an unsuitable way, may also cause an explosion in the size of the formula and the automata built while deciding it. Therefore, our approach uses informed rules that use an estimation of the cost of constructing automata for WSkS formulae. The estimation is based on a model learnt from runs of the decision algorithm on various formulae. An experimental evaluation of our technique shows that antiprenexing can significantly boost the performance of the base WSkS decision procedure, sometimes allowing one to decide formulae that could not be decided before.

ABSTRACT. In biology, Boolean networks are conventionally used to represent and simulate gene regulatory networks. The attractors are the subject of special attention in analyzing the dynamics of a Boolean network. They correspond to stable states and stable cycles, which play a crucial role in biological systems. In this work, we study a new representation of the dynamics of Boolean networks that are based on a new semantics used in answer set programming (ASP). Our work is based on the enumeration of all the attractors of asynchronous Boolean networks having interaction graphs which are circuits. We show that the used semantics allows to design a new approach for computing exhaustively both the stable cycles and the stable states of such networks. The enumeration of all the attractors and the distinction between both types of attractors is a significant step to better understand some critical aspects of biology. We applied and evaluated the proposed approach on randomly generated Boolean networks and the obtained results highlight the benefits of this approach, and match with some conjectured results in biology.

ABSTRACT. The triguarded fragment of first-order logic is an extension of the guarded fragment in which quantification for subformulas with at most two variables need not be guarded. Thus, it unifies two prominent decidable logics: the guarded fragment and the two-variable fragment. Its satisfiability problem is known to be undecidable in the presence of equality, but becomes decidable when equality is forbidden. We consider an extension of the triguarded fragment without equality by transitive relations, allowing them to be used only as guards. We show that the satisfiability problem for the obtained formalism is decidable and 2ExpTime-complete, that is, it is of the same complexity as for the analogous extension of the classical guarded fragment. In fact, in our satisfiability test we use a decision procedure for the latter as a subroutine. We also show how our approach, consisting in exploiting some existing results on guarded logics, can be used to reprove some known facts, as well as to derive some new results on triguarded logics.

ABSTRACT. Fault Tree Analysis (FTA) is a prominent technique in industrial and scientific risk assessment. Repairable Fault Trees (RFT) enhance the classical Fault Tree (FT) model by introducing the possibility to describe complex dependent repairs of system components. Usual frameworks for analyzing FTs such as BDD, SBDD, and Markov chains fail to assess the desired properties over RFT complex models, either because these become too large, or due to cyclic behaviour introduced by dependent repairs. Simulation is another way to carry out this kind of analysis. In this paper we review the RFT model with Repair Boxes as introduced by Daniele Codetta-Raiteri. We present compositional semantics for this model in terms of Input/Output Stochastic Automata, which allows for the modelling of events occurring according to general continuous distribution. Moreover, we prove that the semantics generates (weakly) deterministic models, hence suitable for discrete event simulation, and prominently for rare event simulation using the FIG tool.

ABSTRACT. Satisfiability (SAT) solving has become an important technology in computer-aided mathematics with various successes in number and graph theory. In this paper we apply SAT solvers to color infinitely long strips in the plane with a given height and number of colors. The coloring is constrained as follows: two points that are exactly unit distance apart must be colored differently. To finitize the problem, we tile the strips and all points on a tile have the same color. We evaluated our approach using two different tile shapes: squares and hexagons. We were able to increase the lower bound for the strip height with 5 colors. The visualization of strips using 3 to 6 colors reveal patterns that are similar to the best known lower bounds.

ABSTRACT. Symbolic-heap separation logic with inductive definitions is a popular formalism for reasoning about heap-manipulating programs. The btw-fragment, introduced by Iosif, Rogalewicz and Simacek, is one of the most expressive fragments with a decidable entailment problem. In recent work, we improved on the original decidability proof by providing a direct model-theoretic construction, obtaining a 2-Exptime upper bound.

In this paper, we investigate separation logics built on top of the inductive definitions from the btw-fragment, i.e., separation logics that feature the standard Boolean and separation-logic operators. We give an almost tight delineation between decidability and undecidabilty. We establish the decidability of the satisfiability problem (in 2-Exptime) of a separation-logic with conjunction, disjunction, separating conjunction and guarded forms of negation, magic wand, and septraction. We show that any further generalization leads to undecidabilty (under mild assumptions).

ABSTRACT. In this work we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of facts independently of each other by their rank, the new method uses the notion of _state_ that is updated each time a choice of a fact is made. Our stateful architecture is based on recurrent neural networks which have been recently very successful in stateful tasks such as language translation. The new method is combined with data augmentation techniques, evaluated in several ways on a standard large-theory benchmark and compared to state-of-the-art premise approach based on gradient boosted trees. It is shown to perform significantly better and to solve many new problems.

ABSTRACT. Inprocessing techniques have become one of the most promising advancements in SAT solving over the last decade. Some inprocessing techniques modify a propositional formula in non model-perserving ways. These operations are very problematic when Craig interpolants must be extracted: existing methods take resolution proofs as an input, but these inferences require stronger proof systems; state-of-the-art solvers generate DRAT proofs. We present the first method to transform DRAT proofs into resolution-like proofs by eliminating satisfiability-preserving RAT inferences. This solves the problem of extracting interpolants from DRAT proofs.

ABSTRACT. Controlling access to knowledge plays a crucial role in many multi-agent systems. Indeed, it is related to different central aspects in interactions among agents such as privacy, security, and cooperation. In this paper, we propose a framework for dealing with access to knowledge that is based on the inference process in classical propositional logic: an agent has access to every piece of knowledge that can be derived from the available knowledge using the classical inference process. We first introduce a basic problem in which an agent has to hide pieces of knowledge, and we show that this problem can be solved through the computation of maximal consistent subsets. In the same way, we also propose a counterpart of the previous problem in which an agent has to share pieces of knowledge, and we show that this problem can be solved through the computation of minimal inconsistent subsets. Then, we propose a generalization of the previous problem where an agent has to share pieces of knowledge and hide at the same time others. In this context, we introduce several concepts that allow capturing interesting aspects. Finally, we propose a weight-based approach by associating weights with the pieces of knowledge that have to be shared or hidden.

ABSTRACT. Motivated by Gromov’s subgroup conjecture (GSC), a fundamental open conjecture in the area of geometric group theory, we tackle the problem of the existence of particular types of subgroups---arising from so-called periodic apartments---for a specific set of hyperbolic groups with respect to which GSC is currently open. This problems is equivalent to determining whether specific types of graphs with a non-trivial combination of properties exist. The existence of periodic apartments allows for ruling the groups out as some of the remaining potential counterexamples to GSC. Our approach combines both automated reasoning techniques---in particular, Boolean satisfiability (SAT) solving---with problem-specific orderly generation. Compared to earlier attempts to tackle the problem through computational means, our approach scales several magnitudes better, and allows for both confirming results from a previous computational treatment for smaller parameter values as well as ruling out further groups out as potential counterexamples to GSC.

ABSTRACT. Globalization of integrated circuits manufacturing has led to increased security concerns, notably IP theft. In response, many logic locking techniques have been developed for protecting designs, but many of these locking techniques have been shown to be vulnerable to SAT attacks. In this paper, we explore the use of Boolean sensitivity to analyze circuits locked with these techniques. We show that in typical circuits there is an inverse relationship between input width and sensitivity. We then demonstrate the utility of this relationship for deobfuscating circuits locked with a class of ``provably secure'' logic locking techniques. We conclude with an example of how to resist this attack, although the resistance is shown to be highly circuit dependent.

ABSTRACT. Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.