Logique de séparation
La logique de séparation est une extension de la logique de Hoare, une manière de raisonner sur les programmes.
Il a été développé par John C. Reynolds, Peter O'Hearn, Samin Ishtiaq et Hongseok Yang, s'inspirant des premiers travaux de Rod Burstall. Le langage d'assertion de la logique de séparation est un cas particulier de la logique des implications groupées (BI). Un article de synthèse du MCAC par O'Hearn décrit l'évolution du sujet jusqu'à début 2019
