Formal Verification of UML Sequence Diagrams in the Embedded Systems Context. - Elisabete Cunha; Marcelo Custódio; Herbert Rocha; Raimundo S. Barreto (SBESC, 2011)

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. - Herbert Rocha; Raimundo S. Barreto; Lucas C. Cordeiro; Arilo Dias Neto (IFM, 2012)

Model Checking Embedded C Software Using k-Induction and Invariants. - Herbert Rocha; Hussama Ismail; Lucas C. Cordeiro; Raimundo S. Barreto (SBESC, 2015)

Memory Management Test-Case Generation of C Programs Using Bounded Model Checking. - Herbert Rocha; Raimundo S. Barreto; Lucas C. Cordeiro (SEFM, 2015)

Model Checking C Programs with Loops via k-Induction and Invariants. - Herbert Rocha; Hussama Ismail; Lucas C. Cordeiro; Raimundo S. Barreto (CoRR, 2015)

Model Checking Embedded C Software using k-Induction and Invariants (extended version). - Herbert Rocha; Hussama Ismail; Lucas C. Cordeiro; Raimundo S. Barreto (CoRR, 2015)

Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking. - Herbert O. Rocha (2015)

JFORTES: Java Formal Unit TESt Generation. - Larissa Bentes; Herbert Rocha; Eduardo Valentin; Raimundo S. Barreto (SBESC, 2016)

Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution). - Herbert O. Rocha; Raimundo S. Barreto; Lucas C. Cordeiro (TACAS, 2016)

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution). - Williame Rocha; Herbert Rocha; Hussama Ismail; Lucas C. Cordeiro; Bernd Fischer 002 (TACAS (2), 2017)

Map2Check Using LLVM and KLEE - (Competition Contribution). - Rafael Menezes; Herbert Rocha; Lucas C. Cordeiro; Raimundo S. Barreto (TACAS (2), 2018)

Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution). - Herbert Rocha; Rafael Menezes; Lucas C. Cordeiro; Raimundo S. Barreto (TACAS (2), 2020)

Verifying Security Vulnerabilities in Large Software Systems using Multi-Core k-Induction. - Thales Silva; Carmina Porto; Erickson H. da S. Alves; Lucas C. Cordeiro; Herbert Rocha (CoRR, 2021)

Verification and refutation of C programs based on k-induction and invariant inference. - Omar M. Alhawi; Herbert Rocha; Mikhail R. Gadelha; Lucas C. Cordeiro; Eddie Batista de Lima Filho (Int. J. Softw. Tools Technol. Transf., 2021)