"Dynamite: A tool for the verification of alloy models based on PVS" (2014) Moscato, M.M.; Lopez Pombo, C.G.; Frias, M.F. ACM Transactions on Software Engineering and Methodology. 23(2)

"TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds" (2013) Galeotti, J.P.; Rosner, N.; Lopez Pombo, C.G.; Frias, M.F. IEEE Transactions on Software Engineering. 39(9):1283-1306

"Ranger: Parallel analysis of alloy models by range partitioning" (2013) Rosner, N.;Siddiqui, J.H.;Aguirre, N. (...)IEEE Computer Society; Association for Computing Machinery, Special Interest Group on Software Engineering (ACM SIGSOFT); IEEE Technical Council on Software Engineering (TCSE); ACM SIGART; NASA 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013:147-157

"A dataflow analysis to improve SAT-based bounded program verification" (2011) Cuervo Parrino, B.; Galeotti, J.P.; Garbervetsky, D.; Frias, M.F. 9th International Conference on Software Engineering and Formal Methods, SEFM 2011. 7041 LNCS:138-154

"ParAlloy: Towards a framework for efficient parallel analysis of alloy models" (2010) Rosner, N.; Galeotti, J.P.; Lopez Pombo, C.G.; Frias, M.F. 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010. 5977 LNCS:396-397

"Analysis of invariants for efficient bounded verification" (2010) Galeotti, J.P.; Rosner, N.; Pombo, C.G.L.; Frias, M.F. 19th International Symposium on Software Testing and Analysis, ISSTA 2010:25-35