Accepted Papers with Abstracts
Marisa Navarro (Universidad del País Vasco (UPV/EHU), San Sebastián.)
Fernando Orejas (Universitat Politècnica de Catalunya, Barcelona.)
A refutation procedure for proving satisfiability of constraint specifications on XML documents

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.

Helmut Seidl (TU München)
Thomas Martin Gawlitza (The University of Sydney)
Martin Schwarz (TU München)
Parametric Strategy Iteration

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.

Karsten Martiny (Hamburg University of Technology)
Ralf Moeller (Hamburg University of Technology)
PDT Logic for Stream Reasoning in Multi-agent Systems

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.

Daniel Franzen (LFCS, University of Edinburgh)
David Aspinall (LFCS, University of Edinburgh)
Towards an amortized type system for JavaScript

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.

Cezary Kaliszyk (University of Innsbruck)
Lionel Mamane (None)
Josef Urban (Radboud University)
Machine Learning of Coq Proof Guidance: First Experiments

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.

Amina Saâdaoui (Sup'Com)
Nihel Ben Youssef (SUPCOM university)
Adel Bouhoula (Ecole superieure des communications de Tunis)
Automated detection and resolution of firewall misconfigurations

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.

Alexey Kytmanov (Siberian Federal University)
Alexey Shchuplev (Siberian Federal University)
Symbolic algorithm for construction of toric compactifications

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.

Maherzia Belaazi (Ecole superieure des communications de Tunis : Supcom)
Hanene Boussi Rahmouni (Ecole superieure des communications de Tunis : SupCom)
Adel Bouhoula (Ecole superieure des communications de Tunis : SupCom)
A Self-Disciplined Privacy Oriented Access Control Framework for Public Clouds

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.

Wided Ghardallou (Faculty of sciences of Tunis)
Nafi Diallo (NJIT)
Ali Mili (NJIT)
Merging Termination with Abort Freedom

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.

Nafi Diallo (CCS,New Jersey Institute of Technology)
Wided Ghardallou (Faculy of Sciences of Tunis)
Work-In-Progress: Repairing a Loop by Constructive Transformation using Mutation Analysis

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.

Alexander Baumgartner (Research Institute for Symbolic Computation)
Temur Kutsia (RISC, Johannes Kepler University Linz)
A Library of Anti-Unification Algorithms

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.