ABSTRACT. In this paper we first present three sorts of constraints (positive, negative and conditional ones) to specify that certain patterns must be satisfied in a XML document. These constraints are built on boolean XPath patterns. We define a specification as a set of clauses whose literals are constraints. Then, to reason about these specifications, we study some sound rules which permit to infer, subsume or simplify clauses. The main goal is to design a refutation procedure (based on these rules) to test if a given specification is satisfiable or not. We have formally proven the soundness of our procedure and we study the completeness and termination of the proposed method.

ABSTRACT. Program behavior may depend on parameters, which are either configured before compilation time, or provided at runtime, e.g., by sensors or other input devices. Parametric program analysis explores how different parameter settings may affect the program behavior.

In order to infer invariants depending on parameters, we introduce parametric strategy iteration. This algorithm determines the precise least solution of systems of integer equations depending on surplus parameters. Conceptually, our algorithm performs ordinary strategy iteration on the given integer system for all possible parameter settings in parallel. This is made possible by means of region trees to represent the occurring piecewise affine functions. We indicate that each required operation on these trees is polynomial-time if only constantly many parameters are involved.

Parametric strategy iteration for systems of integer equations allows to construct parametric integer interval analysis as well as parametric analysis of differences of integer variables. It thus provides a general technique to realize precise parametric program analysis if numerical properties of integer variables are of concern.

ABSTRACT. We present Probabilistic Doxastic Temporal (PDT) Logic for streams, a formalism to reason about probabilistic beliefs and their infinite temporal evolution in multi-agent systems. It enables the quantification of beliefs through probability intervals and incorporates the concepts of frequency functions and epistemic actions. We show how agents can update their beliefs with respect to their observations, provide a model for infinite streams of possible worlds and show how we can map clippings of these streams to finite time windows. Based on these time windows, we provide an appropriate semantics for PDT Logic, and show that PDT Logic for streams is decidable.

ABSTRACT. JavaScript programs have access to a wide range of resources and many of those have security implications. Tight bounds on the consumption of those resources can give indication of the functionality provided by the program and minimize the security risks of mobile applications. Resource consumption is typically dependent on the input of the user. In this paper we introduce an amortized type system for a core of JavaScript. The resulting types certify bounds for the resource usage dependent on the input parameters. We define the amortized types and the corresponding typing rules. Furthermore we discuss how to fully automatically infer those resource bounds for arbitrary applications. In addition to the usual example of amortized resource, heap-space, our type system can be applied to many phone specific resources, which we demonstrate using the example of the GPS sensor and others. The main result of this paper is the soundness of the core type system, proving that a valid type for a program corresponds to a bound on the units used of the specified resource.

ABSTRACT. We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependencies from the Coq proofs, the characterization of formulas that is used for the learning, and the evaluation method. Various machine learning methods are compared on a dataset of 5021 toplevel Coq proofs coming from the CoRN repository. The best resulting method covers on average 73% of the needed proof dependencies among the first 100 predictions, which is a comparable performance of such initial experiments on other large-theory corpora.

ABSTRACT. Firewalls provide efficient security services if they are correctly configured. Unfortunately, configuring a firewall is well known highly error prone and work-intensive if performed manually and become infeasible in the presence of a large number of rules in a firewall configuration. Therefore, there is a need of automated methods to analyze, detect and correct misconfigurations. Prior solutions have been proposed but we note their drawbacks are threefold: First, common approaches deal only with pairwise filtering rules. In such a way, some other classes of configuration anomalies could be uncharted. Second, they did not distinguish the intended firewall conflicts from the effective misconfigurations. Third, although anomalies resolution is a tedious task, it is generally given to the network administrator. We present, in this paper, a formal approach whose contributions are the following: Detecting new classes of anomalies, bringing out real misconfigurations and finally, proposing automatic resolution method by considering the security policy. We prove the soundness of our method. The first results we obtained are very promising.

ABSTRACT. Given a toric variety we present an algorithm that constructs a "larger" toric variety such that the initial one can be embedded in it as an infinite part. This compactification of an affine space generalizes the well-known decomposition of n-dimensional complex projective space.

ABSTRACT. While the transformative power of cloud computing in terms of cost scalability and agility is widely known, one of the first questions that arises is how the data hosted in the cloud-is accessed, stored and used? In this context, privacy preserving is a key user concern when judging the adoption of clouds in domains where sensitive personal information are highly involved. Indeed, as far as cloud providers are concerned, they should ensure the privacy protection of data hosted in clouds on behalf of their customers. Equally, they should satisfy the needs of law enforcement. It is a fact that access control is one of the essential and traditional security mechanisms of data protection. However, in the context of open and dynamic environments such as clouds, access control becomes more complicated. This is because the security policies, models and related mechanisms have to be defined across heterogeneous security domains. Thus, improving the current access control paradigms is crucial in order to ensure privacy compliance in distributed environments. In this paper, we aim to produce a self-disciplined access control framework for public clouds. We believe that a formal knowledge representation of access control policies, in particular, when these policies are able to integrate data protection requirements, could enforce privacy compliance at runtime. Indeed, we mainly focus on ontologies, as formalized conceptual models for access rules expression that conducts a private and secure reasoning. It could resolve issues like ambiguity in the expression of privacy legislation. The issue of the interoperability between various jurisdictions, denoted by the geographical area of the different cloud actors, could also be addressed in a formal manner.

ABSTRACT. Termination is the property of a program to complete its execution after a finite number of operations. Abort freedom is the property of a program to complete its execution without attempting an illegal operation, such as a division by zero, an arithmetic overflow, an array reference out of bounds, a reference to a nil pointer, etc. We present an approach to the analysis of iterative programs in which these two aspects are merged into a single formula. We illustrate our approach on a number of examples, and we compare our findings to related work on termination and on abort freedom.

ABSTRACT. One of the issues with traditional mutation testing is the possible large number of mutants generated. In this work, we illustrate how the concept of relative correctness can guide the generation and selection of mutants when repairing a loop program. We show that fewer and better mutants can be generated , thus adding efficiency by reducing the huge computational cost associated with mutation analysis.

ABSTRACT. Generalization problems arise in many areas of software science: code clone detection, program reuse, partial evaluation, program synthesis, invariant generation, etc. Anti-unification is a technique used often to solve generalization problems. In this paper we describe an open-source library of some newly developed anti-unification algorithms in various theories: for first- and second-order unranked terms, higher-order patterns, and nominal terms.