Stateless model checking for POWER, CAV, pp.134-156, 2016. ,
The best of both worlds: Trading efficiency and optimality in fence insertion for TSO, ESOP, pp.308-332, 2015. ,
Soundness of data flow analyses for weak memory models, Programming Languages and Systems, pp.272-288, 2011. ,
Racerd: Compositional static race detection, Proceedings of the ACM on Programming Languages, vol.1, issue.1, 2018. ,
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.238-252, 1977. ,
Numeric domains with summarized dimensions, TACAS, pp.512-529, 2004. ,
Thread-modular shape analysis, In ACM SIGPLAN Notices, vol.42, pp.266-277, 2007. ,
Effect summaries for thread-modular analysis, SAS, pp.169-191, 2017. ,
The BDDApron logico-numerical abstract domains library, 2009. ,
Flow-sensitive composition of thread-modular abstract interpretation, Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp.799-809, 2016. ,
Thread-modular static analysis for relaxed memory models, Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pp.337-348, 2017. ,
How to make a multiprocessor computer that correctly executes multiprocess programs. Computers, IEEE Transactions on, vol.100, issue.9, pp.690-691, 1979. ,
Iterated process analysis over lattice-valued regular expressions, PPDP, pp.132-145, 2016. ,
Static analysis of run-time errors in embedded critical parallel C programs, ESOP, vol.11, pp.398-418, 2011. ,
Relational thread-modular static value analysis by abstract interpretation, VMCAI, pp.39-58, 2014. ,
Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions, VMCAI, pp.386-404, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01490178
Thread-local semantics and its efficient sequential abstractions for racefree programs, SAS, pp.253-276, 2017. ,
A rely-guarantee proof system for x86-TSO, International Conference on Verified Software: Theories, Tools, and Experiments, pp.55-70, 2010. ,
Francesco Zappa Nardelli, and Magnus O Myreen. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010. ,
From array domains to abstract interpretation under store-buffer-based memory models, SAS, pp.469-488, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01360566