Feb 19 2018 cs.LO
This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially quantified. This condition is different from that proposed by Brotherston et al. in 2017 and one of them does not imply the other. The main idea is a novel translation from an entailment of symbolic heaps into a formula in Presburger arithmetic. The second result is the decidability for a system with both arrays and lists. The key idea is to extend the unroll collapse technique proposed by Berdine et al. in 2005 to arrays and arithmetic as well as double-linked lists.
This volume contains the formal proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), held on 8th September 2017 in Oxford, United Kingdom, and affiliated with the Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017).
Feb 16 2018 cs.LO
This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
Feb 16 2018 cs.LO
We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard methods are either geared toward proving the absence of solution or targeted to specific theories, we propose a generic approach based on a reduction to the quantifier-free case. Our technique allows thus to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods.
We study the fine-grained complexity of Leader Contributor Reachability (LCR) and Bounded-Stage Reachability (BSR), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. We contribute new verification algorithms and lower bounds based on the Exponential Time Hypothesis (ETH) and kernels. LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain D and the size of the leader L, and (2) by the size of the contributors C. We present two algorithms, running in O*((L(D+1))^(LD)*D^D) and O*(4^C) time, showing that both parameterizations are fixed-parameter tractable. Further, we suggest a modification of the first algorithm, suitable for practical instances. The upper bounds are complemented by (matching) lower bounds based on ETH and kernels. For BSR, we consider programs involving t different threads. We restrict to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s-stage computation. When parameterized by P, the maximum size of a thread, and t, the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces D or s to a polynomial dependence on P and t. This indicates that symbolic methods may be harder to find for this problem.
Feb 16 2018 cs.LO
In the first part of this paper, we define two resource aware typing systems for the $\lambda\mu$-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments --based on decreasing measures of type derivations-- to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head-reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the $\lambda\mu$-calculus is refined to a resource aware interpretation called $\lambda\mu$r, which is inspired by the substitution at a distance paradigm. The small-step $\lambda\mu$r-calculus turns out to be compatible with a natural extension of the non-idempotent interpretations of $\lambda\mu$, i.e. $\lambda\mu$r-reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly $\lambda\mu$r-normalizing terms by means of typing.
Feb 15 2018 cs.LO
We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound. For Frege we show that circular proofs can be converted into tree-like ones with at most polynomial overhead. For Resolution the translation can no longer be a Resolution proof because, as we show, the pigeonhole principle has circular Resolution proofs of polynomial size. Surprisingly, as proof systems for deriving clauses from clauses, Circular Resolution turns out to be equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: 1) polynomial-time (LP-based) algorithms that find circular Resolution proofs of constant width, 2) examples that separate circular from dag-like Resolution, such as the pigeonhole principle and its variants, and 3) exponentially hard cases for circular Resolution.
A general approach to the realizability semantics of System F is obtained by considering closure operators over sets of lambda-terms. We investigate completeness and relational parametricity in the semantics generated by such closure operators. We prove general results and show that they can be applied to several well-known semantics, as those arising from Tait's saturatedness conditions and from Girard's reducibility candidates. First, we show that, for a wide class of semantics, completeness holds for positive second order types, by generalizing some completeness results in the literature. Then we show that Reynolds parametric semantics can be formulated within the realizability semantics which are stable by union. We prove a parametricity theorem stating that closed realizers of a given type are parametric at that type. Finally, we consider syntactic dinaturality and prove that, for positive second order types, parametric terms are dinatural. Our results show that, for positive second order types, realizability, parametricity, dinaturality and typability are equivalent properties of closed normal lambda-terms.
Feb 15 2018 cs.LO
We show methods to extract Craig-Lyndon interpolants and access interpolants from clausal first-order tableaux as produced by automated first-order theorem provers based on model elimination, the connection method, the hyper tableau calculus and instance-based methods in general. Smullyan introduced an elegant method for interpolant extraction from "non-clausal" first-order tableaux. We transfer this to clausal tableaux where quantifier handling is based on prenexing and Skolemization. A lifting technique leads from ground interpolants of Herbrand expansions of Skolemized input formulas to quantified interpolants of the original input formulas. This is similar to a known interpolant lifting by Huang but based more straightforwardly on Herbrand's theorem instead of the auxiliary notion of relational interpolant. Access interpolation is a recent form of interpolation for formulas with relativized quantifiers targeted at applications in query reformulation and specified in the constructive framework of Smullyan's general tableaux. We transfer this here to clausal tableaux. Relativized quantification upon subformulas seems incompatible with lifting techniques that only introduce a global quantifier prefix. We thus follow a different approach for access interpolation: A structure preserving clausification leads to clausal ground tableaux that can be computed by automated first-order provers and, in a postprocessing step, can be restructured such that in essence the interpolant extraction from Smullyan's tableaux becomes applicable.
Variational systems allow effective building of many custom variants by using features (configuration options) to mark the variable functionality. In many of the applications, their quality assurance and formal verification are of paramount importance. Family-based model checking allows simultaneous verification of all variants of a variational system in a single run by exploiting the commonalities between the variants. Yet, its computational cost still greatly depends on the number of variants (often huge). In this work, we show how to achieve efficient family-based model checking of CTL* temporal properties using variability abstractions and off-the-shelf (single-system) tools. We use variability abstractions for deriving abstract family-based model checking, where the variability model of a variational system is replaced with an abstract (smaller) version of it, called modal featured transition system, which preserves the satisfaction of both universal and existential temporal properties, as expressible in CTL*. Modal featured transition systems contain two kinds of transitions, termed may and must transitions, which are defined by the conservative (over-approximating) abstractions and their dual (under-approximating) abstractions, respectively. The variability abstractions can be combined with different partitionings of the set of variants to infer suitable divide-and-conquer verification plans for the variational system. We illustrate the practicality of this approach for several variational systems.
Feb 15 2018 cs.LO
Linearizability is the standard correctness notion for concurrent objects, i.e., objects designed to be accessed simultaneously by multiple threads. In this paper, we explain why the original definition of linearizability is not applicable to code running on the weak memory models supported by modern multicore architectures, and provide an alternative definition which is applicable. In contrast to earlier work, our definition is proved to be both sound and complete. Furthermore, while earlier work has focussed on linearizability for the TSO (Total Store Order) architecture, ours is applicable to any existing weak memory model. We illustrate how it can be used to prove the correctness of a simple case study on the widely used TSO, Power and ARM architectures.
Feb 15 2018 cs.LO
We present a selective bibliography about efficient SAT solving, focused on optimizations for the CDCL-based algorithms.
Feb 14 2018 cs.LO
We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of $\omega$-tree languages derived from weak regular $\omega$-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived $\omega$-tree languages to learning the underlying class of $\omega$-word languages, for any class of $\omega$-word languages recognized by a deterministic Büchi acceptor. Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli  for the class of weak regular $\omega$-word languages yields the main result. We also show that subset queries that return counterexamples can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or non-deterministic finite word acceptors, and deterministic or non-deterministic Büchi $\omega$-word acceptors. A previous claim of an algorithm to learn regular $\omega$-trees due to Jayasrirani, Begam and Thomas  is unfortunately incorrect, as shown in Angluin .
Feb 14 2018 cs.LO
In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a general algorithm for transforming a class of nested systems into sequent calculus systems, passing through linear nested systems. Moreover, we show a semantical characterisation of intuitionistic, multi-modal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.
Hierarchical Petri nets allow a more abstract view and reconfigurable Petri nets model dynamic structural adaptation. In this contribution we present the combination of reconfigurable Petri nets and hierarchical Petri nets yielding hierarchical structure for reconfigurable Petri nets. Hierarchies are established by substituting transitions by subnets. These subnets are themselves reconfigurable, so they are supplied with their own set of rules. Moreover, global rules that can be applied in all of the net, are provided.
Feb 14 2018 cs.LO
A recent trend in object oriented (OO) programming languages is the use of Access Permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as Linear Concurrent Constraint Programs (lcc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in lcc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of lcc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the lcc model, observing the flow of APs and quickly finding inconsistencies of the APs vis-a-vis the implementation. The latter is an automatic theorem prover based on ILL. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).
In the setting of constructive point-free topology, we introduce a notion of continuous operation between point-free topologies and the corresponding principle of point-free continuity. An operation between points of point-free topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of point-free continuity says that any relation which induces a continuous operation between points is a morphism between the corresponding point-free topologies. The principle holds under the assumption of bi-spatiality. When restricted to a certain class of morphisms from the formal Baire space and the formal unit interval, the principle is equivalent to spatiality of these point-free spaces. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are also reviewed. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of point-free topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.
Syntax-guided synthesis aims to find a program satisfying semantic specification as well as user-provided structural hypothesis. For syntax-guided synthesis there are two main search strategies: concrete search, which systematically or stochastically enumerates all possible solutions, and symbolic search, which interacts with a constraint solver to solve the synthesis problem. In this paper, we propose a concolic synthesis framework which combines the best of the two worlds. Based on a decision tree representation, our framework works by enumerating tree heights from the smallest possible one to larger ones. For each fixed height, the framework symbolically searches a solution through the counterexample-guided inductive synthesis approach. To compensate the exponential blow-up problem with the concolic synthesis framework, we identify two fragments of synthesis problems and develop purely symbolic and more efficient procedures. The two fragments are decidable as these procedures are terminating and complete. We implemented our synthesis procedures and compared with state-of-the-art synthesizers on a range of benchmarks. Experiments show that our algorithms are promising.
Feb 14 2018 cs.LO
Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. Previous work on the semantics of weak memory models has focussed on the behaviour of assembler-level programs. In this paper we utilise that work to extract some general principles underlying instruction reordering, and apply those principles to a wide-spectrum language encompassing abstract data types as well as low-level assembler code. The goal is to support reasoning about implementations of data structures for modern processors with respect to an abstract specification. Specifically, we define an operational semantics, from which we derive some properties of program refinement, and encode the semantics in the rewriting engine Maude as a model-checking tool. The tool is used to validate the semantics against the behaviour of a set of litmus tests (small assembler programs) run on hardware, and also to model check implementations of data structures from the literature against their abstract specifications.
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.
We introduce a new class of automata on infinite trees called \emphalternating nonzero automata, which extends the class of non-deterministic nonzero automata. We reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain as a corollary algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.
Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem provers, both for interactive formalizations and for human-assisted proving of open conjectures in small theories. In this work we explore the use of watchlists in large theories coming from first-order translations of large ITP libraries, aiming at improving hammer-style automation by smarter internal guidance of the ATP systems. In particular, we (i) design watchlist-based clause evaluation heuristics inside the E ATP system, and (ii) develop new proof guiding algorithms that load many previous proofs inside the ATP and focus the proof search using a dynamically updated notion of proof matching. The methods are evaluated on a large set of problems coming from the Mizar library, showing significant improvement of E's standard portfolio of strategies, and also of the previous best set of strategies invented for Mizar by evolutionary methods.
While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, less is known about symmetries in quantified Boolean formulas (QBF). There are some works introducing adaptions of propositional symmetry breaking techniques, with a theory covering only very specific parts of QBF symmetries. We present a general framework that gives a concise characterization of symmetries of QBF. Our framework naturally incorporates the duality of universal and existential symmetries resulting in a general basis for QBF symmetry breaking.
Feb 13 2018 cs.LO
We propose two models of random quantified boolean formulas and their natural random disjunctive logic program counterparts. The models extend the standard models of random k-CNF formulas and the Chen-Interian model of random 2QBFs. The first model controls the generation of programs and QSAT formulas by imposing a specific structure on rules and clauses, respectively. The second model is based on a family of QSAT formulas in a non-clausal form. We provide theoretical bounds for the phase transition region in our models, and show experimentally the presence of the easy-hard-easy pattern and its alignment with the location of the phase transition. We show that boolean formulas and logic programs from our models are significantly harder than those obtained from the standard k-CNF and Chen-Interian models, and that their combination yields formulas and programs that are "super-hard" to evaluate. We also provide evidence suggesting that formulas from one of our models are well suited for assessing solvers tuned to real-world instances. Finally, it is noteworthy that, to the best of our knowledge, our models and results on random disjunctive logic programs are the first of their kind.
Feb 13 2018 cs.LO
Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). By measuring how robustly a CPS run satisfies a specification, RV allows in addition, to quantify the resiliency of a CPS to perturbations. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework for RV, which takes advantage of the monoidal structure of runs (w.r.t. concatenation) and the semiring structure of a specification automaton (w.r.t. choice and concatenation), to compute in an incremental and application specific fashion the resiliency measure. This allows us to expose the core aspects of RV, by developing an abstract monitoring algorithm, and to strengthen and unify the various qualitative and quantitative approaches to RV, by instantiating choice and concatenation with real-valued functions as dictated by the application. We demonstrate the power and effectiveness of our framework on two case studies from the automotive domain.
Feb 13 2018 cs.LO
We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion, and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves orthogonal to the object of clocks. In the case of dependent types, this translates to a unique lifting condition similar to the one found in homotopy theoretic models of type theory. Since the universes defined by the standard Hofmann-Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. A large and technical part of the paper is devoted to showing that these can be constructed in such a way that inclusions between universes induced by inclusions of clock variable contexts commute on the nose with type operations on the universes.
Feb 13 2018 cs.LO
Event structures are a widely accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures where each event has a uniquely determined set of causes, called prime event structures, which in turn can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections. Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new class of event structures, called locally connected, by means of a chain of coreflection relying on an unfolding construction.
Contingency and accident are two important notions in philosophy and philosophical logic. Their meanings are so close that they are mixed sometimes, in both everyday discourse and academic research. This indicates that it is necessary to study them in a unified framework. However, there has been no logical research on them together. In this paper, we propose a language of a bimodal logic with these two concepts, investigate its model-theoretical properties such as expressivity and frame definability. We axiomatize this logic over various classes of frames, whose completeness proofs are shown with the help of a crucial schema. The interactions between contingency and accident can sharpen our understanding of both notions. Then we extend the logic to a dynamic case: public announcements. By finding the required reduction axioms, we obtain a complete axiomatization, which gives us a good application to Moore sentences.
We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.
This note proposes various axiomatizations of contingency logic under neighborhood semantics. In particular, by defining a suitable canonical neighborhood function, we give sound and complete axiomatizations of monotone contingency logic and regular contingency logic, thereby answering two open questions raised by Bakhtiari, van Ditmarsch, and Hansen. The canonical function is inspired by a function proposed by Kuhn in 1995. We show that Kuhn's function is actually equal to a related function originally given by Humberstone.
In this work, we give an algorithm by using Carroll diagrammatic method for deciding the syllogism is valid or not.