Verifying CUDA programs using SMT-based context-bounded model checking. - Phillipe A. Pereira; Higo F. Albuquerque; Hendrio Marques; Isabela da Silva; Celso B. Carvalho; Lucas C. Cordeiro; Vanessa Santos 001; Ricardo Ferreira (SAC, 2016)

OptCE: A Counterexample-Guided Inductive Optimization Solver. - Higo F. Albuquerque; Rodrigo F. Araujo 001; Iury Valente de Bessa; Lucas C. Cordeiro; Eddie Batista de Lima Filho (SBMF, 2017)

SMT-based context-bounded model checking for CUDA programs. - Phillipe A. Pereira; Higo F. Albuquerque; Isabela da Silva; Hendrio Marques; Felipe R. Monteiro; Ricardo Ferreira; Lucas C. Cordeiro (Concurr. Comput. Pract. Exp., 2017)

Counterexample Guided Inductive Optimization. - Rodrigo F. Araujo 001; Higo F. Albuquerque; Iury Valente de Bessa; Lucas C. Cordeiro; João Edgar Chaves Filho (CoRR, 2017)

Counterexample guided inductive optimization based on satisfiability modulo theories. - Rodrigo F. Araujo 001; Higo F. Albuquerque; Iury Valente de Bessa; Lucas C. Cordeiro; João Edgar Chaves Filho (Sci. Comput. Program., 2018)