Abstract   Partners   Events   Publications   Contact   Focus Science CNRS

NARCO is a research project funded by the French National Research Agency (ANR) under grant ANR-21-CE48-0011.

It is devoted to reasoning on non-aggregative resource composition in separation logic.

Duration: January 1 2022-December 31 2026.

---

Abstract

The complexity faced by the design of a computer system can be tackled by a high degree of modularity. Modularity is instrumental in maintaining a system throughout its lifetime, by performing updates and reconfigurations. These systems control important aspects of our lives, thus the importance of ensurring their correct behavior, by using formal models and verification techniques. This project provides a basis for the design and verification of complex systems, based on the formal notions of resource and composition. By resource we understand any (physical or logical) component of a system and composition accounts for the interaction of components. The composition operators need thus to be more general than simple aggregative compositions (disjoint unions). We shall devise logics encompassing these general notions of non-aggregative compositions. Special interest is given to the development of automated reasoning and system verification techniques.

---

Partners

• LIG (Laboratory of Informatics of Grenoble) - CNRS
  • N. Peltier
  • M. Echenim
• LMF (Laboratoire Méthodes formelles) - ENS Saclay
  • M. Sighireanu
  • S. Demri
  • P.-A. Mellies
  • Q. Petitjean
• LORIA - Univ. of Lorraine
  • D. Galmiche
  • B. Izart
  • D. Larchey-Wending
  • D. Méry
• Verimag - CNRS
• R. Iosif
• S. Bliudze
• M. Bozga
• L. Bueri

---

Events

• First plenary meeting on February 11 2022 (virtual).
  • Local Reasoning about Parameterized Reconfigurable Distributed Systems (R. Iosif)
  • Labelled Tableaux for a Linear Time Bunched Implication Logic (D. Méry)
  • The Coq Library of Undecidability Proofs (D. Larchey-Wending)
  • Deciding verification problems for heap-lists (M. Sighireanu)
  • A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning (N. Peltier)
• Second plenary meeting on July 7 2022 (Paris, IRIF).
  • Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (L. Bueri)
  • Relating Labelled and Label-Free Bunched Calculi in BI Logic (D. Méry)
  • A Framework for Reasoning about Dynamic Axioms in Description Logics (S. Demri)
  • Toward Polynomial-Time Proof Procedures in Separation Logic with Inductively Defined Predicates (N. Peltier)
• ASL (Workshop on Advancing Separation Logics) on July 31 2022.
• Third plenary meeting on December 8 2022 (Paris, IRIF).
  • Expressiveness Results for an Inductive Logic of Separated Relations (R. Iosif, joint work with F. Zuleger, TU Wien)
  • On an Invariance Problem for Parameterized Concurrent Systems (L. Bueri)
  • On the satisfiability problem for SL formulas with inductive definitions and permissions (N. Peltier)
• On February 2 2023, L. Bueri gave a presentation at Verimag on the paper "Logical Characterization of the Sets of Hypergraphs Defined by Hyperedge Replacement Grammars” by Bruno Courcelle and Joost Engelfriet
• Fourth plenary meeting on June 22 2023 (Paris).
  • What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? (Q. Petitjean)
  • Overlaid Data Structures (M. Sighireanu)
  • The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations (M. Bozga)
  • On the Definability of Context-free Sets of Graphs in (Counting) MSO (R. Iosif)
  • Bi-Intuitionistic BI: Models and Proofs (B. Izart)
• Fifth plenary meeting on March 13 2024 (Paris).
  • Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations (Radu Iosif)
  • JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java (Simon Bliudze)
  • Tree-Verifiable Graph Grammars (Mark Chimes)
  • Relating Label-free and Labelled Sequent Calculi in Intuitionistic Sentential Logic with Identity (Daniel Méry)
  • A Direct Decision Procedure for Testing Entailment in Relational Separation Logic (Nicolas Peltier)
• Sixth plenary meeting on December 11-12 2024 (Grenoble).
  • Cyclic proofs for Linear Time Bunched Implications Logic (Benjamin Izart)
  • Regular Grammars for Sets of Graphs of Tree-Width 2 (Radu Iosif)
  • The Entailment Problem for SL Formulas with PCE Inductive Rules and Overlaid Data Structures (Quentin Petitjean)
  • The Entailment Problem in Separation Logic with Permissions and Domain Variables (Nicolas Peltier)
• Seventh plenary meeting on January 29-30 2025 (Saclay).
  • Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Adam Rogalewicz, joint Verification seminar at IRIF)
  • Bifurcation Logic: Separation Through Ordering (D. Méry)
  • Optimal Recognizers for Unranked and Unordered Trees and Series-Parallel Graphs (R. Iosif)
  • Iterating Non-Aggregative Structure Compositions (F. Zuleger)
  • Bi-Intuitionistic Bunched Implications logic: Beth Semantics and Axiomatization (B. Izart)
• Quentin Petitjean defended his thesis Automated Tools for Inductive Reasoning in Separation Logic (ENS Saclay).

---

---

Contact

N. Peltier (scientific leader of the project).