,
The benefits of duality in verifying concurrent programs under TSO, 2016. ,
Memorax, a precise and sound tool for automatic fence insertion under TSO, 2013. ,
Regular model checking without transducers, 2007. ,
Parameterized verification of infinite-state processes with global conditions, 2007. ,
The semantics of power and arm multiprocessor machine code, 2008. ,
Software verification for weak memory via program transformation, 2013. ,
Herding cats: Modelling, simulation, testing, and data mining for weak memory, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01081413
Limits for automatic verification of finite-state concurrent systems, Inf. Process. Lett, 1986. ,
Lazy tso reachability, 2015. ,
Checking and enforcing robustness against tso, 2013. ,
Reasoning about networks with many identical finite-state processes, 1986. ,
Cubicle: A parallel smtbased model checker for parameterized systems: Tool paper, 2012. ,
Invariants for Finite Instances and Beyond, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00924640
Certificates for parameterized model checking, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01761274
Reasoning about systems with many processes, J, 1992. ,
MCMT: A model checker modulo theories, 2010. ,
The arbiter: an active system component for implementing synchronizing primitives, Fundam. Inform, 1981. ,
, The Art of Multiprocessor Programming, 2008.
How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput, 1979. ,
, A better x86 memory model: X86-TSO, 2009.
X86-TSO: A rigorous and usable programmer's model for x86 multiprocessors, 2010. ,