Automatic Refinement of Split Binary Semaphore. - Damián Barsotti; Javier O. Blanco (ICTAC, 2007)

Local reasoning for abstraction and sharing. - Renato Cherini; Javier O. Blanco (SAC, 2009)

A Shape Analysis for Non-linear Data Structures. - Renato Cherini; Lucas Rearte; Javier O. Blanco (SAS, 2010)