Specification and Verification of a Transient Stack (Artifact)

Alexandre Moine (1) , Arthur Charguéraud (2) , François Pottier (1)

1 CAMBIUM - Langages de programmation : systèmes de types, concurrence, preuve de programme
2 CAMUS - Compilation pour les Architectures MUlti-coeurS

This repository contains the formalization of a transient stack and its iterator, as described in the CPP'22 paper "Specification and Verification of a Transient Stack".

Domaines: Informatique [cs]

Alexandre Moine, Arthur Charguéraud, François Pottier. Specification and Verification of a Transient Stack (Artifact). 2021, ⟨swh:1:dir:80952d7602e8e9614979f1b1f50fdad8a4c369f1;origin=https://hal.archives-ouvertes.fr/hal-03473197;visit=swh:1:snp:781fc4f58efbdfa6ea16006272793bf7c610d760;anchor=swh:1:rel:3df60f40567bfdf2b365cac2fe61c6bb38d94503;path=/⟩. ⟨hal-03473197⟩