Author of the publication

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.

, , , and . SAC, page 1881-1890. ACM, (2018)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

No persons found for author name Demange, Delphine
add a person with the name Demange, Delphine
 

Other publications of authors with the same name

Verifying Fast and Sparse SSA-Based Optimizations in Coq., , and . CC, volume 9031 of Lecture Notes in Computer Science, page 233-252. Springer, (2015)Formal Verification of an SSA-Based Middle-End for CompCert., , and . ACM Trans. Program. Lang. Syst., 36 (1): 4:1-4:35 (2014)Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology., , , , , , and . J. Autom. Reasoning, 63 (2): 489-515 (2019)A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert., , and . ESOP, volume 7211 of Lecture Notes in Computer Science, page 47-66. Springer, (2012)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology., , , , , , and . ITP, volume 10499 of Lecture Notes in Computer Science, page 496-513. Springer, (2017)A verified information-flow architecture., , , , , , , , and . POPL, page 165-178. ACM, (2014)A verified information-flow architecture., , , , , , , , and . Journal of Computer Security, 24 (6): 689-734 (2016)A Provably Correct Stackless Intermediate Representation for Java Bytecode., , and . APLAS, volume 6461 of Lecture Notes in Computer Science, page 97-113. Springer, (2010)Mechanizing conventional SSA for a verified destruction with coalescing., and . CC, page 77-87. ACM, (2016)Plan B: a buffered memory model for Java., , , , , and . POPL, page 329-342. ACM, (2013)