Search

Abstract: Self-adaptive behavior is a feature which architects needs to include in their systems in order to improve its reliability. However, despite several ways to get it, it is still hard to implement a self-adaptive system focused on non-functional properties. Difficulties to express quality attributes in the system without combining business logic with the self-adaptation logic and to include new services on runtime are some of them. In this paper we propose a model-driven analysis approach to offer a mechanism which allow the desired quality requirements to be expressed in a simple and non-intrusive manner, to find the best services available in a system and, to offer a code generation mechanism which takes the models created under the first objective and generates the necessary code for autonomously monitoring and adapting a SOA system. [Copyright &y& Elsevier]

Abstract: In this paper we describe a static analyser for Java bytecode which uses a combination of amortised analysis and Separation Logic due to Robert Atkey. With the help of Java annotations we are able to give precise resource utilisation constraints for Java methods which manipulate various heap-based data structures. [Copyright &y& Elsevier]

Abstract: Testing and verification of asynchronously communicating objects in open environments are challenging due to non-determinism. We explore a formal approach for black-box testing by proposing an interface specification language that gives an assumption-commitment style description of an object''s behavior. The approach is applied to Creol objects. Creol is a high-level, object-oriented modelling language, hence we do model-based testing of behavioral models. The testing is done by synchronising execution of a specification and the component under test. Due to the asynchronous nature of communication, testing should be done up-to observational equivalence. This leads to a large increase in the reachable state space for the test cases. We reduce the state space by using facilities for rewriting modulo AC (associativity and commutativity) built into the rewriting logic system Maude, and explore the state space by breadth first search. We present experimental results that show the usefulness of this approach. [Copyright &y& Elsevier]

Abstract: Recently, Brotherston & Kanovich, and independently Larchey-Wendling & Galmiche, proved the undecidability of the bunched implication logic BBI. Moreover, Brotherston & Kanovich also proved the undecidability of the related logic CBI, as well as its neighbours. All of the above results are based on encodings of two-counter Minsky machines, but are derived using different techniques. Here, we show that the technique of Larchey-Wendling & Galmiche can also be extended, via group Kripke semantics, to prove the undecidability of CBI. Hence, we propose an alternative direct simulation of Minsky machines into both BBI and CBI. We identify a fragment called elementary Boolean BI (eBBI) which is common to the BBI/CBI families of logics and we show that the problem of Minsky machine acceptance can be encoded into eBBI. The soundness of the encoding is derived from the soundness of a goal directed sequent calculus designed for eBBI. The faithfulness of the encoding is obtained from a Kripke model based on the free commutative group . [Copyright &y& Elsevier]

Abstract: Many formal systems, particularly in computer science, may be expressed through equations modulated by assertions regarding the ''freshness of names''. It is the presence of binding operators that make such structure non-trivial. Clouston and Pitts''s Nominal Equational Logic presented a formalism for this style of reasoning in which support for name binding was implicit. This paper extends this logic to offer explicit support for binding and then demonstrates that such an extension does not in fact add expressivity. [Copyright &y& Elsevier]

Abstract: This paper presents a formal framework for compositional reasoning about secure systems. A key insight is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is confined to the interfaces it has access to, but may combine interface calls without restriction. Compositional reasoning for such systems is based on an extension of rely-guarantee reasoning for system correctness [Misra, J. and K.M. Chandy, Proofs of networks of processes, IEEE Transactions on Software Engineering 7 (1981), pp. 417–426; Jones, C.B., Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS) 5 (1983), pp. 596–619] to a setting that involves an adversary whose exact program is not known. At a technical level, the paper presents an expressive concurrent programming language with recursive functions for modeling interfaces and a logic of programs in which compositional reasoning principles are formalized and proved sound with respect to trace semantics. The methods are illustrated through a small fragment of an idealized file system. [Copyright &y& Elsevier]

Abstract: Natural deduction (ND) for first order classical logic is obtainable from the intuitionist system by the addition of Peirce rule. In a previous paper [Luiz Carlos Pereira, Edward Hermann Haeusler, Vaston G. Costa, and Wagner Sanz. Normalization for the implicational fragment of classical propositional logic. Submited to a Journal, 2008], it was presented a normalization strategy for the implicational fragment with Pierce rule. The end normal form is divided in two parts: an intuitionist subdeduction followed by a series of Peirce rule applications, maybe empty. Here, we extend this normalization process to the system for first order classical logic NP system. NP normal derivations also present the same structure. This structure is the basis on which many properties for ND derivations can be presented. In particular, we present a form of Glivenko''s theorem for the conjunction-implication fragment. Unfortunately, NP lacks strong normalization, although ND with classical absurdity rule doesn''t lack it, as it''s well-known. [Copyright &y& Elsevier]

Abstract: Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a “light-weight” algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach. [Copyright &y& Elsevier]

Abstract: We consider a simple modal logic whose non-modal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of (e.g.) T, S4 and S5, such logics are useful, as shown in previous work by Baltag, Coecke and the first author, for encoding and reasoning about information and misinformation in multi-agent systems. For such a logic we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario. [Copyright &y& Elsevier]

Abstract: Type assignment systems for λ-calculus based on intersection types are a general framework for building models of λ-calculus (known as filter-models) which are useful tools for reasoning in a finitary way about the denotational interpretation of terms. Indeed the denotation of a term is the set of types derivable for it and a type is a “finite piece” of information on such a denotation. This approach to the λ-calculus semantics is called in the literature logical semantics, and it has been intensively studied in relation with λ-models in the Scott''s domain setting. In this paper we define two intersection type assignment systems for λ-calculus, parametric with respect to a coherence relation between types. We prove that, when the instantiation of the parameter satisfies a given condition, our two type systems induce models of λ-calculus, that we call clique-models. Lastly we show that such systems give a logical characterization of two classes of models built on the category of Girard''s coherence spaces and stable functions [Copyright &y& Elsevier]

Abstract: In the standard sequent presentations of Girard''s Linear Logic [Girard, J.-Y., Linear logic, Theoretical Computer Science 50 (1987), pp. 1–102] (LL), there are two “non-decreasing” rules, where the premises are not smaller than the conclusion, namely the cut and the contraction rules. It is a universal concern to eliminate the cut rule. We show that, using an admissible modification of the tensor rule, contractions can be eliminated, and that cuts can be simultaneously limited to a single initial occurrence. This view leads to a consistent, but incomplete game model for LL with exponentials, which is finitary, in the sense that each play is finite. The game is based on a set of inference rules which does not enjoy cut elimination. Nevertheless, the cut rule is valid in the model. [Copyright &y& Elsevier]

Abstract: We introduce a semantic approach to the study of logics for access control and dependency analysis, based on Game Semantics. We use a variant of AJM games with explicit justification (but without pointers). Based on this, we give a simple and intuitive model of the information flow constraints underlying access control. This is used to give strikingly simple proofs of non-interference theorems in robust, semantic versions. [Copyright &y& Elsevier]

Abstract: Bove and Capretta have presented a method to deal with partial and general recursive functions in constructive type theory which relies on an inductive characterisation of the domains of the functions. The method separates the logical and the computational aspects of an algorithm, and facilitates the formal verification of the functions being defined. For nested recursive functions, the method uses Dybjer'' schema for simultaneous inductive-recursive definitions. However, not all constructive type theories support this kind of definitions. Here we present a new approach for dealing with partial and general recursive functions that preserves the advantages of the method by Bove and Capretta, but which does not rely on inductive-recursive definitions. In this approach, we start by inductively defining the graph of the function, from which we first define the domain and afterwards the type-theoretic version of the function. We show two ways of proving the formal specification of the functions defined with this new approach: by induction on the graph, or by using an induction principle in the style of the induction principle associated to the domain predicates of the Bove-Capretta method. [Copyright &y& Elsevier]

Abstract: We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termination of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity allows us to show actual theorem-prover code of the formal proofs. The formalisations are done in Nominal Isabelle, a definitional extention of the theorem prover Isabelle/HOL. The point of these formalisations is to be as close as possible to the “pencil-and-paper” proofs for these properties, but of course be completely rigorous. We describe where Nominal Isabelle is of great help with such formalisations and where one has to invest additional effort in order to obtain formal proofs. [Copyright &y& Elsevier]

Abstract: IEEE 802.11 is a widely used technology which powers many of the digital wireless communication revolutions currently taking place. It uses OFDM (Orthogonal Frequency Division Multiplexing) in its physical layer which is an efficient way to deal with multipath, good for relatively slow time-varying channels, and robust against narrowband interference. In this paper, we formally specify and verify an implementation of the IEEE 802.11 standard physical layer based OFDM modem using the HOL (Higher Order Logic) theorem prover. The versatile expressive power of HOL helped us model the original design at all abstraction levels starting from a floating-point model to the fixed-point design and then synthesized and implemented in FPGA technology. We have been able to find a bug in one of the blocks of the design that is responsible for modulation which implementation diverts from the constellation provided in the IEEE standard specification. The paper also derives new expressions for the rounding error accumulated during ideal real to floating-point and fixed-point transitions at the algorithmic level and performs a formal error analysis for the OFDM modem in HOL. [Copyright &y& Elsevier]

Abstract: We use a modal logic in order to show that the strategy-based rewrite semantics for membrane systems fully preserves the maximal concurrency of evolution rules actions, whereas the maximal concurrency of communication actions and structural actions is partially preserved. Consequently, the strategy-based rewrite semantics describes more faithfully the behavior of the membrane systems than the rewrite logic-based semantics. It is known that the rewrite logic-based semantics implements the maximal concurrency of the evolution rules in membrane systems only by interleaving concurrency. The concurrency degrees of the communication and structural actions are the same for the two rewrite-based semantics. [Copyright &y& Elsevier]

Abstract: We use strategies to specify how a wide range of exercises can be solved incrementally, such as bringing a logic proposition to disjunctive normal form, reducing a matrix, or calculating with fractions. With such a strategy, we can automatically generate worked-out solutions, track the progress of a student by inspecting submitted intermediate answers, and report back suggestions in case the student deviates from the strategy. Because we can calculate all kinds of feedback automatically from a strategy specification, it becomes less labor-intensive and less ad-hoc to specify new exercise domains and exercises within that domain. A strategy describes valid sequences of transformation rules that solve the exercise at hand, which turns tracking intermediate steps into a parsing problem. This is a promising view at the problem because it allows us to take advantage of many years of experience in parsing sentences of context-free languages, and transfer this knowledge and technology to the domain of stepwise solving exercises. In this paper we work out the similarities between parsing and solving exercises incrementally, and we discuss the implementation of a recognizer for strategies. We present a full implementation of such a recognizer, and discuss a number of design choices we have made. In particular, we discuss the use of a fixed point combinator to deal with repetition, and labels to mark positions in the strategy. [Copyright &y& Elsevier]

Abstract: In this paper we discuss and compare abstract machines for the lambda-calculus, implementing various evaluation strategies. Starting from the well-known Categorical abstract machine (CAM) and Krivine''s abstract machine (KAM), we develop two families of machines that differ in the way they treat environments. The first family is inspired by the work on closed reduction strategies, whereas the second is built in the spirit of the jumping machines based on the work done on Linear Logic. [Copyright &y& Elsevier]

Abstract: In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion. [Copyright &y& Elsevier]

Abstract: This paper introduces a new object-oriented specification and modeling language called DeSpec. The language targets primarily model checking in the Windows NT kernel driver environment. It integrates the majority of Zing modeling language features and adds means for defining parameterized abstractions of the environment at varying levels of detail. The DeSpec language also enables capturing constrains imposed on drivers by the Windows kernel in a form of quantified temporal logic patterns – easy-to-read templates of LTL formulae introduced by the Bandera toolset. [Copyright &y& Elsevier]

Abstract: The intention of this paper is to extend the generic component framework presented at FASE 2002 [H. Ehrig, F. Orejas, B. Braatz, M. Klein, and M. Piirainen. A Generic Component Concept for System Modeling. In Proc. FASE 2002: Formal Aspects of Software Engineering, volume 2306 of Lecture Notes in Computer Science, pages 32–48. Springer Verlag, 2002] to allow component verification based on export-import implications. In the generic component framework components with explicit import, export interfaces and a body specification connected by embeddings and transformations provide hierarchical composition of components with a compositional transformation semantics. We introduce implications that relate sentences of the import stating what the component requires to sentences of the export stating what the component guarantees. The main result of this paper is that these import-export implications are compatible with the hierarchical composition as given in [H. Ehrig, F. Orejas, B. Braatz, M. Klein, and M. Piirainen. A Generic Component Concept for System Modeling. In Proc. FASE 2002: Formal Aspects of Software Engineering, volume 2306 of Lecture Notes in Computer Science, pages 32–48. Springer Verlag, 2002]. The second part illustrates how this abstract concept can be instantiated to Petri net systems. [Copyright &y& Elsevier]

Abstract: Turning type and effect deduction systems into an algorithm is a tedious and error-prone job, and usually results in an implementation that leaves no room to modify the solving strategy, without actually changing it. We employ constraints to declaratively specify the rules of a type system. Starting from a constraint based formulation of a type system, we introduce special combinators in the type rules to specify in which order constraints may be solved. A solving strategy can then be chosen by giving a particular interpretation to these combinators, and the resulting list of constraints can be fed into a constraint solver; thus the gap between the declarative specification and the deterministic implementation is bridged. This design makes the solver simpler and easier to reuse. Our combinators have been used in the development of a real-life compiler. [Copyright &y& Elsevier]

Abstract: This paper addresses the design of architectures for proximity-aware services with unobtrusive and context-based identification and authentication features. A service is “proximity-aware” when it automatically detects the presence of entities in its proximity. A process of authentication is “context-based” when it uses contextual information to discern among different identities and to evaluate whether they are authentic or not. We refer to an existing architecture, available in our institute, where a network of sensors is used to detect the presence users and user devices in various locations in the building. Proximity-aware services are offered at intelligent coffee corners where users are unobtrusively identified and authenticated while approaching. A level of authentication for an approaching identity is calculated as the overall expectation of belief (i.e., trust) that the identity (and not another) is effectively standing at the coffee space. We use the Subjective Logic as a theoretic framework for belief calculations. According to a previous study of ours, we manage each sensors as it was a recommender giving subjective “opinions” over statements concerning the position of users. Informally, an identity has higher level of authentication in a certain place the more sensors-recommenders believe that that identity stands in that place. We present and comment the results from an array of experiments where we show how trust can be used to authenticate an identity in a room. We perform the experiments under different circumstances, namely we change the area of the room and the relative disposition of the sensors. We comment the results and we indicate some guidelines for a design that aims to maximise its benefits from our authentication framework. [Copyright &y& Elsevier]

Abstract: Protocol composition logic, PCL, is a formal approach for proving security properties of a class of network protocols. PCL involves reasoning directly about properties achieved by protocols steps, in a setting that does not require explicit reasoning about attacker actions. The method relies on protocol invariants to combine properties of different roles of a protocol. While some protocol invariants can be complex to identify and prove, many useful PCL invariants are relatively straightforward consequences of the programs (roles) executed by the agents involved in the protocol. We present a logic program based approach for automating proofs of invariants that appears effective for invariants that are required for several standardized, widely deployed protocols. We use the well-known Transport Layer Security Protocol (TLS/SSL) to illustrate the approach. [Copyright &y& Elsevier]

Abstract: As an extension to Floyd-Hoare logic, separation logic has been used to facilitate reasoning about imperative programs manipulating shared mutable data structures. Recently, it has also been extended to support modular reasoning in Java-like object-oriented languages where only single inheritance is allowed. In this paper we propose an extension of separation logic to support also the reasoning for multiple inheritance in C++ -like languages. To cater for multiple inheritance, we modified the standard storage model for separation logic in a way that the correct reference to a field or a method can be easily determined. On top of this storage model, a set of proof rules are proposed. Our verification system also provides basic support for behavioral subtyping. [Copyright &y& Elsevier]

Abstract: We describe some results inspired to Lafont''s Soft Linear Logic (SLL) which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations. SLL is the basis for the design of type assignment systems for lambda-calculus, characterizing the complexity classes PTIME, PSPACE and NPTIME. PTIME is characterized by a type assignments system where types are a proper subset of SLL formulae. The characterization consists in the fact that a well typed term can be reduced to normal form by a number of beta-reductions polynomial in its lenght, and moreover all polynomial time functions can be computed by well typed terms. PSPACE is characterized by a type assignment system obtained from the previous one, by extending the set of types by a type for booleans, and the lambda-calculus by two boolean constants and a conditional constructor. The system assigns types to terms in such a way that the evaluation of programs (closed terms of type boolean) can be performed carefully in polynomial space. Moreover all polynomial space decision problems can be computed by terms typable in this system. In order to characterize NPTIME we extend the lambda-calculus by a nondeterministic choice operator, and the system by a rule for dealing with this new term constructor. [Copyright &y& Elsevier]

Abstract: There have been several research works that analyze and optimize programs using temporal logic. However, no evaluation of optimization time or execution time of these implementations has been done for any real programming language. In this paper, we present a system that generates a Java optimizer from specifications in temporal logic. The specification is simpler, and the generated optimizers run more efficiently than previously reported work. We implemented a new model checker for a bidirectional CTL (computational tree logic) called CTL bd , which is equivalent to CTL-FV [Lacey, D., Jones, N.D., Van Wyk, E. and Frederiksen, C.C.: Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation, Vol. 17, No. 3, pp. 173–206, 2004] after removing free variables. The model checker can check future and past temporal CTL operators symmetrically without any conversion. We also present a new specification language based on the bidirectional CTL that can express typical optimization rules very naturally. By adding rewriting conditions to allow for temporary variables and considering real-world language features such as exceptions, the system can perform optimization of Java programs. So far, a compiler optimizer using temporal logic was assumed to be impractical, because it consumes too much time. However, with our method, the generated Java compiler optimizer can compile seven of the SPECjvm98 benchmarks with a compile time from 4 seconds to 4 minutes. [Copyright &y& Elsevier]

Abstract: This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles. [Copyright &y& Elsevier]

Abstract: Current mechanizations of programming logics are often in the form of verification condition generators. These front ends to a prover translate a program and assertions into conditions that state that the program fulfills its assertions. Traditional verification condition generators are monolithic encapsulations of a programming language''s semantics. This makes it hard to build such verification generators when designing a new language, or when extending a language. We propose a more compositional method of building verification condition generators, using ideas from monadic denotational semantics and from generic programming. Our technique allows us to extend an existing verification condition generator to handle new language constructs, but also to add extensions at another level, such as the ability to generate validation traces. We explain the technique through an example, extending a simple while language with a construct for exception handling. This construct not only needs an extension to the logic, but also a change of its structure. [Copyright &y& Elsevier]

Abstract: In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou developed a sound and relatively complete Duration Calculus as an extension of NL. We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get many properties for free. As one important result we obtain that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we discuss other interval operations like Allen''s 13 relations between intervals and their relationship to semiring neighbours. Then we present some possible interpretations for neighbours beyond interval settings. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirings to Kleene algebras and ω algebras. These extensions are useful for formulating properties of repetitive procedures like loops. [Copyright &y& Elsevier]

Abstract: In this paper we use a program logic and automatic theorem provers to certify resource usage of low-level bytecode programs equipped with annotations describing resource consumption for methods. We have adapted an existing resource counting logic [Aspinall, D., L. Beringer, M. Hofmann, H.-W. Loidl and A. Momigliano, A program logic for resource verification, in: Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004), Lecture Notes in Computer Science 3223 (2004), pp. 34–49] to fit the first-order setting, implemented a verification condition generator, and tested our approach on programs that contain recursion and deal with recursive data structures. We have successfully applied our framework to programs that did not involve any updates to recursive data structures. But mutation is more tricky because of aliasing of heap. We discuss problems related to this and suggest techniques to solve them. [Copyright &y& Elsevier]

Abstract: The interpretative approach to compilation allows compiling programs by partially evaluating an interpreter w.r.t. a source program. This approach, though very attractive in principle, has not been widely applied in practice mainly because of the difficulty in finding a partial evaluation strategy which always obtain “quality” compiled programs. In spite of this, in recent work we have performed a proof of concept of that, at least for some examples, this approach can be applied to decompile Java bytecode into Prolog. This allows applying existing advanced tools for analysis of logic programs in order to verify Java bytecode. However, successful partial evaluation of an interpreter for (a realistic subset of) Java bytecode is a rather challenging problem. The aim of this work is to improve the performance of the decompilation process above in two respects. First, we would like to obtain quality decompiled programs, i.e., simple and small. We refer to this as the effectiveness of the decompilation. Second, we would like the decompilation process to be as efficient as possible, both in terms of time and memory usage, in order to scale up in practice. We refer to this as the efficiency of the decompilation. With this aim, we propose several techniques for improving the partial evaluation strategy. We argue that our experimental results show that we are able to improve significantly the efficiency and effectiveness of the decompilation process. [Copyright &y& Elsevier]

Abstract: A distinctive feature of modern functional logic languages like Toy or Curry is the possibility of programming non-strict and non-deterministic functions with call-time choice semantics. For almost ten years the CRWL framework [J.C. González-Moreno, T. Hortalá-González, F. López-Fraguas, and M. Rodríguez-Artalejo. A rewriting logic for declarative programming. In Proc. European Symposium on Programming (ESOP''96), pages 156–172. Springer LNCS 1058, 1996, J.C. González-Moreno, T. Hortalá-González, F. López-Fraguas, and M. Rodríguez-Artalejo. An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1):47–87, 1999] has been the only formal setting covering all these semantic aspects. But recently [E. Albert, M. Hanus, F. Huch, J. Oliver, and G. Vidal. Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40(1):795–829, 2005] an alternative proposal has appeared, focusing more on operational aspects. In this work we investigate the relation between both approaches, which is far from being obvious due to the wide gap between both descriptions, even at syntactical level. [Copyright &y& Elsevier]

Abstract: Reductants are a useful theoretical tool introduced for proving correctness properties in the context of generalized annotated logic programming. This concept was adapted to the more recent and flexible framework of multi-adjoint logic programming for solving a problem of incompleteness that arises when working with some lattices. In order to be complete, multi-adjoint logic programs must be extended with their set of reductants. In general, the notion of reductant may introduce an important efficiency drawback. In this work we provide a more refined version of this concept that we call PE-reductant, by using (threshold) partial evaluation techniques. Our proposal is intended to be semantically equivalent to the classical notion of reductant, and improves previous approaches at least in the following two efficiency criteria. Firstly, using the new definition of reductant, we can obtain computed answers for a given goal with a lesser computational effort than by using its precedent ones. Secondly, the proper construction of a reductant by means of partial evaluation methods, is drastically improved after introducing thresholding techniques which dynamically reduce the size of the underlying unfolding trees. [Copyright &y& Elsevier]

Abstract: This paper presents a proposal for the cooperation of solvers in constraint functional logic programming, a quite expressive programming paradigm which combines functional, logic and constraint programming using constraint lazy narrowing as goal solving mechanism. Cooperation of solvers for different constraint domains can improve the efficiency of implementations since solvers can take advantage of other solvers'' deductions. We restrict our attention to the cooperation of three solvers, dealing with syntactic equality and disequality constraints, real arithmetic constraints, and finite domain () constraints, respectively. As cooperation mechanism, we consider to propagate to the real solver the constraints which have been submitted to the solver (and viceversa), imposing special communication constraints to ensure that both solvers will allow the same integer values for all the variables involved in the cooperation. [Copyright &y& Elsevier]

Abstract: Programs in modern functional logic languages are rewrite systems following the constructor discipline but where confluence and termination are not required, thus defining possibly non strict and non-deterministic functions. While in practice and in some theoretical papers rewrite rules can contain extra variables in right hand sides, some other works and techniques do not consider such possibility. We address in this paper the question of whether extra variables can be eliminated in such kind of functional logic programs, proving the soundness and completeness of an easy solution that takes advantage of the possibility of non-confluence. Although the focus of the paper is mainly theoretical, we give some first steps towards the practical usability of the technique. [Copyright &y& Elsevier]

Abstract: The integration of declarative paradigms such as functional-logic and fuzzy-logic programming seems to be an interesting challenge in the design of highly expressive declarative languages where mathematical functions cohabit with fuzzy logic features. Starting with two representative languages from both settings, namely Curry and Likelog, we have recently proposed an hybrid dialect where a set of (Curry) rewrite rules together with a set of (Likelog) similarity equations can be safely executed by means of a fuzzy variant of needed narrowing. This paper is devoted to show some important properties enjoyed by the new narrowing strategy. Firstly, we prove the termination of the process which determines the set of tuples that enable new narrowing steps for a given term. Termination in the fuzzy context is not trivial since, apart that it is required to compute the transitive closure of the initial set of similarity equations, it is also mandatory to ensure the finiteness of the set of recursive calls performed by the narrowing strategy, as well as that each call never falls into an infinite loop. From here, we prove two important (somehow complementary) properties, that we call crispness and fuzziness, respectively. The first one implies that the new strategy is (at least) conservative with respect to the original one of needed narrowing, in the sense that each tuple obtained in the crisp case, is also replicated (with the maximum truth degree) in the fuzzy case. On the other hand, fuzziness means the maximality of the new strategy when exploiting (as much as possible) the similarity relations collected in a given program. [Copyright &y& Elsevier]

Abstract: Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proofs using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge. [Copyright &y& Elsevier]

Abstract: The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we present a monadic datatype to represent the state information of a proof and we illustrate its use in the PVS theorem prover. We show how this representation can be used to design a new set of powerful tacticals for PVS, called PVS#, that have a simpler and clearer semantics compared to the semantics of standard PVS tacticals. [Copyright &y& Elsevier]

Abstract: The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that an inference system generates finitely many clauses from the presentation of a theory and a finite set of ground unit clauses, then any fair strategy based on that system can be used as a -satisfiability procedure. In this paper, we introduce a set of sufficient conditions to generalize the entire framework of rewrite-based -satisfiability procedures to rewrite-based -decision procedures. These conditions, collectively termed subterm-inactivity, will allow us to obtain rewrite-based -decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures. [Copyright &y& Elsevier]

Abstract: We introduce a new framework for describing computations which are both concurrent and probabilistic. This framework is a natural extension of the Configuration Theories of [Pietro Cenciarelli. Configuration theories. In CSL ''02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, pages 200–215, London, UK, 2002. Springer-Verlag], and allows to express properties about both the causal and the probabilistic aspect of concurrent computations. Computations are described in an axiomatic way, by using a probabilistic extensions of poset sequents. A scheme of structural rules on these sequents is introduced and shown to be sound, while completeness can be obtained by adding a rule which is not treated in the present work. We also introduce a new probabilistic extension of Configuration Structures, which we use as models for probabilistic sequents. [Copyright &y& Elsevier]

Abstract: We show that there exists an almost everywhere (a.e.) dominating computably enumerable (c.e.) degree which is half of a minimal pair. [Copyright &y& Elsevier]

Abstract: Software systems evolve over time. To facilitate this, the coordination language Reo offers operations to dynamically reconfigure the topology of component connectors. We present a semantics of Reo in the presence of reconfiguration, and a logic, and its model checking algorithm, for reasoning about connector behaviour in this setting. [Copyright &y& Elsevier]

Abstract: We propose a formal method to validate the reliability of a web application, by modeling interactions among its constituent objects. Modeling exploits the recent “Multiple Levels of Integrity” mechanism which allows objects with dynamically changing reliability to cooperate within the application. The novelty of the method is the ability to describe systems where objects can modify their own integrity level, and react to such changes in other objects. The model is formalized with a process algebra, properties are expressed using the ACTL temporal logic, and can be verified by means of a model checker. Any instance of the above model inherits both the established properties and the proof techniques. To substantiate our proposal we consider several case-studies of web applications, showing how to express specific useful properties, and their validation schemata. Examples range from on-line travel agencies, inverted Turing test to detect malicious web-bots, to content cross-validation in peer to peer systems. [Copyright &y& Elsevier]

Abstract: In this paper we develop the language theory underpinning the logical framework PLF. This language features lambda abstraction with patterns and application via pattern-matching. Reductions are allowed in patterns. The framework is particularly suited as a metalanguage for encoding rewriting logics and logical systems where proof terms have a special syntactic constraints, as in term rewriting systems, and rule-based languages. PLF is a conservative extension of the well-known Edinburgh Logical Framework LF. Because of sophisticated pattern matching facilities PLF is suitable for verification and manipulation of HXML documents. [Copyright &y& Elsevier]

Abstract: This paper describes a Java-based framework for the development of component-based software systems supporting the specification of the logic of component interactions as a first-class aspect. Java is used as the reference development language. On the one side, the framework makes it possible to specify the logic of interaction at the component-level, in terms of input and output interfaces, the events generated and observed by a component, and related information about the management of the control flow. On the other side, it is possible to specify the logic of interaction at the inter-component level, providing a modelling and linguistic support for designing and (dynamically) programming the glue among the components, enabling general forms of observation, control and construction of the interaction space. As a result, the framework supports the coordination of components at different levels: from interoperability among heterogeneous and unknown components, to the support for dynamic introduction, removal and update of components, to general coordination patterns, such as workflow. The framework adopts first-order logic as the reference computational model for describing and defining the logic of interaction: the modalities adopted by components to interact, the coordination laws gluing the components and the interaction events occurring in the system are expressed as facts and rules. They compose the (evolving) logic theories describing and defining the interaction at the system level, and can be observed and controlled at runtime to allow dynamic re-configurability. [Copyright &y& Elsevier]

Abstract: We present a meta-logic that contains a new quantifier ∇ (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The ∇ quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation. [Copyright &y& Elsevier]

Abstract: The Rewriting Calculus has been proposed as a language for defining term rewriting strategies. Rules are explicitly represented as terms, and are applied explicitly to other terms to transform them. Sets of rules may be applied to (sets of) terms non-deterministically to obtain sets of results. Strategies are implemented as rules which accept other rules as arguments and apply them in certain ways. This paper describes work in progress to strengthen the Rewriting Calculus by giving it a logical semantics. Such a semantics can provide crucial guidance for studying the language and increasing its expressive power. The latter is demonstrated by adding support to the Rewriting Calculus for what we call higher-form rewriting, where rules rewrite other rules. The logical semantics used is based on ordered linear logic. The paper develops the ideas through several examples. [Copyright &y& Elsevier]

Abstract: Many proof search strategies can be expressed as restrictions on the order of application of the rules of the sequent calculus. Properties of these strategies are then shown by permutation arguments, such as showing that a given strategy is complete by transforming an arbitrary proof into one which obeys the strategy. Such analyses involve some very tedious manipulations of proofs, and are potentially overwhelming for humans. In this paper we investigate the development of systematic techniques for the analysis of sequent calculi. We show how a particular specification of inference rules leads to a detailed analysis of permutation properties for these rules, and we also investigate how to detect redundancies in proofs resulting from these rules. [Copyright &y& Elsevier]

Abstract: Model checking of LTL formulæis traditionally carried out by a conversion to Büchi automata, and there is therefore a large body of research in this area including some recent studies on the use of alternating automata as an intermediate representation. Bounded model checking has until recently been apart from this, typically using a direct conversion from LTL to propositional logic. In this paper we give a new bounded model checking encoding using alternating automata and focus on the relationship between alternating automata and SNF. We also explore the differences in the way SNF, alternating, and Büchi automata are used from both a theoretical and an experimental perspective. [Copyright &y& Elsevier]