Weak Ordering -A New Definition, ISCA, pp.2-14, 1990. ,
Software Verification for Weak Memory via Program Transformation, ESOP, pp.512-532, 2013. ,
DOI : 10.1007/978-3-642-37036-6_28
URL : http://arxiv.org/abs/1207.7264
Checking and Enforcing Robustness against TSO, ESOP, pp.533-553, 2013. ,
DOI : 10.1007/978-3-642-37036-6_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.670.9758
Full Abstraction for a Shared Variable Parallel Language, LICS, pp.98-109, 1993. ,
Concurrent Library Correctness on the TSO Memory Model, ESOP, pp.87-107, 2012. ,
DOI : 10.1007/978-3-642-28869-2_5
Deny-Guarantee Reasoning, ESOP, pp.363-377, 2009. ,
DOI : 10.1007/978-3-642-00590-9_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.148.980
Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.70-83, 1994. ,
DOI : 10.1145/174675.174673
A concurrent, generational garbage collector for a multithreaded implementation of ML, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.113-123, 1993. ,
DOI : 10.1145/158511.158611
URL : https://hal.archives-ouvertes.fr/hal-01499969
Implementing an On-the-Fly Garbage Collector for Java, ISMM, pp.155-166, 2000. ,
Simplifying Linearizability Proofs with Reduction and Abstraction, TACAS, pp.296-311, 2010. ,
DOI : 10.1007/978-3-642-12002-2_25
A calculus of atomic actions, POPL, pp.2-15, 2009. ,
Local rely-guarantee reasoning, POPL, pp.315-327, 2009. ,
DOI : 10.1145/1480881.1480922
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.173.3677
Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.3-463, 1990. ,
DOI : 10.1145/78969.78972
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.5315
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
DOI : 10.1145/363235.363259
Oracle Semantics for Concurrent Separation Logic, ESOP, pp.353-367, 2008. ,
DOI : 10.1007/978-3-540-78739-6_27
Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems, vol.5, issue.4, pp.4-596, 1983. ,
DOI : 10.1145/69575.69577
A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009. ,
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768
The CompCert Memory Model, Version 2, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00703441
A rely-guarantee-based simulation for verifying concurrent program transformations, POPL, pp.455-468, 2012. ,
A rely-guarantee-based simulation for verifying concurrent program transformations, 2012. ,
Verifying a Compiler for Java Threads, ESOP, pp.427-447, 2010. ,
DOI : 10.1007/978-3-642-11957-6_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.496.8823
A certified framework for compiling and executing garbage-collected languages, ICFP, pp.273-284, 2010. ,
A Rely-Guarantee Proof System for x86-TSO, VSTTE, pp.55-70, 2010. ,
DOI : 10.1007/978-3-642-15057-9_4
Understanding POWER multiprocessors, PLDI, pp.175-186, 2011. ,
DOI : 10.1145/2345156.1993520
URL : https://hal.archives-ouvertes.fr/hal-01100824
Relaxed-memory concurrency and verified compilation, POPL, pp.43-54, 2011. ,
CompCertTSO, Journal of the ACM, vol.60, issue.3, p.22, 2013. ,
DOI : 10.1145/2487241.2487248
The SPARC Architecture Manual (version 9), 1994. ,
Systems Programming: Coping with Parallelism -RJ 5118, 1986. ,
A separation logic for refining concurrent objects, POPL, pp.247-258, 2011. ,
A Marriage of Rely/Guarantee and Separation Logic, In CONCUR, pp.256-271, 2007. ,
DOI : 10.1007/978-3-540-74407-8_18