Semantic foundations for typed assembly languages, TOPLAS, vol.32, pp.1-67, 2010. ,
Mathematizing C++ Concurrency, POPL, pp.55-66, 2011. ,
Outlawing ghosts: Avoiding out-of-thin-air results, MSPC, 2014. ,
Permission accounting in separation logic, pp.259-270, 2005. ,
Checking interference with fractional permissions, SAS (LNCS), 2003. ,
Dynamic circular work-stealing deque, SPAA. 21-28, 2005. ,
Appendix and Coq development accompanying this paper, 2019. ,
Verifying C11 Programs Operationally, PPoPP, pp.355-365, 2019. ,
A Program Logic for C11 Memory Fences, VMCAI (LNCS), pp.413-430, 2016. ,
Tackling Real-Life Relaxed Concurrency with FSL++, ESOP, 2017. ,
Local Reasoning for Storable Locks and Threads, RustBelt project webpage, pp.19-37, 2007. ,
GPS+: Reasoning About Fences and Relaxed Atomics, International Journal of Parallel Programming, vol.46, pp.1157-1183, 2018. ,
Oracle Semantics for Concurrent Separation Logic, ESOP, pp.353-367, 2008. ,
Insufficient synchronization in Arc::get_mut, 2018. ,
RustBelt: Securing the Foundations of the Rust Programming Language, Article, vol.2, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01633165
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic, Journal of Functional Programming, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01945446
Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris, ECOOP (LIPIcs), vol.17, p.29, 2017. ,
Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxedmemory Concurrency, POPL. ACM, pp.175-189 ,
Interactive Proofs in Higher-Order Concurrent Separation Logic, Amin Timany, and Lars Birkedal, 2017. ,
Repairing sequential consistency in C/C++11, PLDI, 2017. ,
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Trans. Computers, vol.28, pp.690-691, 1979. ,
Operational Aspects of C/C++ Concurrency, 2016. ,
Separation logic: A logic for shared mutable data structures, LICS, 2002. ,
A Separation Logic for a Promising Semantics, ESOP, pp.357-384, 2018. ,
Verifying read-copy-update in a logic for weak memory, 2015. ,
Crossbeam: Support for concurrent and parallel programming, 2016. ,
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation, OOPSLA. ACM, pp.691-707, 2014. ,
Relaxed Separation Logic: A Program Logic for C11 Concurrency, OOPSLA, 2013. ,