Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking. - Iury Valente de Bessa; Hussama Ibrahim Ismail; Lucas Carvalho Cordeiro; Joao Edgar Chaves Filho (SBESC, 2014)

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

Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems. - Alessandro Trindade; Hussama Ismail; Lucas C. Cordeiro (SBESC, 2015)

DSVerifier: A Bounded Model Checking Tool for Digital Systems. - Hussama Ismail; Iury Bessa; Lucas C. Cordeiro; Eddie Batista de Lima Filho; Joao Edgar Chaves Filho (SPIN, 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)

Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version). - Alessandro Trindade; Hussama Ismail; Lucas C. Cordeiro (CoRR, 2015)

Verification of fixed-point digital controllers using direct and delta forms realizations. - Iury Valente de Bessa; Hussama Ismail; Lucas C. Cordeiro; João Edgar Chaves Filho (Des. Autom. Embed. Syst., 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)

Multi-core model checking and maximum satisfiability applied to hardware-software partitioning. - Alessandro Bezerra Trindade; Renato De Faria Degelo; Edilson Galvão Dos Santos Junior; Hussama Ibrahim Ismail; Helder Cruz Da Silva; Lucas Carvalho Cordeiro (Int. J. Embed. Syst., 2017)

Handling loops in bounded model checking of C programs via k-induction. - Mikhail Y. R. Gadelha; Hussama Ibrahim Ismail; Lucas C. Cordeiro (Int. J. Softw. Tools Technol. Transf., 2017)

Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty. - Iury Bessa; Hussama Ismail; Reinaldo M. Palhares; Lucas C. Cordeiro; Joao Edgar Chaves Filho (IEEE Trans. Computers, 2017)

ESBMC-GPU A context-bounded model checking tool to verify CUDA programs. - Felipe R. Monteiro; Erickson H. da S. Alves; Isabela da Silva; Hussama Ismail; Lucas C. Cordeiro; Eddie Batista de Lima Filho (Sci. Comput. Program., 2018)

DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles. - Lennon C. Chaves; Iury Bessa; Hussama Ismail; Adriano Bruno dos Santos Frutuoso; Lucas C. Cordeiro; Eddie Batista de Lima Filho (IEEE Trans. Reliab., 2018)

Verifying fragility in digital systems with uncertainties using DSVerifier v2.0. - Lennon C. Chaves; Hussama Ibrahim Ismail; Iury Valente de Bessa; Lucas C. Cordeiro; Eddie Batista de Lima Filho (J. Syst. Softw., 2019)