NARCO - Non-Aggregative Resource COmpositions

Abstract Partners Events Deliverables 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.


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.





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.


N. Peltier (scientific leader of the project).