Foundations for Decision Problems in Separation Logic with General Inductive Predicates
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExpTime-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is PI_2^p complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.
In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi.
We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents.
This volume contains the proceedings of the 17th International Conference on the Foundations of Software Science and Computation Structures, FOSSACS 2014, held in Grenoble, France, 5–13 April 2014. FOSSACS is an event of the Joint European Conferences on Theory and Practice of Software (ETAPS).
FOSSACS presents original papers on the foundations of software science. The conference invited submissions on theories and methods to support analysis, synthesis, transformation, and verification of programs and software systems.
We received 128 abstracts and 106 full paper s ubmissions; of these, 28 were selected for presentation at FOSSACS and inclusion in the proceedings.
The PC members, and the external experts they consulted, wrote over 320 paper reviews, and the discussion phase of the meeting included a 3-day author rebuttal phase. The competition was very strong, and unfortunately many good papers could not be accepted.
This volume contains the papers selected for presentation at the 18th European Symposium on Research in Computer Security (ESORICS 2013), held during September 9–13, 2013, in Egham, UK. In response to the symposium’s call for papers, 242 papers were submitted to the conference from 38 countries. These papers were evaluated on the basis of their significance, novelty, technical quality, as well as on their practical impact and/or their level of advancement of the field’s foundations. The Program Committee’s work was carri ed out electronically, yielding in- tensive discussions over a period of a few weeks. Of the papers submitted, 43 were selected for presentation at the conf erence (resulting in an acceptance rate of 18%). We note that many top-quality submissions were not selected for pre- sentation because of the high technical level of the overall submissions, and we are certain that many of these submissions will, nevertheless, be published at other competitive forums in the future.
It is well-known that the Dolev-Yao adversary is a powerful adversary. Besides acting as the network, intercepting, sending, and composing messages, he can remember as much information as he needs. That is, his memory is unbounded.
We recently proposed a weaker Dolev-Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev-Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where there is only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts nor an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev-Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 2).
The second contribution of this paper is the formalization of Progressing Collaborative Systems that may create fresh values, such as nonces. In this setting there is no unbounded adversary, although bounded memory adversaries may be present. We prove the NP-completeness of the reachability problem for Progressing Collaborative Systems that may create fresh values.
We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.