Speaker : Nicolas Peltier (CR CNRS, LIG Grenoble)
Title : A proof procedure in separation logic with inductive definitions
Abstract: Separation logic is used in program verification to facilitate reasoning on the dynamically allocated memory. In this talk, I will review recent results concerning the automation of reasoning in Separation logic with inductively defined predicates. In particular I will focus on an inductive proof procedure that is sound, complete and terminating for a fragment of inductive definitions satisfying the so called PCE conditions (Progress, Connectivity, Establishment).
Speaker : Clara Bertolissi (LIS)
Title : Access control policies specification and analysis
Abstract: Access control is a fundamental aspect of computer security; it aims at protecting resources from non-authorised users. The generalised use of access control in modern computing environments has increased the need for high-level declarative languages that enable security administrators to specify a wide range of policy models. In this talk we introduce the main notions of access control and define a declarative meta-model, called CBAC, able to subsume many of the most well known access control models (e.g., MAC, DAC, RBAC). We also design a graphical representation of CBAC policies that aims at easing the specification and verification tasks for security policy administrators. Using such representation of policies, answers to usual administrator queries can be automatically computed, and several properties of access control policies checked.
Speaker : Cameron Calk (Postdoc, LIS)
Title : Coherence via rewriting in higher Kleene algebras
Abstract: Squier’s coherence theorem and its generalisations provide a categorical interpretation of contracting homotopies via confluent and terminating rewriting. In particular, this approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, modal Kleene algebras (MKAs) have provided a description of properties of abstract rewriting systems, and classic (one-dimensional) consistency results have been formalised in this setting.
In this talk, I will recall the notion of higher Kleene algebra, introduced as an extension of MKAs, and which provide a formal setting for reasoning about (higher dimensional) coherence proofs for abstract rewriting systems. First, I will briefly discuss how rewriting techniques are captured in MKAs before showing how these techniques may be extended to higher dimensions.