A Formal Verification Tool for UML Behavioral Diagrams. - Luciana Brasil Rebelo dos Santos; Eduardo Rohde Eras; Valdivino Alexandre de Santiago Jr.; Nandamudi Lankalapalli Vijaykumar (ICCSA (1), 2014)

Towards a Wide Acceptance of Formal Methods to the Design of Safety Critical Software: an Approach Based on UML and Model Checking. - Eduardo Rohde Eras; Luciana Brasil Rebelo dos Santos; Valdivino Alexandre de Santiago Júnior; Nandamudi Lankalapalli Vijaykumar (ICCSA (4), 2015)

On the Feasibility of Probabilistic Model Checking to Analyze Battery Sustained Power Supply Systems. - Marina Dioto; Eduardo Rohde Eras; Valdivino Alexandre de Santiago Júnior (ICCSA (2), 2019)

Singularity: A methodology for automatic unit test data generation for C++ applications based on Model Checking counterexamples. - Eduardo Rohde Eras; Valdivino Alexandre de Santiago Júnior; Luciana Brasil Rebelo dos Santos (SAST, 2019)