NARCO - Non-Aggregative Resource COmpositions

Abstract Partners Events Publications Contact

NARCO is a research project funded by the ANR under grant ANR-21-CE48-0011. It is devoted to reasoning on non-aggregative resource composition in separation logic. The project started on January 1 2022. Its duration is 4 years.

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)

Publications

Here are some publications related to the project. See also HAL

Demri, S., Etienne Lozes, & Mansutti, A. (2021). The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic. ACM Trans. Comput. Log., 22(2), 14:1-14:56.

Demri, S., Fervari, R., & Mansutti, A. (2021). Internal proof calculi for modal logics with separating conjunction. J. Log. Comput., 31(3)

Echenim, M., Iosif, R., & Peltier, N. (2020). The Bernays-Schoenfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log., 21(3), 19:1-19:46.

Echenim, M., Iosif, R., & Peltier, N. (2022). Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules. Inf. Process. Lett., 173, 106169.

Echenim, M., Iosif, R., & Peltier, N. (2021a). Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. In C. Baier & J. Goubault-Larrecq (Eds.), 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference) (Vol. 183, p. 20:1-20:18). Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

Echenim, M., Iosif, R., & Peltier, N. (2021b). Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In A. Platzer & G. Sutcliffe (Eds.), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings (Vol. 12699, pp. 183-199). Springer.

Galmiche, D., & Méry, D. (2021). Labelled cyclic proofs for separation logic. J. Log. Comput., 31(3), 892-922.

Sighireanu, M. (2021). SL-COMP: competition of solvers for separation logic. Int. J. Softw. Tools Technol. Transf., 23(6), 895-903.

Echenim, M., and Peltier, N. (2022). Two Results on Separation Logic With Theory Reasoning. In ASL 22 (Workshop on Advancing Separation Logic), July 2022.

Daniel Mery and Didier Galmiche (2022). Labelled Tableaux for Linear Time Bunched Implication Logic. In ASL 22 (Workshop on Advancing Separation Logic), July 2022.

Wanyun Sun, Zhilin Wu and Mihaela Sighireanu (2022). Deciding Separation Logic with Heap Lists. In ASL 22 (Workshop on Advancing Separation Logic), July 2022.

Radu Iosif and Florian Zuleger (2022). On the Expressiveness of a Logic of Separated Relations. In ASL 22 (Workshop on Advancing Separation Logic), July 2022.

Contact

N. Peltier (scientific leader of the project).