publications | Lucas C. Cordeiro

2026

Adversarial Example Detection and Mitigation Using Machine Learning

E Nowroozi, R Taheri, and Cordeiro L. C. (Eds.)

2026

DOI Bib

@book{cordeiro2026adversarial,
  title = {Adversarial Example Detection and Mitigation Using Machine Learning},
  author = {Nowroozi, E and Taheri, R and (Eds.), Cordeiro L. C.},
  booktitle = {Springer Nature, 2026. ISBN 978-3-031-99446-3.},
  year = {2026},
  doi = {10.1007/978-3-031-99447-0},
}

LLM-Assisted Translation and Bounded Model Checking of Python Code

S Shivaji, K Havelund, N Lobakhina, and 2 more authors

In International Symposium on AI Verification (AISoLA), 2026

Bib PDF Slides

@inproceedings{cordeiro2026assisted,
  title = {LLM-Assisted Translation and Bounded Model Checking of Python Code},
  author = {Shivaji, S and Havelund, K and Lobakhina, N and Cordeiro, L. C and Pinto, A},
  booktitle = {International Symposium on AI Verification (AISoLA)},
  year = {2026},
}

ICCE

Memory Safety in Linux Device Drivers: Enhancing Security with Formal Verification

Janislley O. Sousa, David A. O. Ferreira, Eddie B. Lima Filho, and 1 more author

In IEEE International Conference on Consumer Electronics, ICCE 2026, Dubai, United Arab Emirates, February 3-5, 2026, 2026

DOI Bib PDF

@inproceedings{sousa2026memory,
  title = {Memory Safety in Linux Device Drivers: Enhancing Security with Formal Verification},
  author = {Sousa, Janislley O. and Ferreira, David A. O. and de Lima Filho, Eddie B. and Cordeiro, Lucas C.},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2026, Dubai, United Arab Emirates, February 3-5, 2026},
  pages = {1--6},
  year = {2026},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE67443.2026.11449875},
  url = {https://doi.org/10.1109/ICCE67443.2026.11449875}
}

2025

Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

Norbert Tihanyi, Tamás Bisztray, Mohamed Amine Ferrag, and 4 more authors

CoRR, 2025

DOI Bib

@article{tihanyi2026vulnerability,
  title = {Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview},
  author = {Tihanyi, Norbert and Bisztray, Tam{\'{a}}s and Ferrag, Mohamed Amine and Cherif, Bilel and Dubniczky, Richard A. and Jain, Ridhi and Cordeiro, Lucas C.},
  journal = {CoRR},
  volume = {abs/2503.10784},
  year = {2025},
  doi = {10.1007/978-3-031-99447-0_3},
  eprinttype = {arXiv},
  url = {https://doi.org/10.48550/arXiv.2503.10784}
}

AST

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

Norbert Tihanyi, Yiannis Charalambous, Ridhi Jain, and 2 more authors

In IEEE/ACM International Conference on Automation of Software Test, AST@ICSE 2025, Ottawa, ON, Canada, April 28-29, 2025, 2025

DOI Bib PDF Slides

@inproceedings{tihanyi2025software,
  title = {A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification},
  author = {Tihanyi, Norbert and Charalambous, Yiannis and Jain, Ridhi and Ferrag, Mohamed Amine and Cordeiro, Lucas C.},
  booktitle = {{IEEE/ACM} International Conference on Automation of Software Test, AST@ICSE 2025, Ottawa, ON, Canada, April 28-29, 2025},
  pages = {136--147},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/AST66626.2025.00020},
  editor = {Zaidman, Andy and Lonetti, Francesca and Schieferdecker, Ina and Subramanyan, Rajesh},
  url = {https://doi.org/10.1109/AST66626.2025.00020}
}

A review of state-of-the-art techniques for large language model compression

Pierre V. Dantas, Lucas C. Cordeiro, and Waldir S. S. Júnior

Complex Intell. Syst., 2025

DOI Bib

@article{dantas2025review,
  title = {A review of state-of-the-art techniques for large language model compression},
  author = {Dantas, Pierre V. and Cordeiro, Lucas C. and J{\'{u}}nior, Waldir S. S.},
  journal = {Complex Intell. Syst.},
  volume = {11},
  number = {9},
  year = {2025},
  doi = {10.1007/s40747-025-02019-z},
  url = {https://doi.org/10.1007/s40747-025-02019-z}
}

ICCE

Automated Evaluation of Digital TV Middleware: Using Fuzzing and Pairwise for Test Generation

Sergillam Barroso Oliveira, Eddie Batista Lima Filho, Orlewilson B. Maia, and 1 more author

In IEEE International Conference on Consumer Electronics, ICCE 2025, Las Vegas, NV, USA, January 11-14, 2025, 2025

DOI Bib PDF

@inproceedings{oliveira2025automated,
  title = {Automated Evaluation of Digital TV Middleware: Using Fuzzing and Pairwise for Test Generation},
  author = {Oliveira, Sergillam Barroso and de Lima Filho, Eddie Batista and Maia, Orlewilson B. and Cordeiro, Lucas C.},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2025, Las Vegas, NV, USA, January 11-14, 2025},
  pages = {1--5},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE63647.2025.10930091},
  url = {https://doi.org/10.1109/ICCE63647.2025.10930091}
}

CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs Towards CWE Detection

Richard A. Dubniczky, Krisztofer Zoltán Horvát, Tamás Bisztray, and 3 more authors

In Theoretical Aspects of Software Engineering - 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14-16, 2025, Proceedings, 2025

DOI Bib PDF Slides

@inproceedings{dubniczky2025castle,
  title = {CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs Towards CWE Detection},
  author = {Dubniczky, Richard A. and Horv{\'{a}}t, Krisztofer Zolt{\'{a}}n and Bisztray, Tam{\'{a}}s and Ferrag, Mohamed Amine and Cordeiro, Lucas C. and Tihanyi, Norbert},
  booktitle = {Theoretical Aspects of Software Engineering - 19th International Symposium, {TASE} 2025, Limassol, Cyprus, July 14-16, 2025, Proceedings},
  volume = {15841},
  pages = {253--272},
  year = {2025},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-98208-8_15},
  editor = {R{\"{u}}mmer, Philipp and Wu, Zhilin},
  url = {https://doi.org/10.1007/978-3-031-98208-8\_15}
}

ESBMC v7.6: Enhanced model checking of C++ programs with clang AST

Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, and 4 more authors

Sci. Comput. Program., 2025

DOI Bib

@article{li2025esbmc,
  title = {ESBMC v7.6: Enhanced model checking of C++ programs with clang AST},
  author = {Li, Xianzhiyu and Song, Kunjian and Gadelha, Mikhail R. and Brau{\ss}e, Franz and Menezes, Rafael S. and Korovin, Konstantin and Cordeiro, Lucas C.},
  journal = {Sci. Comput. Program.},
  volume = {246},
  pages = {103336},
  year = {2025},
  doi = {10.1016/j.scico.2025.103336},
  url = {https://doi.org/10.1016/j.scico.2025.103336}
}

FASE

ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving - (Competition Contribution)

Chenfeng Wei, Tong Wu, Rafael Sá Menezes, and 6 more authors

In Fundamental Approaches to Software Engineering - 28th International Conference, FASE 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, 2025

DOI Bib PDF Video Slides

@inproceedings{wei2025esbmc,
  title = {ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving - (Competition Contribution)},
  author = {Wei, Chenfeng and Wu, Tong and Menezes, Rafael S{\'{a}} and Shmarov, Fedor and Aljaafari, Fatimah and Godboley, Sangharatna and Alshmrany, Kaled M. and de Freitas, Rosiane and Cordeiro, Lucas C.},
  booktitle = {Fundamental Approaches to Software Engineering - 28th International Conference, {FASE} 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, {ETAPS} 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings},
  volume = {15693},
  pages = {281--286},
  year = {2025},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-90900-9_15},
  editor = {Boronat, Artur and Fraser, Gordon},
  url = {https://doi.org/10.1007/978-3-031-90900-9\_15}
}

TACAS

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction - (Competition Contribution)

Tong Wu, Xianzhiyu Li, Edoardo Manino, and 6 more authors

In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part III, 2025

DOI Bib PDF Slides

@inproceedings{wu2025esbmc,
  title = {ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction - (Competition Contribution)},
  author = {Wu, Tong and Li, Xianzhiyu and Manino, Edoardo and Menezes, Rafael S{\'{a}} and Gadelha, Mikhail R. and Xiong, Shale and Tihanyi, Norbert and Petoumenos, Pavlos and Cordeiro, Lucas C.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, {TACAS} 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, {ETAPS} 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part {III}},
  volume = {15698},
  pages = {223--228},
  year = {2025},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-90660-2_16},
  editor = {Gurfinkel, Arie and Heule, Marijn},
  url = {https://doi.org/10.1007/978-3-031-90660-2\_16}
}

ICCE

Enhanced User Experience in Digital TV: Recommending Content in Free-to-Air TV Contexts

Sergillam Barroso Oliveira, Tiago Souza, Petrina Kimura, and 7 more authors

In IEEE International Conference on Consumer Electronics, ICCE 2025, Las Vegas, NV, USA, January 11-14, 2025, 2025

DOI Bib PDF

@inproceedings{oliveira2025enhanced,
  title = {Enhanced User Experience in Digital TV: Recommending Content in Free-to-Air TV Contexts},
  author = {Oliveira, Sergillam Barroso and Souza, Tiago and Kimura, Petrina and Machado, Hayd{\{e}} and Maia, Orlewilson Bentes and de Lima Filho, Eddie B. and do Nascimento, Edson Weslley Almeida and Negreiros, Leandro and Santana, Rafaell Guimar{\~{a}}es and Cordeiro, Lucas C.},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2025, Las Vegas, NV, USA, January 11-14, 2025},
  pages = {1--6},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE63647.2025.10930178},
  url = {https://doi.org/10.1109/ICCE63647.2025.10930178}
}

How secure is AI-generated code: a large-scale comparison of large language models

Norbert Tihanyi, Tamás Bisztray, Mohamed Amine Ferrag, and 2 more authors

Empir. Softw. Eng., 2025

DOI Bib

@article{tihanyi2025secure,
  title = {How secure is AI-generated code: a large-scale comparison of large language models},
  author = {Tihanyi, Norbert and Bisztray, Tam{\'{a}}s and Ferrag, Mohamed Amine and Jain, Ridhi and Cordeiro, Lucas C.},
  journal = {Empir. Softw. Eng.},
  volume = {30},
  number = {2},
  pages = {47},
  year = {2025},
  doi = {10.1007/s10664-024-10590-1},
  url = {https://doi.org/10.1007/s10664-024-10590-1}
}

Mitigating Insider Threats: Insights from Software Security Experts for Process Improvement and Risk Reduction

Azzah AlGhamdi, Mahmood Niazi, Lucas Carvalho Cordeiro, and 2 more authors

In Proceedings of the 2025 29th International Conference on Evaluation and Assessment in Software Engineering Companion, EASE Companion 2025, Istanbul, Turkey, June 17-20, 2025, 2025

DOI Bib

@inproceedings{alghamdi2025mitigating,
  title = {Mitigating Insider Threats: Insights from Software Security Experts for Process Improvement and Risk Reduction},
  author = {AlGhamdi, Azzah and Niazi, Mahmood and Cordeiro, Lucas Carvalho and Humayun, Mamoona and Stewart, Andrew},
  booktitle = {Proceedings of the 2025 29th International Conference on Evaluation and Assessment in Software Engineering Companion, {EASE} Companion 2025, Istanbul, Turkey, June 17-20, 2025},
  pages = {41--48},
  year = {2025},
  publisher = {{ACM}},
  doi = {10.1145/3727967.3756845},
  editor = {Babar, Muhammad Ali and Tosun, Ayse and Wagner, Stefan and Stray, Viktoria},
  url = {https://doi.org/10.1145/3727967.3756845}
}

Montague semantics and modifier consistency measurement in neural language models

Danilo Silva Carvalho, Edoardo Manino, Julia Rozanova, and 2 more authors

In Proceedings of the 31st International Conference on Computational Linguistics, COLING 2025, Abu Dhabi, UAE, January 19-24, 2025, 2025

Bib

@inproceedings{carvalho2025montague,
  title = {Montague semantics and modifier consistency measurement in neural language models},
  author = {de Carvalho, Danilo Silva and Manino, Edoardo and Rozanova, Julia and Cordeiro, Lucas C. and Freitas, Andr{\'{e}}},
  booktitle = {Proceedings of the 31st International Conference on Computational Linguistics, {COLING} 2025, Abu Dhabi, UAE, January 19-24, 2025},
  pages = {5515--5529},
  year = {2025},
  publisher = {Association for Computational Linguistics},
  editor = {Rambow, Owen and Wanner, Leo and Apidianaki, Marianna and Al{-}Khalifa, Hend and Eugenio, Barbara Di and Schockaert, Steven},
  url = {https://aclanthology.org/2025.coling-main.370/}
}

ICCE

Natural Language Processing Models for Named Entity Recognition in Digital TV Audio

Edson Weslley Almeida Nascimento, Petrina Kimura, Tiago Souza, and 5 more authors

In IEEE International Conference on Consumer Electronics, ICCE 2025, Las Vegas, NV, USA, January 11-14, 2025, 2025

DOI Bib

@inproceedings{nascimento2025natural,
  title = {Natural Language Processing Models for Named Entity Recognition in Digital TV Audio},
  author = {do Nascimento, Edson Weslley Almeida and Kimura, Petrina and Souza, Tiago and Oliveira, Sergillam Barroso and Machado, Hayd{\{e}} and Cordeiro, Lucas C. and Fabr{\'{\i}}cio, R{\{o}}mulo and de Lima Filho, Eddie B.},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2025, Las Vegas, NV, USA, January 11-14, 2025},
  pages = {1--6},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE63647.2025.10929817},
  url = {https://doi.org/10.1109/ICCE63647.2025.10929817}
}

ESOP

Neural Network Verification is a Programming Language Challenge

Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, and 8 more authors

In Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, 2025

DOI Bib Slides

@inproceedings{cordeiro2025neural,
  title = {Neural Network Verification is a Programming Language Challenge},
  author = {Cordeiro, Lucas C. and Daggitt, Matthew L. and Girard{-}Satabin, Julien and Isac, Omri and Johnson, Taylor T. and Katz, Guy and Komendantskaya, Ekaterina and Lemesle, Augustin and Manino, Edoardo and Sinkarovs, Artjoms and Wu, Haoze},
  booktitle = {Programming Languages and Systems - 34th European Symposium on Programming, {ESOP} 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, {ETAPS} 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part {I}},
  volume = {15694},
  pages = {206--235},
  year = {2025},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-91118-7_9},
  editor = {Vafeiadis, Viktor},
  url = {https://doi.org/10.1007/978-3-031-91118-7\_9}
}

ICCE

Optimizing User Experience: A Feedback-Based Performance Evaluation Methodology for Recommendation Systems

Sergillam Barroso Oliveira, Tiago Souza, Petrina Kimura, and 5 more authors

In IEEE International Conference on Consumer Electronics, ICCE 2025, Las Vegas, NV, USA, January 11-14, 2025, 2025

DOI Bib

@inproceedings{oliveira2025optimizing,
  title = {Optimizing User Experience: A Feedback-Based Performance Evaluation Methodology for Recommendation Systems},
  author = {Oliveira, Sergillam Barroso and Souza, Tiago and Kimura, Petrina and Machado, Hayd{\{e}} and Maia, Orlewilson Bentes and de Lima Filho, Eddie B. and do Nascimento, Edson Weslley Almeida and Cordeiro, Lucas C.},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2025, Las Vegas, NV, USA, January 11-14, 2025},
  pages = {1--6},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE63647.2025.10930168},
  url = {https://doi.org/10.1109/ICCE63647.2025.10930168}
}

ReqInOne: A Large Language Model-Based Agent for Software Requirements Specification Generation

Taohong Zhu, Lucas C. Cordeiro, and Youcheng Sun

In 33rd IEEE International Requirements Engineering Conference, RE 2025, Valencia, Spain, September 1-5, 2025, 2025

DOI Bib PDF

@inproceedings{zhu2025reqinone,
  title = {ReqInOne: A Large Language Model-Based Agent for Software Requirements Specification Generation},
  author = {Zhu, Taohong and Cordeiro, Lucas C. and Sun, Youcheng},
  booktitle = {33rd {IEEE} International Requirements Engineering Conference, {RE} 2025, Valencia, Spain, September 1-5, 2025},
  pages = {449--457},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/RE63999.2025.00054},
  url = {https://doi.org/10.1109/RE63999.2025.00054}
}

SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection With LLMs?

Mohamed Amine Ferrag, Ammar Ayman Battah, Norbert Tihanyi, and 8 more authors

IEEE Trans. Software Eng., 2025

DOI Bib

@article{ferrag2025securefalcon,
  title = {SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection With LLMs?},
  author = {Ferrag, Mohamed Amine and Battah, Ammar Ayman and Tihanyi, Norbert and Jain, Ridhi and Maimut, Diana and Alwahedi, Fatima and Lestable, Thierry and Thandi, Narinderjit Singh and Mechri, Abdechakour and Debbah, M{\'{e}}rouane and Cordeiro, Lucas C.},
  journal = {{IEEE} Trans. Software Eng.},
  volume = {51},
  number = {4},
  pages = {1248--1265},
  year = {2025},
  doi = {10.1109/TSE.2025.3548168},
  url = {https://doi.org/10.1109/TSE.2025.3548168}
}

Supporting Software Formal Verification with Large Language Models: An Experimental Study

Weiqi Wang, Marie Farrell, Lucas C. Cordeiro, and 1 more author

In 33rd IEEE International Requirements Engineering Conference, RE 2025, Valencia, Spain, September 1-5, 2025, 2025

DOI Bib HTML Slides

@inproceedings{wang2025supporting,
  title = {Supporting Software Formal Verification with Large Language Models: An Experimental Study},
  author = {Wang, Weiqi and Farrell, Marie and Cordeiro, Lucas C. and Zhao, Liping},
  booktitle = {33rd {IEEE} International Requirements Engineering Conference, {RE} 2025, Valencia, Spain, September 1-5, 2025},
  pages = {423--431},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/RE63999.2025.00049},
  url = {https://doi.org/10.1109/RE63999.2025.00049}
}

UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification

Yiannis Charalambous, Claudionor N. Coelho Jr., Luı́s C. Lamb, and 1 more author

In Proceedings of the Generative Code Intelligence Workshop (GeCoIn 2025) co-located with 28th European Conference on Artificial Intelligence (ECAI 2025), Bologna, Italy, October 26, 2025, 2025

Bib HTML

@inproceedings{charalambous2025unittenx,
  title = {UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification},
  author = {Charalambous, Yiannis and Jr., Claudionor N. Coelho and Lamb, Lu{\'{\i}}s C. and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the Generative Code Intelligence Workshop (GeCoIn 2025) co-located with 28th European Conference on Artificial Intelligence {(ECAI} 2025), Bologna, Italy, October 26, 2025},
  volume = {4075},
  year = {2025},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  editor = {Iotti, Eleonora and Dolcetti, Greta and Arceri, Vincenzo and Maffeis, Sergio},
  url = {https://ceur-ws.org/Vol-4075/paper5.pdf}
}

FSE

VO-GCSE: Verification Optimization through Global Common Subexpression Elimination

Rafael Sá Menezes, Norbert Tihanyi, Ridhi Jain, and 3 more authors

In Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, FSE Companion 2025, Clarion Hotel Trondheim, Trondheim, Norway, June 23-28, 2025, 2025

DOI Bib PDF

@inproceedings{menezes2025gcse,
  title = {VO-GCSE: Verification Optimization through Global Common Subexpression Elimination},
  author = {Menezes, Rafael S{\'{a}} and Tihanyi, Norbert and Jain, Ridhi and Levin, Alexander and de Freitas, Rosiane and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 33rd {ACM} International Conference on the Foundations of Software Engineering, {FSE} Companion 2025, Clarion Hotel Trondheim, Trondheim, Norway, June 23-28, 2025},
  pages = {1060--1064},
  year = {2025},
  publisher = {{ACM}},
  doi = {10.1145/3696630.3728581},
  editor = {Montecchi, Leonardo and Li, Jingyue and Poshyvanyk, Denys and Zhang, Dongmei},
  url = {https://doi.org/10.1145/3696630.3728581}
}

ASE

VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods

Chenfeng Wei, Shiyu Cai, Yiannis Charalambous, and 3 more authors

In 40th IEEE/ACM International Conference on Automated Software Engineering, ASE 2025, Seoul, Korea, Republic of, November 16-20, 2025, 2025

DOI Bib PDF Poster Slides

@inproceedings{wei2025veriexploit,
  title = {VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods},
  author = {Wei, Chenfeng and Cai, Shiyu and Charalambous, Yiannis and Wu, Tong and Godboley, Sangharatna and Cordeiro, Lucas C.},
  booktitle = {40th {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2025, Seoul, Korea, Republic of, November 16-20, 2025},
  pages = {1415--1426},
  year = {2025},
  publisher = {{IEEE}},
  doi = {10.1109/ASE63991.2025.00120},
  url = {https://doi.org/10.1109/ASE63991.2025.00120}
}

GPT, But Backwards: Exactly Inverting Language Model Outputs

Adrians Skapars, Edoardo Manino, Youcheng Sun, and 1 more author

CoRR, 2025

DOI Bib HTML

@article{skapars2025gpt,
  title = {GPT, But Backwards: Exactly Inverting Language Model Outputs},
  author = {Skapars, Adrians and Manino, Edoardo and Sun, Youcheng and Cordeiro, Lucas C.},
  journal = {CoRR},
  volume = {abs/2507.01693},
  year = {2025},
  doi = {10.48550/arXiv.2507.01693},
}

2024

A comprehensive review of model compression techniques in machine learning

Pierre V. Dantas, Waldir Sabino Silva Jr., Lucas Carvalho Cordeiro, and 1 more author

Appl. Intell., 2024

DOI Bib

@article{dantas2024comprehensive,
  title = {A comprehensive review of model compression techniques in machine learning},
  author = {Dantas, Pierre V. and da Silva Jr., Waldir Sabino and Cordeiro, Lucas Carvalho and Carvalho, Celso Barbosa},
  journal = {Appl. Intell.},
  volume = {54},
  number = {22},
  pages = {11804--11844},
  year = {2024},
  doi = {10.1007/s10489-024-05747-w},
  url = {https://doi.org/10.1007/s10489-024-05747-w}
}

Counterexample Guided Neural Network Quantization Refinement

João Batista Pereira Matos Jr., Eddie B. Lima Filho, Iury Bessa, and 3 more authors

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024

DOI Bib

@article{jr2024counterexample,
  title = {Counterexample Guided Neural Network Quantization Refinement},
  author = {Jr., Jo{\~{a}}o Batista Pereira Matos and de Lima Filho, Eddie B. and Bessa, Iury and Manino, Edoardo and Song, Xidan and Cordeiro, Lucas C.},
  journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
  volume = {43},
  number = {4},
  pages = {1121--1134},
  year = {2024},
  doi = {10.1109/TCAD.2023.3335313},
  url = {https://doi.org/10.1109/TCAD.2023.3335313}
}

Dynamic Intelligence Assessment: Benchmarking LLMs on the Road to AGI with a Focus on Model Confidence

Norbert Tihanyi, Tamás Bisztray, Richard A. Dubniczky, and 11 more authors

In IEEE International Conference on Big Data, BigData 2024, Washington, DC, USA, December 15-18, 2024, 2024

DOI Bib

@inproceedings{tihanyi2024dynamic,
  title = {Dynamic Intelligence Assessment: Benchmarking LLMs on the Road to AGI with a Focus on Model Confidence},
  author = {Tihanyi, Norbert and Bisztray, Tam{\'{a}}s and Dubniczky, Richard A. and T{\'{o}}th, Rebeka and Borsos, Bertalan and Cherif, Bilel and Jain, Ridhi and Muzsai, Lajos and Ferrag, Mohamed Amine and Marinelli, Ryan and Cordeiro, Lucas C. and Debbah, M{\'{e}}rouane and Mavroeidis, Vasileios and J{\o}sang, Audun},
  booktitle = {{IEEE} International Conference on Big Data, BigData 2024, Washington, DC, USA, December 15-18, 2024},
  pages = {3313--3321},
  year = {2024},
  publisher = {{IEEE}},
  doi = {10.1109/BIGDATA62323.2024.10825051},
  editor = {Ding, Wei and Lu, Chang{-}Tien and Wang, Fusheng and Di, Liping and Wu, Kesheng and Huan, Jun and Nambiar, Raghu and Li, Jundong and Ilievski, Filip and Baeza{-}Yates, Ricardo and Hu, Xiaohua},
  url = {https://doi.org/10.1109/BigData62323.2024.10825051}
}

TACAS

ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)

Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, and 9 more authors

In Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, 2024

DOI Bib PDF Slides

@inproceedings{menezes2024esbmc,
  title = {ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)},
  author = {Menezes, Rafael S{\'{a}} and Aldughaim, Mohannad and Farias, Bruno and Li, Xianzhiyu and Manino, Edoardo and Shmarov, Fedor and Song, Kunjian and Brau{\ss}e, Franz and Gadelha, Mikhail R. and Tihanyi, Norbert and Korovin, Konstantin and Cordeiro, Lucas C.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, {TACAS} 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part {III}},
  volume = {14572},
  pages = {376--380},
  year = {2024},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-57256-2_24},
  editor = {Finkbeiner, Bernd and Kov{\'{a}}cs, Laura},
  url = {https://doi.org/10.1007/978-3-031-57256-2\_24}
}

ISSTA

ESBMC-Python: A Bounded Model Checker for Python Programs

Bruno Farias, Rafael Menezes, Eddie B. Lima Filho, and 2 more authors

In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, Vienna, Austria, September 16-20, 2024, 2024

DOI Bib Slides

@inproceedings{farias2024esbmc,
  title = {ESBMC-Python: A Bounded Model Checker for Python Programs},
  author = {Farias, Bruno and Menezes, Rafael and de Lima Filho, Eddie B. and Sun, Youcheng and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 33rd {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis, {ISSTA} 2024, Vienna, Austria, September 16-20, 2024},
  pages = {1836--1840},
  year = {2024},
  publisher = {{ACM}},
  doi = {10.1145/3650212.3685304},
  editor = {Christakis, Maria and Pradel, Michael},
  url = {https://doi.org/10.1145/3650212.3685304}
}

FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis

Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat, and 1 more author

Formal Aspects Comput., 2024

DOI Bib

@article{alshmrany2024fusebmc,
  title = {FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis},
  author = {Alshmrany, Kaled M. and Aldughaim, Mohannad and Bhayat, Ahmed and Cordeiro, Lucas C.},
  journal = {Formal Aspects Comput.},
  volume = {36},
  number = {2},
  pages = {12},
  year = {2024},
  doi = {10.1145/3665337},
  url = {https://doi.org/10.1145/3665337}
}

ISSTA

JCWIT: A Correctness-Witness Validator for Java Programs Based on Bounded Model Checking

Zaiyu Cheng, Tong Wu, Peter Schrammel, and 3 more authors

In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, Vienna, Austria, September 16-20, 2024, 2024

DOI Bib Slides

@inproceedings{cheng2024jcwit,
  title = {JCWIT: A Correctness-Witness Validator for Java Programs Based on Bounded Model Checking},
  author = {Cheng, Zaiyu and Wu, Tong and Schrammel, Peter and Tihanyi, Norbert and de Lima Filho, Eddie B. and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 33rd {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis, {ISSTA} 2024, Vienna, Austria, September 16-20, 2024},
  pages = {1831--1835},
  year = {2024},
  publisher = {{ACM}},
  doi = {10.1145/3650212.3685303},
  editor = {Christakis, Maria and Pradel, Michael},
  url = {https://doi.org/10.1145/3650212.3685303}
}

ASE

LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling

Muhammad A. A. Pirzada, Giles Reger, Ahmed Bhayat, and 1 more author

In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, 2024

Awarded DOI Bib Slides

ACM SIGSOFT Distinguished Paper Award

@inproceedings{pirzada2024generated,
  title = {LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling},
  author = {Pirzada, Muhammad A. A. and Reger, Giles and Bhayat, Ahmed and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 39th {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2024, Sacramento, CA, USA, October 27 - November 1, 2024},
  pages = {1395--1407},
  year = {2024},
  publisher = {{ACM}},
  doi = {10.1145/3691620.3695512},
  editor = {Filkov, Vladimir and Ray, Baishakhi and Zhou, Minghui},
  url = {https://doi.org/10.1145/3691620.3695512}
}

Privacy-preserving and Accountable Billing in Peer-to-Peer Energy Trading Markets with Homomorphic Encryption and Blockchain

K Erdayandi and L. & Mustafa M. A Cordeiro

To appear at Sustainable Energy, Grids and Networks, 2024

Bib PDF

@article{cordeiro2024privacy,
  title = {Privacy-preserving and Accountable Billing in Peer-to-Peer Energy Trading Markets with Homomorphic Encryption and Blockchain},
  author = {Erdayandi, K and Cordeiro, L.  Mustafa M. A},
  journal = {To appear at Sustainable Energy, Grids and Networks},
  year = {2024},
}

FSE

Rapid Taint Assisted Concolic Execution (TACE)

Ridhi Jain, Norbert Tihanyi, Mthandazo Ndhlovu, and 2 more authors

In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, Porto de Galinhas, Brazil, July 15-19, 2024, 2024

DOI Bib PDF Slides

@inproceedings{jain2024rapid,
  title = {Rapid Taint Assisted Concolic Execution (TACE)},
  author = {Jain, Ridhi and Tihanyi, Norbert and Ndhlovu, Mthandazo and Ferrag, Mohamed Amine and Cordeiro, Lucas C.},
  booktitle = {Companion Proceedings of the 32nd {ACM} International Conference on the Foundations of Software Engineering, {FSE} 2024, Porto de Galinhas, Brazil, July 15-19, 2024},
  pages = {627--631},
  year = {2024},
  publisher = {{ACM}},
  doi = {10.1145/3663529.3663812},
  editor = {d'Amorim, Marcelo},
  url = {https://doi.org/10.1145/3663529.3663812}
}

Revolutionizing Cyber Threat Detection With Large Language Models: A Privacy-Preserving BERT-Based Lightweight Model for IoT/IIoT Devices

Mohamed Amine Ferrag, Mthandazo Ndhlovu, Norbert Tihanyi, and 4 more authors

IEEE Access, 2024

DOI Bib

@article{ferrag2024revolutionizing,
  title = {Revolutionizing Cyber Threat Detection With Large Language Models: A Privacy-Preserving BERT-Based Lightweight Model for IoT/IIoT Devices},
  author = {Ferrag, Mohamed Amine and Ndhlovu, Mthandazo and Tihanyi, Norbert and Cordeiro, Lucas C. and Debbah, M{\'{e}}rouane and Lestable, Thierry and Thandi, Narinderjit Singh},
  journal = {{IEEE} Access},
  volume = {12},
  pages = {23733--23750},
  year = {2024},
  doi = {10.1109/ACCESS.2024.3363469},
  url = {https://doi.org/10.1109/ACCESS.2024.3363469}
}

Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

Tong Wu, Shale Xiong, Edoardo Manino, and 2 more authors

CoRR, 2024

DOI Bib PDF Slides

@article{wu2024verifying,
  title = {Verifying components of Arm(R) Confidential Computing Architecture with ESBMC},
  author = {Wu, Tong and Xiong, Shale and Manino, Edoardo and Stockwell, Gareth and Cordeiro, Lucas C.},
  journal = {CoRR},
  volume = {abs/2406.04375},
  year = {2024},
  doi = {10.48550/ARXIV.2406.04375},
  eprinttype = {arXiv},
  url = {https://doi.org/10.48550/arXiv.2406.04375}
}

2023

A fuzzing-based test-creation approach for evaluating digital TV receivers via transport streams

Fabrı́cio Izumi, Eddie B. Lima Filho, Lucas C. Cordeiro, and 4 more authors

Softw. Test. Verification Reliab., 2023

DOI Bib PDF Slides

@article{izumi2024fuzzing,
  title = {A fuzzing-based test-creation approach for evaluating digital TV receivers via transport streams},
  author = {Izumi, Fabr{\'{\i}}cio and de Lima Filho, Eddie B. and Cordeiro, Lucas C. and Maia, Orlewilson B. and Fabr{\'{\i}}cio, R{\{o}}mulo and Farias, Bruno and Silva, Aguinaldo},
  journal = {Softw. Test. Verification Reliab.},
  volume = {33},
  number = {1},
  year = {2023},
  doi = {10.1002/STVR.1833},
  url = {https://doi.org/10.1002/stvr.1833}
}

A fuzzing-based test-creation approach for evaluating digital TV receivers via transport streams

Fabrı́cio Izumi, Eddie B. Lima Filho, Lucas C. Cordeiro, and 4 more authors

Softw. Test. Verification Reliab., 2023

DOI Bib PDF

@article{izumi2023fuzzing,
  title = {A fuzzing-based test-creation approach for evaluating digital TV receivers via transport streams},
  author = {Izumi, Fabr{\'{\i}}cio and de Lima Filho, Eddie B. and Cordeiro, Lucas C. and Maia, Orlewilson B. and Fabr{\'{\i}}cio, R{\{o}}mulo and Farias, Bruno and Silva, Aguinaldo},
  journal = {Softw. Test. Verification Reliab.},
  volume = {33},
  number = {1},
  year = {2023},
  doi = {10.1002/stvr.1833},
  url = {https://doi.org/10.1002/stvr.1833}
}

A Privacy-Preserving and Accountable Billing Protocol for Peer-to-Peer Energy Trading Markets

Kamil Erdayandi, Lucas C. Cordeiro, and Mustafa A. Mustafa

CoRR, 2023

DOI Bib PDF

@article{erdayandi2023privacy,
  title = {A Privacy-Preserving and Accountable Billing Protocol for Peer-to-Peer Energy Trading Markets},
  author = {Erdayandi, Kamil and Cordeiro, Lucas C. and Mustafa, Mustafa A.},
  journal = {CoRR},
  volume = {abs/2307.04501},
  year = {2023},
  doi = {10.48550/ARXIV.2307.04501},
  eprinttype = {arXiv},
  url = {https://doi.org/10.48550/arXiv.2307.04501}
}

ICSE

AIREPAIR: A Repair Platform for Neural Networks

Xidan Song, Youcheng Sun, Mustafa A. Mustafa, and 1 more author

In 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, Melbourne, Australia, May 14-20, 2023, 2023

DOI Bib PDF Slides

@inproceedings{song2023airepair,
  title = {AIREPAIR: A Repair Platform for Neural Networks},
  author = {Song, Xidan and Sun, Youcheng and Mustafa, Mustafa A. and Cordeiro, Lucas C.},
  booktitle = {45th {IEEE/ACM} International Conference on Software Engineering: {ICSE} 2023 Companion Proceedings, Melbourne, Australia, May 14-20, 2023},
  pages = {98--101},
  year = {2023},
  publisher = {{IEEE}},
  doi = {10.1109/ICSE-COMPANION58688.2023.00033},
  url = {https://doi.org/10.1109/ICSE-Companion58688.2023.00033}
}

Certified Private Inference on Neural Networks via Lipschitz-Guided Abstraction Refinement

Edoardo Manino, Bernardo Magri, Mustafa A. Mustafa, and 1 more author

In Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023, 2023

DOI Bib PDF Slides

@inproceedings{manino2023certified,
  title = {Certified Private Inference on Neural Networks via Lipschitz-Guided Abstraction Refinement},
  author = {Manino, Edoardo and Magri, Bernardo and Mustafa, Mustafa A. and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023},
  volume = {16},
  pages = {35--46},
  year = {2023},
  publisher = {EasyChair},
  series = {Kalpa Publications in Computing},
  doi = {10.29007/59W3},
  editor = {Narodytska, Nina and Amir, Guy and Katz, Guy and Isac, Omri},
  url = {https://doi.org/10.29007/59w3}
}

TACAS

EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution)

Fatimah Aljaafari, Fedor Shmarov, Edoardo Manino, and 2 more authors

In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II, 2023

DOI Bib PDF Video Slides

@inproceedings{aljaafari2023black,
  title = {EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution)},
  author = {Aljaafari, Fatimah and Shmarov, Fedor and Manino, Edoardo and Menezes, Rafael and Cordeiro, Lucas C.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
  volume = {13994},
  pages = {541--546},
  year = {2023},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-30820-8_33},
  editor = {Sankaranarayanan, Sriram and Sharygina, Natasha},
  url = {https://doi.org/10.1007/978-3-031-30820-8\_33}
}

ESBMC v7.3: Model Checking C++ Programs Using Clang AST

Kunjian Song, Mikhail R. Gadelha, Franz Brauße, and 2 more authors

In Formal Methods: Foundations and Applications - 26th Brazilian Symposium, SBMF 2023, Manaus, Brazil, December 4-8, 2023, Proceedings, 2023

DOI Bib PDF

@inproceedings{song2023esbmc,
  title = {ESBMC v7.3: Model Checking C++ Programs Using Clang AST},
  author = {Song, Kunjian and Gadelha, Mikhail R. and Brau{\ss}e, Franz and Menezes, Rafael S. and Cordeiro, Lucas C.},
  booktitle = {Formal Methods: Foundations and Applications - 26th Brazilian Symposium, {SBMF} 2023, Manaus, Brazil, December 4-8, 2023, Proceedings},
  volume = {14414},
  pages = {141--152},
  year = {2023},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-49342-3_9},
  editor = {Barbosa, Haniel and Zohar, Yoni},
  url = {https://doi.org/10.1007/978-3-031-49342-3\_9}
}

Edge Learning for 6G-Enabled Internet of Things: A Comprehensive Survey of Vulnerabilities, Datasets, and Defenses

Mohamed Amine Ferrag, Othmane Friha, Burak Kantarci, and 6 more authors

IEEE Commun. Surv. Tutorials, 2023

DOI Bib

@article{ferrag2023edge,
  title = {Edge Learning for 6G-Enabled Internet of Things: A Comprehensive Survey of Vulnerabilities, Datasets, and Defenses},
  author = {Ferrag, Mohamed Amine and Friha, Othmane and Kantarci, Burak and Tihanyi, Norbert and Cordeiro, Lucas C. and Debbah, M{\'{e}}rouane and Hamouda, Djallel and Al{-}Hawawreh, Muna and Choo, Kim{-}Kwang Raymond},
  journal = {{IEEE} Commun. Surv. Tutorials},
  volume = {25},
  number = {4},
  pages = {2654--2713},
  year = {2023},
  doi = {10.1109/COMST.2023.3317242},
  url = {https://doi.org/10.1109/COMST.2023.3317242}
}

ICCE

Evaluation of Ginga’s CC-Web-Service Module

Sergillam Barroso Oliveira, Andre R. Silva Conceição, Eddie Batista Lima Filho, and 1 more author

In International Conference on Consumer Electronics - Taiwan, ICCE-Taiwan 2023, PingTung, Taiwan, July 17-19, 2023, 2023

DOI Bib PDF Poster

@inproceedings{oliveira2023evaluation,
  title = {Evaluation of Ginga's CC-Web-Service Module},
  author = {Oliveira, Sergillam Barroso and da Silva Concei{\c{c}}{\~{a}}o, Andre R. and de Lima Filho, Eddie Batista and Cordeiro, Lucas C.},
  booktitle = {International Conference on Consumer Electronics - Taiwan, ICCE-Taiwan 2023, PingTung, Taiwan, July 17-19, 2023},
  pages = {697--698},
  year = {2023},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE-TAIWAN58799.2023.10226701},
  url = {https://doi.org/10.1109/ICCE-Taiwan58799.2023.10226701}
}

FASE

FuSeBMC_IA: Interval Analysis and Methods for Test Case Generation - (Competition Contribution)

Mohannad Aldughaim, Kaled M. Alshmrany, Mikhail R. Gadelha, and 2 more authors

In Fundamental Approaches to Software Engineering - 26th International Conference, FASE 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, 2023

DOI Bib PDF Video Slides

@inproceedings{aldughaim2023fusebmc,
  title = {FuSeBMC\_IA: Interval Analysis and Methods for Test Case Generation - (Competition Contribution)},
  author = {Aldughaim, Mohannad and Alshmrany, Kaled M. and Gadelha, Mikhail R. and de Freitas, Rosiane and Cordeiro, Lucas C.},
  booktitle = {Fundamental Approaches to Software Engineering - 26th International Conference, {FASE} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 22-27, 2023, Proceedings},
  volume = {13991},
  pages = {324--329},
  year = {2023},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-30826-0_18},
  editor = {Lambers, Leen and Uchitel, Sebasti{\'{a}}n},
  url = {https://doi.org/10.1007/978-3-031-30826-0\_18}
}

Interventional Probing in High Dimensions: An NLI Case Study

Julia Rozanova, Marco Valentino, Lucas C. Cordeiro, and 1 more author

In Findings of the Association for Computational Linguistics: EACL 2023, Dubrovnik, Croatia, May 2-6, 2023, 2023

DOI Bib HTML

@inproceedings{rozanova2023interventional,
  title = {Interventional Probing in High Dimensions: An NLI Case Study},
  author = {Rozanova, Julia and Valentino, Marco and Cordeiro, Lucas C. and Freitas, Andr{\'{e}}},
  booktitle = {Findings of the Association for Computational Linguistics: {EACL} 2023, Dubrovnik, Croatia, May 2-6, 2023},
  volume = {{EACL} 2023},
  pages = {2444--2455},
  year = {2023},
  publisher = {Association for Computational Linguistics},
  series = {Findings of {ACL}},
  doi = {10.18653/V1/2023.FINDINGS-EACL.188},
  editor = {Vlachos, Andreas and Augenstein, Isabelle},
  url = {https://doi.org/10.18653/v1/2023.findings-eacl.188}
}

LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects

J. O.; Farias B. C Sousa, T. A Silva, E. B Lima Filho, and 1 more author

In 23rd Brazilian Symposium on Information and Computational Systems Security (SBSeg), 2023

Bib PDF Slides

@inproceedings{cordeiro2023lsverifier,
  title = {LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software Projects},
  author = {Sousa, J. O.; Farias B. C and Silva, T. A and Lima Filho, E. B and Cordeiro, L. C},
  booktitle = {23rd Brazilian Symposium on Information and Computational Systems Security (SBSeg)},
  pages = {1--8},
  year = {2023},
}

MISOFuzz: A Modular Infrastructure for Scalable Fuzzing Orchestration

N Gervasoni, M Lubinets, R Jain, and 1 more author

In 4th Workshop on Cooperative Software Veriﬁcation (COOP), 2023. 35. Rozanova, J., Valentino, M., Cordeiro, L. C., Freitas, A, 2023

Bib PDF Video Slides

@inproceedings{cordeiro2023misofuzz,
  title = {MISOFuzz: A Modular Infrastructure for Scalable Fuzzing Orchestration},
  author = {Gervasoni, N and Lubinets, M and Jain, R and Cordeiro, L. C},
  booktitle = {4th Workshop on Cooperative Software Veriﬁcation (COOP), 2023. 35. Rozanova, J., Valentino, M., Cordeiro, L. C., Freitas, A},
  year = {2023},
}

QNNRepair: Quantized Neural Network Repair

Xidan Song, Youcheng Sun, Mustafa A. Mustafa, and 1 more author

In Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings, 2023

DOI Bib PDF Slides

@inproceedings{song2023qnnrepair,
  title = {QNNRepair: Quantized Neural Network Repair},
  author = {Song, Xidan and Sun, Youcheng and Mustafa, Mustafa A. and Cordeiro, Lucas C.},
  booktitle = {Software Engineering and Formal Methods - 21st International Conference, {SEFM} 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings},
  volume = {14323},
  pages = {320--339},
  year = {2023},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-47115-5_18},
  editor = {Ferreira, Carla and Willemse, Tim A. C.},
  url = {https://doi.org/10.1007/978-3-031-47115-5\_18}
}

The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification

Norbert Tihanyi, Tamás Bisztray, Ridhi Jain, and 3 more authors

In Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering, PROMISE 2023, San Francisco, CA, USA, 8 December 2023, 2023

DOI Bib PDF Slides

@inproceedings{tihanyi2023formai,
  title = {The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification},
  author = {Tihanyi, Norbert and Bisztray, Tam{\'{a}}s and Jain, Ridhi and Ferrag, Mohamed Amine and Cordeiro, Lucas C. and Mavroeidis, Vasileios},
  booktitle = {Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering, {PROMISE} 2023, San Francisco, CA, USA, 8 December 2023},
  pages = {33--43},
  year = {2023},
  publisher = {{ACM}},
  doi = {10.1145/3617555.3617874},
  editor = {McIntosh, Shane and Choi, Eunjong and Herbold, Steffen},
  url = {https://doi.org/10.1145/3617555.3617874}
}

Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration

Rafael G. Silvestrim, Felipe V. Trigo, Williame Rocha, and 5 more authors

In XIII Brazilian Symposium on Computing Systems Engineering, SBESC 2023, Porto Alegre, Brazil, November 21-24, 2023, 2023

DOI Bib PDF

@inproceedings{silvestrim2023integrity,
  title = {Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration},
  author = {Silvestrim, Rafael G. and Trigo, Felipe V. and Rocha, Williame and Vieira, Michael R. S. and Junior, Jogno V. and Mendes, Otoniel Da C. and Menezes, Rafael S{\'{a}} and Cordeiro, Lucas C.},
  booktitle = {{XIII} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2023, Porto Alegre, Brazil, November 21-24, 2023},
  pages = {1--6},
  year = {2023},
  publisher = {{IEEE}},
  doi = {10.1109/SBESC60926.2023.10324098},
  url = {https://doi.org/10.1109/SBESC60926.2023.10324098}
}

Towards global neural network abstractions with locally-exact reconstruction

Edoardo Manino, Iury Bessa, and Lucas C. Cordeiro

Neural Networks, 2023

DOI Bib

@article{manino2023global,
  title = {Towards global neural network abstractions with locally-exact reconstruction},
  author = {Manino, Edoardo and Bessa, Iury and Cordeiro, Lucas C.},
  journal = {Neural Networks},
  volume = {165},
  pages = {344--357},
  year = {2023},
  doi = {10.1016/j.neunet.2023.06.002},
  url = {https://doi.org/10.1016/j.neunet.2023.06.002}
}

2022

CEG4N: Counter-Example Guided Neural Network Quantization Refinement

João Batista Pereira Matos Jr., Iury Bessa, Edoardo Manino, and 2 more authors

In Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Haifa, Israel, July 31 - August 1, and August 11, 2022, Proceedings, 2022

DOI Bib PDF

@inproceedings{jr2022counter,
  title = {CEG4N: Counter-Example Guided Neural Network Quantization Refinement},
  author = {Jr., Jo{\~{a}}o Batista Pereira Matos and Bessa, Iury and Manino, Edoardo and Song, Xidan and Cordeiro, Lucas C.},
  booktitle = {Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, {NSV} 2022, Haifa, Israel, July 31 - August 1, and August 11, 2022, Proceedings},
  volume = {13466},
  pages = {29--45},
  year = {2022},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-031-21222-2_3},
  editor = {Isac, Omri and Ivanov, Radoslav and Katz, Guy and Narodytska, Nina and Nenzi, Laura},
  url = {https://doi.org/10.1007/978-3-031-21222-2\_3}
}

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs

Fatimah K. Aljaafari, Rafael Menezes, Edoardo Manino, and 3 more authors

IEEE Access, 2022

DOI Bib

@article{aljaafari2022combining,
  title = {Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs},
  author = {Aljaafari, Fatimah K. and Menezes, Rafael and Manino, Edoardo and Shmarov, Fedor and Mustafa, Mustafa A. and Cordeiro, Lucas C.},
  journal = {{IEEE} Access},
  volume = {10},
  pages = {121365--121384},
  year = {2022},
  doi = {10.1109/ACCESS.2022.3223359},
  url = {https://doi.org/10.1109/ACCESS.2022.3223359}
}

Control flow graph, formal verification and constraint programming techniques

J Deveza, L Santos, L Freitas, and 1 more author

In 10th Latin American Workshop on Cliques in Graphs (LAWCG), 2022 (to appear), 2022

Bib PDF

@inproceedings{cordeiro2022control,
  title = {Control flow graph, formal verification and constraint programming techniques},
  author = {Deveza, J and Santos, L and de Freitas, L and Cordeiro, L. C},
  booktitle = {10th Latin American Workshop on Cliques in Graphs (LAWCG), 2022 (to appear)},
  year = {2022},
}

ISSTA

ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC

Franz Brauße, Fedor Shmarov, Rafael Menezes, and 4 more authors

In ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022, 2022

DOI Bib PDF

@inproceedings{brausse2022esbmc,
  title = {ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC},
  author = {Brau{\ss}e, Franz and Shmarov, Fedor and Menezes, Rafael and Gadelha, Mikhail R. and Korovin, Konstantin and Reger, Giles and Cordeiro, Lucas C.},
  booktitle = {{ISSTA} '22: 31st {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022},
  pages = {773--776},
  year = {2022},
  publisher = {{ACM}},
  doi = {10.1145/3533767.3543289},
  editor = {Ryu, Sukyoung and Smaragdakis, Yannis},
  url = {https://doi.org/10.1145/3533767.3543289}
}

ISSTA

ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation

Rafael Menezes, Daniel Moura, Helena Cavalcante, and 2 more authors

In ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022, 2022

DOI Bib PDF

@inproceedings{menezes2022esbmc,
  title = {ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation},
  author = {Menezes, Rafael and Moura, Daniel and Cavalcante, Helena and de Freitas, Rosiane and Cordeiro, Lucas C.},
  booktitle = {{ISSTA} '22: 31st {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022},
  pages = {777--780},
  year = {2022},
  publisher = {{ACM}},
  doi = {10.1145/3533767.3543294},
  editor = {Ryu, Sukyoung and Smaragdakis, Yannis},
  url = {https://doi.org/10.1145/3533767.3543294}
}

ICSE

ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

Kunjian Song, Nedas Matulevicius, Eddie B. Lima Filho, and 1 more author

In 44th IEEE/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2022, Pittsburgh, PA, USA, May 22-24, 2022, 2022

DOI Bib PDF

@inproceedings{song2022esbmc,
  title = {ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts},
  author = {Song, Kunjian and Matulevicius, Nedas and de Lima Filho, Eddie B. and Cordeiro, Lucas C.},
  booktitle = {44th {IEEE/ACM} International Conference on Software Engineering: Companion Proceedings, {ICSE} Companion 2022, Pittsburgh, PA, USA, May 22-24, 2022},
  pages = {65--69},
  year = {2022},
  publisher = {{ACM/IEEE}},
  doi = {10.1145/3510454.3516855},
  url = {https://doi.org/10.1145/3510454.3516855}
}

EnnCore: End-to-End Conceptual Guarding of Neural Architectures

Edoardo Manino, Danilo S. Carvalho, Yi Dong, and 8 more authors

In Proceedings of the Workshop on Artificial Intelligence Safety 2022 (SafeAI 2022) co-located with the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI2022), Virtual, February, 2022, 2022

Bib PDF

@inproceedings{manino2022enncore,
  title = {EnnCore: End-to-End Conceptual Guarding of Neural Architectures},
  author = {Manino, Edoardo and Carvalho, Danilo S. and Dong, Yi and Rozanova, Julia and Song, Xidan and Mustafa, Mustafa A. and Freitas, Andr{\'{e}} and Brown, Gavin and Luj{\'{a}}n, Mikel and Huang, Xiaowei and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the Workshop on Artificial Intelligence Safety 2022 (SafeAI 2022) co-located with the Thirty-Sixth {AAAI} Conference on Artificial Intelligence (AAAI2022), Virtual, February, 2022},
  volume = {3087},
  year = {2022},
  publisher = {CEUR-WS.org},
  series = {{CEUR} Workshop Proceedings},
  editor = {Pedroza, Gabriel and Hern{\'{a}}ndez{-}Orallo, Jos{\'{e}} and Chen, Xin Cynthia and Huang, Xiaowei and Espinoza, Hu{\'{a}}scar and Castillo{-}Effen, Mauricio and McDermid, John A. and Mallah, Richard and h{\'{E}}igeartaigh, Se{\'{a}}n {\'{O}}},
  url = {https://ceur-ws.org/Vol-3087/paper\_9.pdf}
}

Formal Synthesis of Non-fragile State-Feedback Digital Controllers Considering Performance Requirements for Step Response

T Cavalcante, I Bessa, E Lima Filho, and 1 more author

Scientiﬁc Reports, 12, 15429 (2022). *13 Monteiro, F., Gadelha, M., Cordeiro, L. C, 2022

DOI Bib PDF

@article{cordeiro2022formal,
  title = {Formal Synthesis of Non-fragile State-Feedback Digital Controllers Considering Performance Requirements for Step Response},
  author = {Cavalcante, T and Bessa, I and de Lima Filho, E and Cordeiro, L},
  journal = {Scientiﬁc Reports, 12, 15429 (2022). *13 Monteiro, F., Gadelha, M., Cordeiro, L. C},
  year = {2022},
  doi = {10.1038/s41598-022-19284-4},
}

FASE

FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing - (Competition Contribution)

Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat, and 1 more author

In Fundamental Approaches to Software Engineering - 25th International Conference, FASE 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, 2022

DOI Bib PDF Slides

@inproceedings{alshmrany2022fusebmc,
  title = {FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing - (Competition Contribution)},
  author = {Alshmrany, Kaled M. and Aldughaim, Mohannad and Bhayat, Ahmed and Cordeiro, Lucas C.},
  booktitle = {Fundamental Approaches to Software Engineering - 25th International Conference, {FASE} 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7, 2022, Proceedings},
  volume = {13241},
  pages = {336--340},
  year = {2022},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-99429-7_19},
  editor = {Johnsen, Einar Broch and Wimmer, Manuel},
  url = {https://doi.org/10.1007/978-3-030-99429-7\_19}
}

Model checking C++ programs

Felipe R. Monteiro, Mikhail R. Gadelha, and Lucas C. Cordeiro

Softw. Test. Verification Reliab., 2022

DOI Bib PDF

@article{monteiro2022model,
  title = {Model checking C++ programs},
  author = {Monteiro, Felipe R. and Gadelha, Mikhail R. and Cordeiro, Lucas C.},
  journal = {Softw. Test. Verification Reliab.},
  volume = {32},
  number = {1},
  year = {2022},
  doi = {10.1002/stvr.1793},
  url = {https://doi.org/10.1002/stvr.1793}
}

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities

Kaled M. Alshmrany, Ahmed Bhayat, Franz Brauße, and 7 more authors

In IEEE Secure Development Conference, SecDev 2022, Atlanta, GA, USA, October 18-20, 2022, 2022

DOI Bib PDF Slides

@inproceedings{alshmrany2022position,
  title = {Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities},
  author = {Alshmrany, Kaled M. and Bhayat, Ahmed and Brau{\ss}e, Franz and Cordeiro, Lucas C. and Korovin, Konstantin and Melham, Tom and Mustafa, Mustafa A. and Olivier, Pierre and Reger, Giles and Shmarov, Fedor},
  booktitle = {{IEEE} Secure Development Conference, SecDev 2022, Atlanta, GA, USA, October 18-20, 2022},
  pages = {52--58},
  year = {2022},
  publisher = {{IEEE}},
  doi = {10.1109/SECDEV53368.2022.00020},
  url = {https://doi.org/10.1109/SecDev53368.2022.00020}
}

Privacy-Friendly Peer-to-Peer Energy Trading: A Game Theoretical Approach

Kamil Erdayandi, Amrit Paudel, Lucas C. Cordeiro, and 1 more author

CoRR, 2022

Bib PDF

@article{erdayandi2022privacy,
  title = {Privacy-Friendly Peer-to-Peer Energy Trading: A Game Theoretical Approach},
  author = {Erdayandi, Kamil and Paudel, Amrit and Cordeiro, Lucas C. and Mustafa, Mustafa A.},
  journal = {CoRR},
  volume = {abs/2201.01810},
  year = {2022},
  eprinttype = {arXiv},
  url = {https://arxiv.org/abs/2201.01810}
}

Summary of Model Checking C++ Programs

Felipe R. Monteiro, Mikhail R. Gadelha, and Lucas C. Cordeiro

In 15th IEEE Conference on Software Testing, Verification and Validation, ICST 2022, Valencia, Spain, April 4-14, 2022, 2022

DOI Bib PDF

@inproceedings{monteiro2022summary,
  title = {Summary of Model Checking C++ Programs},
  author = {Monteiro, Felipe R. and Gadelha, Mikhail R. and Cordeiro, Lucas C.},
  booktitle = {15th {IEEE} Conference on Software Testing, Verification and Validation, {ICST} 2022, Valencia, Spain, April 4-14, 2022},
  pages = {461},
  year = {2022},
  publisher = {{IEEE}},
  doi = {10.1109/ICST53961.2022.00054},
  url = {https://doi.org/10.1109/ICST53961.2022.00054}
}

Systematicity, Compositionality and Transitivity of Deep NLP Models: a Metamorphic Testing Perspective

Edoardo Manino, Julia Rozanova, Danilo S. Carvalho, and 2 more authors

In Findings of the Association for Computational Linguistics: ACL 2022, Dublin, Ireland, May 22-27, 2022, 2022

DOI Bib PDF Video Poster Slides

@inproceedings{manino2022systematicity,
  title = {Systematicity, Compositionality and Transitivity of Deep NLP Models: a Metamorphic Testing Perspective},
  author = {Manino, Edoardo and Rozanova, Julia and Carvalho, Danilo S. and Freitas, Andr{\'{e}} and Cordeiro, Lucas C.},
  booktitle = {Findings of the Association for Computational Linguistics: {ACL} 2022, Dublin, Ireland, May 22-27, 2022},
  volume = {{ACL} 2022},
  pages = {2355--2366},
  year = {2022},
  publisher = {Association for Computational Linguistics},
  series = {Findings of {ACL}},
  doi = {10.18653/V1/2022.FINDINGS-ACL.185},
  editor = {Muresan, Smaranda and Nakov, Preslav and Villavicencio, Aline},
  url = {https://doi.org/10.18653/v1/2022.findings-acl.185}
}

Towards Privacy Preserving Local Energy Markets

K Erdayandi, L. C Cordeiro, and M. O Mustafa

In Competitive Advantage in the Digital Economy (CADE), pp, 2022

DOI Bib PDF

@inproceedings{cordeiro2022privacy,
  title = {Towards Privacy Preserving Local Energy Markets},
  author = {Erdayandi, K and Cordeiro, L. C and Mustafa, M. O},
  booktitle = {Competitive Advantage in the Digital Economy (CADE), pp},
  year = {2022},
  doi = {10.1049/icp.2022.2053},
}

TACAS

Wit4Java: A violation-witness validator for Java Verifiers (Competition Paper)

T Wu, P Schrammel, and L. C Cordeiro

In 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 13244, pp, 2022

Bib PDF Video Slides

@inproceedings{cordeiro2022java,
  title = {Wit4Java: A violation-witness validator for Java Verifiers (Competition Paper)},
  author = {Wu, T and Schrammel, P and Cordeiro, L. C},
  booktitle = {28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 13244, pp},
  year = {2022},
}

2021

Assisted Counterexample-Guided Inductive Optimization for Robot Path Planning

Mengze Li and Lucas C. Cordeiro

In XI Brazilian Symposium on Computing Systems Engineering, SBESC 2021, Florianopolis, Brazil, November 22-26, 2021, 2021

DOI Bib PDF Video Slides

@inproceedings{li2021assisted,
  title = {Assisted Counterexample-Guided Inductive Optimization for Robot Path Planning},
  author = {Li, Mengze and Cordeiro, Lucas C.},
  booktitle = {{XI} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2021, Florianopolis, Brazil, November 22-26, 2021},
  pages = {1--8},
  year = {2021},
  publisher = {{IEEE}},
  doi = {10.1109/SBESC53686.2021.9628295},
  url = {https://doi.org/10.1109/SBESC53686.2021.9628295}
}

ESBMC 6.1: automated test case generation using bounded model checking

Mikhail R. Gadelha, Rafael S. Menezes, and Lucas C. Cordeiro

Int. J. Softw. Tools Technol. Transf., 2021

DOI Bib PDF

@article{gadelha2021esbmc,
  title = {ESBMC 6.1: automated test case generation using bounded model checking},
  author = {Gadelha, Mikhail R. and Menezes, Rafael S. and Cordeiro, Lucas C.},
  journal = {Int. J. Softw. Tools Technol. Transf.},
  volume = {23},
  number = {6},
  pages = {857--861},
  year = {2021},
  doi = {10.1007/s10009-020-00571-2},
  url = {https://doi.org/10.1007/s10009-020-00571-2}
}

Exploiting the SAT Revolution for Automated Software Verification: Report from an Industrial Case Study

Lucas C. Cordeiro

In 10th Latin-American Symposium on Dependable Computing, LADC 2021, Florianópolis, Brazil, November 22-26, 2021 - Companion Volume, 2021

DOI Bib PDF Video

@inproceedings{cordeiro2021exploiting,
  title = {Exploiting the SAT Revolution for Automated Software Verification: Report from an Industrial Case Study},
  author = {Cordeiro, Lucas C.},
  booktitle = {10th Latin-American Symposium on Dependable Computing, {LADC} 2021, Florian{\'{o}}polis, Brazil, November 22-26, 2021 - Companion Volume},
  pages = {8--9},
  year = {2021},
  publisher = {Brazilian Computing Society},
  doi = {10.5753/LADC.2021.18531},
  url = {https://doi.org/10.5753/ladc.2021.18531}
}

FASE

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)

Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha, and 1 more author

In Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, 2021

DOI Bib PDF Video Slides

@inproceedings{alshmrany2021fusebmc,
  title = {FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)},
  author = {Alshmrany, Kaled M. and Menezes, Rafael S. and Gadelha, Mikhail R. and Cordeiro, Lucas C.},
  booktitle = {Fundamental Approaches to Software Engineering - 24th International Conference, {FASE} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings},
  volume = {12649},
  pages = {363--367},
  year = {2021},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-71500-7_19},
  editor = {Guerra, Esther and Stoelinga, Mari{\"{e}}lle},
  url = {https://doi.org/10.1007/978-3-030-71500-7\_19}
}

FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs

Kaled M. Alshmrany, Mohannad Aldughaim, Ahmed Bhayat, and 1 more author

In Tests and Proofs - 15th International Conference, TAP 2021, Held as Part of STAF 2021, Virtual Event, June 21-22, 2021, Proceedings, 2021

DOI Bib PDF Slides

@inproceedings{alshmrany2021fusebmc2,
  title = {FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs},
  author = {Alshmrany, Kaled M. and Aldughaim, Mohannad and Bhayat, Ahmed and Cordeiro, Lucas C.},
  booktitle = {Tests and Proofs - 15th International Conference, {TAP} 2021, Held as Part of {STAF} 2021, Virtual Event, June 21-22, 2021, Proceedings},
  volume = {12740},
  pages = {85--105},
  year = {2021},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-79379-1_6},
  editor = {Loulergue, Fr{\'{e}}d{\'{e}}ric and Wotawa, Franz},
  url = {https://doi.org/10.1007/978-3-030-79379-1\_6}
}

Hardware Update through Digital TV Signals

R Olveira, F Guimaraes, M Lucena, and 3 more authors

Electronics, 2021

DOI Bib

@article{cordeiro2021hardware,
  title = {Hardware Update through Digital TV Signals},
  author = {de Olveira, R and Guimaraes, F and de Lucena, M and Cordeiro, L and de Lima Filho, E and de Lucena Jr, V},
  journal = {Electronics},
  volume = {10},
  number = {24},
  pages = {1--20},
  year = {2021},
  doi = {10.3390/electronics10243072},
}

Verification and refutation of C programs based on k-induction and invariant inference

Omar M. Alhawi, Herbert Rocha, Mikhail R. Gadelha, and 2 more authors

Int. J. Softw. Tools Technol. Transf., 2021

DOI Bib PDF

@article{alhawi2021verification,
  title = {Verification and refutation of C programs based on k-induction and invariant inference},
  author = {Alhawi, Omar M. and Rocha, Herbert and Gadelha, Mikhail R. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {Int. J. Softw. Tools Technol. Transf.},
  volume = {23},
  number = {2},
  pages = {115--135},
  year = {2021},
  doi = {10.1007/s10009-020-00564-1},
  url = {https://doi.org/10.1007/s10009-020-00564-1}
}

Verifying Security Vulnerabilities for Blockchain-based Smart Contracts

Nedas Matulevicius and Lucas C. Cordeiro

In XI Brazilian Symposium on Computing Systems Engineering, SBESC 2021, Florianopolis, Brazil, November 22-26, 2021, 2021

DOI Bib PDF Video Slides

@inproceedings{matulevicius2021verifying,
  title = {Verifying Security Vulnerabilities for Blockchain-based Smart Contracts},
  author = {Matulevicius, Nedas and Cordeiro, Lucas C.},
  booktitle = {{XI} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2021, Florianopolis, Brazil, November 22-26, 2021},
  pages = {1--8},
  year = {2021},
  publisher = {{IEEE}},
  doi = {10.1109/SBESC53686.2021.9628229},
  url = {https://doi.org/10.1109/SBESC53686.2021.9628229}
}

2020

Survey on automated symbolic verification and its application for synthesising cyber-physical systems

Lucas C. Cordeiro, Eddie Batista Lima Filho, and Iury Valente Bessa

IET Cyper-Phys. Syst.: Theory & Appl., 2020

DOI Bib PDF

@article{cordeiro2020survey,
  title = {Survey on automated symbolic verification and its application for synthesising cyber-physical systems},
  author = {Cordeiro, Lucas C. and de Lima Filho, Eddie Batista and de Bessa, Iury Valente},
  journal = {{IET} Cyper-Phys. Syst.: Theory {\&} Appl.},
  volume = {5},
  number = {1},
  pages = {1--24},
  year = {2020},
  doi = {10.1049/iet-cps.2018.5006},
  url = {https://doi.org/10.1049/iet-cps.2018.5006}
}

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs

Mikhail R. Gadelha, Lucas C. Cordeiro, and Denis A. Nicole

In Software Verification - 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers, 2020

DOI Bib PDF Video Slides

@inproceedings{gadelha2020efficient,
  title = {An Efficient Floating-Point Bit-Blasting API for Verifying C Programs},
  author = {Gadelha, Mikhail R. and Cordeiro, Lucas C. and Nicole, Denis A.},
  booktitle = {Software Verification - 12th International Conference, {VSTTE} 2020, and 13th International Workshop, {NSV} 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers},
  volume = {12549},
  pages = {178--195},
  year = {2020},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-63618-0_11},
  editor = {Christakis, Maria and Polikarpova, Nadia and Duggirala, Parasara Sridhar and Schrammel, Peter},
  url = {https://doi.org/10.1007/978-3-030-63618-0\_11}
}

Classificação Automática de Modulações Utilizando Redes Neurais Artificais com Regularização Bayesiana e Algoritmo de Retropropagação de Levenberg-Marquardt

M Valadão, A Pereira, D Amoedo, and 5 more authors

In 38th Brazilian Symposium on Telecommunications and Signal, pp, 2020

Bib PDF

@inproceedings{cordeiro2020classifica,
  title = {Classificação Automática de Modulações Utilizando Redes Neurais Artificais com Regularização Bayesiana e Algoritmo de Retropropagação de Levenberg-Marquardt},
  author = {Valadão, M and Pereira, A and Amoedo, D and Lima Filho, E and Carvalho, C and Costa, A and Cordeiro, L and Silva Júnior, W},
  booktitle = {38th Brazilian Symposium on Telecommunications and Signal, pp},
  year = {2020},
}

FASE

ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory - (Competition Contribution)

Mikhail Y. R. Gadelha, Rafael Menezes, Felipe R. Monteiro, and 2 more authors

In Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, 2020

DOI Bib PDF

@inproceedings{gadelha2020esbmc,
  title = {ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory - (Competition Contribution)},
  author = {Gadelha, Mikhail Y. R. and Menezes, Rafael and Monteiro, Felipe R. and Cordeiro, Lucas C. and Nicole, Denis A.},
  booktitle = {Fundamental Approaches to Software Engineering - 23rd International Conference, {FASE} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings},
  volume = {12076},
  pages = {525--529},
  year = {2020},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-45234-6_27},
  editor = {Wehrheim, Heike and Cabot, Jordi},
  url = {https://doi.org/10.1007/978-3-030-45234-6\_27}
}

Formal Non-fragile Verification of Step Response Requirements for Digital State-Feedback Control Systems

A Cavalcante, I Bessa, and E. Cordeiro L Lima Filho

Journal of Control, Automation and Electrical Systems, 2020

DOI Bib PDF

@article{cordeiro2020formal,
  title = {Formal Non-fragile Verification of Step Response Requirements for Digital State-Feedback Control Systems},
  author = {Cavalcante, A and Bessa, I and de Lima Filho, E. Cordeiro L},
  journal = {Journal of Control, Automation and Electrical Systems},
  volume = {31},
  number = {3},
  pages = {1--21},
  year = {2020},
  doi = {10.1007/s40313-020-00575-y},
}

TACAS

Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution)

Herbert Rocha, Rafael Menezes, Lucas C. Cordeiro, and 1 more author

In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, 2020

DOI Bib PDF

@inproceedings{rocha2020check,
  title = {Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution)},
  author = {Rocha, Herbert and Menezes, Rafael and Cordeiro, Lucas C. and Barreto, Raimundo S.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, {TACAS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {II}},
  volume = {12079},
  pages = {403--407},
  year = {2020},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-45237-7_29},
  editor = {Biere, Armin and Parker, David},
  url = {https://doi.org/10.1007/978-3-030-45237-7\_29}
}

Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison

Alessandro Trindade and Lucas C. Cordeiro

In Software Verification - 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers, 2020

DOI Bib PDF Video Slides

@inproceedings{trindade2020synthesis,
  title = {Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison},
  author = {Trindade, Alessandro and Cordeiro, Lucas C.},
  booktitle = {Software Verification - 12th International Conference, {VSTTE} 2020, and 13th International Workshop, {NSV} 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers},
  volume = {12549},
  pages = {87--105},
  year = {2020},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-63618-0_6},
  editor = {Christakis, Maria and Polikarpova, Nadia and Duggirala, Parasara Sridhar and Schrammel, Peter},
  url = {https://doi.org/10.1007/978-3-030-63618-0\_6}
}

Automated formal synthesis of provably safe digital controllers for continuous plants

Alessandro Abate, Iury Bessa, Lucas C. Cordeiro, and 4 more authors

Acta Informatica, 2020

DOI Bib PDF

@article{abate2019automated,
  title = {Automated formal synthesis of provably safe digital controllers for continuous plants},
  author = {Abate, Alessandro and Bessa, Iury and Cordeiro, Lucas C. and David, Cristina and Kesseli, Pascal and Kroening, Daniel and Polgreen, Elizabeth},
  journal = {Acta Informatica},
  volume = {57},
  number = {1-2},
  pages = {223--244},
  year = {2020},
  doi = {10.1007/s00236-019-00359-1},
  url = {https://doi.org/10.1007/s00236-019-00359-1}
}

2019

Boost the Impact of Continuous Formal Verification in Industry

Felipe R. Monteiro, Mikhail Y. R. Gadelha, and Lucas C. Cordeiro

CoRR, 2019

Bib PDF Slides

@article{monteiro2019boost,
  title = {Boost the Impact of Continuous Formal Verification in Industry},
  author = {Monteiro, Felipe R. and Gadelha, Mikhail Y. R. and Cordeiro, Lucas C.},
  journal = {CoRR},
  volume = {abs/1904.06152},
  year = {2019},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1904.06152}
}

Compressão de Sinais de Eletrocardiograma Utilizando Técnicas de Codificação Distribuída

P Souza, E Lima Filho, L Cordeiro, and 1 more author

In 37th Brazilian Symposium on Telecommunications and Signal Processing (SBrT), pp, 2019

Bib PDF

@inproceedings{cordeiro2019compress,
  title = {Compressão de Sinais de Eletrocardiograma Utilizando Técnicas de Codificação Distribuída},
  author = {Souza, P and Lima Filho, E and Cordeiro, L and Silva Júnior, W},
  booktitle = {37th Brazilian Symposium on Telecommunications and Signal Processing (SBrT), pp},
  year = {2019},
}

TACAS

ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution)

Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, and 1 more author

In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, 2019

DOI Bib PDF Slides

@inproceedings{gadelha2019esbmc,
  title = {ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution)},
  author = {Gadelha, Mikhail Y. R. and Monteiro, Felipe R. and Cordeiro, Lucas C. and Nicole, Denis A.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}},
  volume = {11429},
  pages = {209--213},
  year = {2019},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-17502-3_15},
  editor = {Beyer, Dirk and Huisman, Marieke and Kordon, Fabrice and Steffen, Bernhard},
  url = {https://doi.org/10.1007/978-3-030-17502-3\_15}
}

Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification

Omar M. Alhawi, Mustafa A. Mustafa, and Lucas C. Cordeiro

In 2019 International Workshop on Secure Internet of Things, SIoT 2019, Luxembourg, Luxembourg, September 26, 2019, 2019

DOI Bib PDF Slides

@inproceedings{alhawi2019finding,
  title = {Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification},
  author = {Alhawi, Omar M. and Mustafa, Mustafa A. and Cordeiro, Lucas C.},
  booktitle = {2019 International Workshop on Secure Internet of Things, SIoT 2019, Luxembourg, Luxembourg, September 26, 2019},
  pages = {1--9},
  year = {2019},
  publisher = {{IEEE}},
  doi = {10.1109/SIOT48044.2019.9637109},
  url = {https://doi.org/10.1109/SIOT48044.2019.9637109}
}

Incremental Bounded Model Checking of Artificial Neural Networks in CUDA

Luiz H. Sena, Iury Valente Bessa, Mikhail Y. R. Gadelha, and 2 more authors

In IX Brazilian Symposium on Computing Systems Engineering, SBESC 2019, Natal, Brazil, November 19-22, 2019, 2019

DOI Bib PDF Slides

@inproceedings{sena2019incremental,
  title = {Incremental Bounded Model Checking of Artificial Neural Networks in CUDA},
  author = {Sena, Luiz H. and de Bessa, Iury Valente and Gadelha, Mikhail Y. R. and Cordeiro, Lucas C. and Mota, Edjard},
  booktitle = {{IX} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2019, Natal, Brazil, November 19-22, 2019},
  pages = {1--8},
  year = {2019},
  publisher = {{IEEE}},
  doi = {10.1109/SBESC49506.2019.9046094},
  url = {https://doi.org/10.1109/SBESC49506.2019.9046094}
}

TACAS

JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution)

Lucas C. Cordeiro, Daniel Kroening, and Peter Schrammel

DOI Bib PDF Poster Slides

@inproceedings{cordeiro2019jbmc,
  title = {JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution)},
  author = {Cordeiro, Lucas C. and Kroening, Daniel and Schrammel, Peter},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}},
  volume = {11429},
  pages = {219--223},
  year = {2019},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-17502-3_17},
  editor = {Beyer, Dirk and Huisman, Marieke and Kordon, Fabrice and Steffen, Bernhard},
  url = {https://doi.org/10.1007/978-3-030-17502-3\_17}
}

ICSE

SMT-based refutation of spurious bug reports in the clang static analyzer

Mikhail Y. R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro, and 2 more authors

In Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, ICSE 2019, Montreal, QC, Canada, May 25-31, 2019, 2019

DOI Bib PDF Poster Slides

@inproceedings{gadelha2019refutation,
  title = {SMT-based refutation of spurious bug reports in the clang static analyzer},
  author = {Gadelha, Mikhail Y. R. and Steffinlongo, Enrico and Cordeiro, Lucas C. and Fischer, Bernd and Nicole, Denis A.},
  booktitle = {Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, {ICSE} 2019, Montreal, QC, Canada, May 25-31, 2019},
  pages = {11--14},
  year = {2019},
  publisher = {{IEEE} / {ACM}},
  doi = {10.1109/ICSE-COMPANION.2019.00026},
  editor = {Atlee, Joanne M. and Bultan, Tevfik and Whittle, Jon},
  url = {https://doi.org/10.1109/ICSE-Companion.2019.00026}
}

Verifying fragility in digital systems with uncertainties using DSVerifier \emphv2.0

Lennon C. Chaves, Hussama Ibrahim Ismail, Iury Valente Bessa, and 2 more authors

J. Syst. Softw., 2019

DOI Bib PDF

@article{chaves2019verifying,
  title = {Verifying fragility in digital systems with uncertainties using DSVerifier \emphv2.0},
  author = {Chaves, Lennon C. and Ismail, Hussama Ibrahim and de Bessa, Iury Valente and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {J. Syst. Softw.},
  volume = {153},
  pages = {22--43},
  year = {2019},
  doi = {10.1016/j.jss.2019.03.015},
  url = {https://doi.org/10.1016/j.jss.2019.03.015}
}

2018

Automated Verification of Stand-alone Solar Photovoltaic Systems

Alessandro Trindade and Lucas C. Cordeiro

CoRR, 2018

DOI Bib PDF

@article{trindade2019automated,
  title = {Automated Verification of Stand-alone Solar Photovoltaic Systems},
  author = {Trindade, Alessandro and Cordeiro, Lucas C.},
  journal = {CoRR},
  volume = {abs/1811.09438},
  year = {2018},
  doi = {10.1016/j.solener.2019.09.093},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1811.09438}
}

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

Lucas C. Cordeiro, Daniel Kroening, and Peter Schrammel

ACM SIGSOFT Softw. Eng. Notes, 2018

DOI Bib PDF Slides

@article{cordeiro2018benchmarking,
  title = {Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)},
  author = {Cordeiro, Lucas C. and Kroening, Daniel and Schrammel, Peter},
  journal = {{ACM} {SIGSOFT} Softw. Eng. Notes},
  volume = {43},
  number = {4},
  pages = {56},
  year = {2018},
  doi = {10.1145/3282517.3282529},
  url = {https://doi.org/10.1145/3282517.3282529}
}

ASE

Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract)

Felipe R. Monteiro, Mário A. P. Garcia, Lucas C. Cordeiro, and 1 more author

In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, 2018

DOI Bib PDF Slides

@inproceedings{monteiro2018bounded,
  title = {Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract)},
  author = {Monteiro, Felipe R. and Garcia, M{\'{a}}rio A. P. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  booktitle = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated Software Engineering, {ASE} 2018, Montpellier, France, September 3-7, 2018},
  pages = {954},
  year = {2018},
  publisher = {{ACM}},
  doi = {10.1145/3238147.3241981},
  editor = {Huchard, Marianne and K{\"{a}}stner, Christian and Fraser, Gordon},
  url = {https://doi.org/10.1145/3238147.3241981}
}

Counterexample guided inductive optimization based on satisfiability modulo theories

Rodrigo F. Araujo, Higo F. Albuquerque, Iury Valente Bessa, and 2 more authors

Sci. Comput. Program., 2018

DOI Bib PDF

@article{araujo2018counterexample,
  title = {Counterexample guided inductive optimization based on satisfiability modulo theories},
  author = {Araujo, Rodrigo F. and Albuquerque, Higo F. and de Bessa, Iury Valente and Cordeiro, Lucas C. and Filho, Jo{\~{a}}o Edgar Chaves},
  journal = {Sci. Comput. Program.},
  volume = {165},
  pages = {3--23},
  year = {2018},
  doi = {10.1016/j.scico.2017.10.004},
  url = {https://doi.org/10.1016/j.scico.2017.10.004}
}

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems

Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, and 1 more author

In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2018, Porto, Portugal, April 11-13, 2018, 2018

DOI Bib PDF Slides

@inproceedings{chaves2018dsvalidator,
  title = {DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems},
  author = {Chaves, Lennon C. and Bessa, Iury and Cordeiro, Lucas C. and Kroening, Daniel},
  booktitle = {Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week), {HSCC} 2018, Porto, Portugal, April 11-13, 2018},
  pages = {253--258},
  year = {2018},
  publisher = {{ACM}},
  doi = {10.1145/3178126.3178151},
  editor = {Prandini, Maria and Deshmukh, Jyotirmoy V.},
  url = {https://doi.org/10.1145/3178126.3178151}
}

DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles

Lennon C. Chaves, Iury Bessa, Hussama Ismail, and 3 more authors

IEEE Trans. Reliab., 2018

DOI Bib PDF

@article{chaves2018dsverifier,
  title = {DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles},
  author = {Chaves, Lennon C. and Bessa, Iury and Ismail, Hussama and dos Santos Frutuoso, Adriano Bruno and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {{IEEE} Trans. Reliab.},
  volume = {67},
  number = {4},
  pages = {1420--1441},
  year = {2018},
  doi = {10.1109/TR.2018.2873260},
  url = {https://doi.org/10.1109/TR.2018.2873260}
}

ASE

ESBMC 5.0: an industrial-strength C model checker

Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, and 3 more authors

In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, 2018

DOI Bib PDF Poster Slides

@inproceedings{gadelha2018esbmc,
  title = {ESBMC 5.0: an industrial-strength C model checker},
  author = {Gadelha, Mikhail Y. R. and Monteiro, Felipe R. and Morse, Jeremy and Cordeiro, Lucas C. and Fischer, Bernd and Nicole, Denis A.},
  booktitle = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated Software Engineering, {ASE} 2018, Montpellier, France, September 3-7, 2018},
  pages = {888--891},
  year = {2018},
  publisher = {{ACM}},
  doi = {10.1145/3238147.3240481},
  editor = {Huchard, Marianne and K{\"{a}}stner, Christian and Fraser, Gordon},
  url = {https://doi.org/10.1145/3238147.3240481}
}

ESBMC-GPU A context-bounded model checking tool to verify CUDA programs

Felipe R. Monteiro, Erickson H. S. Alves, Isabela Silva, and 3 more authors

Sci. Comput. Program., 2018

DOI Bib PDF

@article{monteiro2018esbmc,
  title = {ESBMC-GPU A context-bounded model checking tool to verify CUDA programs},
  author = {Monteiro, Felipe R. and da S. Alves, Erickson H. and da Silva, Isabela and Ismail, Hussama and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {Sci. Comput. Program.},
  volume = {152},
  pages = {63--69},
  year = {2018},
  doi = {10.1016/j.scico.2017.09.005},
  url = {https://doi.org/10.1016/j.scico.2017.09.005}
}

CAV

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

Lucas C. Cordeiro, Pascal Kesseli, Daniel Kroening, and 2 more authors

In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, 2018

DOI Bib PDF Slides

@inproceedings{cordeiro2018jbmc,
  title = {JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode},
  author = {Cordeiro, Lucas C. and Kesseli, Pascal and Kroening, Daniel and Schrammel, Peter and Trt{\'{\i}}k, Marek},
  booktitle = {Computer Aided Verification - 30th International Conference, {CAV} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part {I}},
  volume = {10981},
  pages = {183--190},
  year = {2018},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-96145-3_10},
  editor = {Chockler, Hana and Weissenbacher, Georg},
  url = {https://doi.org/10.1007/978-3-319-96145-3\_10}
}

TACAS

Map2Check Using LLVM and KLEE - (Competition Contribution)

Rafael Menezes, Herbert Rocha, Lucas C. Cordeiro, and 1 more author

In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, 2018

DOI Bib PDF Slides

@inproceedings{menezes2018check,
  title = {Map2Check Using LLVM and KLEE - (Competition Contribution)},
  author = {Menezes, Rafael and Rocha, Herbert and Cordeiro, Lucas C. and Barreto, Raimundo S.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, {TACAS} 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part {II}},
  volume = {10806},
  pages = {437--441},
  year = {2018},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-89963-3_28},
  editor = {Beyer, Dirk and Huisman, Marieke},
  url = {https://doi.org/10.1007/978-3-319-89963-3\_28}
}

Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants

A Abate, I.; Cattaruzza D Bessa, L Cordeiro, and 4 more authors

In 7th Workshop on Synthesis (SYNT), 2018

Bib PDF

@inproceedings{cordeiro2018safe,
  title = {Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants},
  author = {Abate, A and Bessa, I.; Cattaruzza D and Cordeiro, L and David, C and Kesseli, P and Kroening, D and Polgreen, E},
  booktitle = {7th Workshop on Synthesis (SYNT)},
  year = {2018},
}

Sim3Tanks: A Benchmark Model Simulator for Process Control and Monitoring

Arllem O. Farias, Gabriel Alisson C. Queiroz, Iury Valente Bessa, and 3 more authors

IEEE Access, 2018

DOI Bib PDF

@article{farias2018tanks,
  title = {Sim3Tanks: A Benchmark Model Simulator for Process Control and Monitoring},
  author = {Farias, Arllem O. and Queiroz, Gabriel Alisson C. and de Bessa, Iury Valente and de Medeiros, Renan Landau Paiva and Cordeiro, Lucas C. and Palhares, Reinaldo M.},
  journal = {{IEEE} Access},
  volume = {6},
  pages = {62234--62254},
  year = {2018},
  doi = {10.1109/ACCESS.2018.2874752},
  url = {https://doi.org/10.1109/ACCESS.2018.2874752}
}

FSE

Towards counterexample-guided k-induction for fast bug detection

Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, and 1 more author

In Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018, 2018

DOI Bib PDF Slides

@inproceedings{gadelha2018counterexample,
  title = {Towards counterexample-guided k-induction for fast bug detection},
  author = {Gadelha, Mikhail Y. R. and Monteiro, Felipe R. and Cordeiro, Lucas C. and Nicole, Denis A.},
  booktitle = {Proceedings of the 2018 {ACM} Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, {ESEC/SIGSOFT} {FSE} 2018, Lake Buena Vista, FL, USA, November 04-09, 2018},
  pages = {765--769},
  year = {2018},
  publisher = {{ACM}},
  doi = {10.1145/3236024.3264840},
  editor = {Leavens, Gary T. and Garcia, Alessandro and Pasareanu, Corina S.},
  url = {https://doi.org/10.1145/3236024.3264840}
}

Using clang as a Frontend on a Formal Verification Tool

M. Y. R Gadelha, J Morse, L. C Cordeiro, and 1 more author

In European LLVM Developers Meeting (EuroLLVM), 2018

Bib PDF Poster

@inproceedings{cordeiro2018clang,
  title = {Using clang as a Frontend on a Formal Verification Tool},
  author = {Gadelha, M. Y. R and Morse, J and Cordeiro, L. C and Nicole, D},
  booktitle = {European LLVM Developers Meeting (EuroLLVM)},
  year = {2018},
}

2017

A method to localize faults in concurrent C programs

Erickson H. S. Alves, Lucas C. Cordeiro, and Eddie Batista Lima Filho

J. Syst. Softw., 2017

DOI Bib

@article{alves2017method,
  title = {A method to localize faults in concurrent C programs},
  author = {da S. Alves, Erickson H. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {J. Syst. Softw.},
  volume = {132},
  pages = {336--352},
  year = {2017},
  doi = {10.1016/j.jss.2017.03.010},
  url = {https://doi.org/10.1016/j.jss.2017.03.010}
}

A Power Control and Anticolision Mechanism for RFID Systems

W. C Lucena Filho, L. C Cordeiro, W. S Silva Junior, and 1 more author

IEEE Latin America Transactions, 2017

DOI Bib

@article{cordeiro2017power,
  title = {A Power Control and Anticolision Mechanism for RFID Systems},
  author = {Lucena Filho, W. C and Cordeiro, L. C and Silva Junior, W. S and Carvalho, C. B},
  journal = {IEEE Latin America Transactions},
  volume = {15},
  number = {10},
  pages = {1933--1940},
  year = {2017},
  doi = {10.1109/TLA.2017.8071238},
}

CAV

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Alessandro Abate, Iury Bessa, Dario Cattaruzza, and 5 more authors

In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, 2017

DOI Bib PDF Slides

@inproceedings{abate2017automated,
  title = {Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants},
  author = {Abate, Alessandro and Bessa, Iury and Cattaruzza, Dario and Cordeiro, Lucas C. and David, Cristina and Kesseli, Pascal and Kroening, Daniel and Polgreen, Elizabeth},
  booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {I}},
  volume = {10426},
  pages = {462--482},
  year = {2017},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-63387-9_23},
  editor = {Majumdar, Rupak and Kuncak, Viktor},
  url = {https://doi.org/10.1007/978-3-319-63387-9\_23}
}

BMCLua: A Translator for Model Checking Lua Programs

Felipe R. Monteiro, Francisco A. P. Januário, Lucas C. Cordeiro, and 1 more author

ACM SIGSOFT Softw. Eng. Notes, 2017

DOI Bib PDF

@article{monteiro2017bmclua,
  title = {BMCLua: A Translator for Model Checking Lua Programs},
  author = {Monteiro, Felipe R. and Janu{\'{a}}rio, Francisco A. P. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {{ACM} {SIGSOFT} Softw. Eng. Notes},
  volume = {42},
  number = {3},
  pages = {1--10},
  year = {2017},
  doi = {10.1145/3127360.3127367},
  url = {https://doi.org/10.1145/3127360.3127367}
}

Bounded model checking of C++ programs based on the Qt cross-platform framework

Felipe R. Monteiro, Mário Garcia, Lucas C. Cordeiro, and 1 more author

Softw. Test. Verification Reliab., 2017

DOI Bib PDF

@article{monteiro2017bounded,
  title = {Bounded model checking of C++ programs based on the Qt cross-platform framework},
  author = {Monteiro, Felipe R. and Garcia, M{\'{a}}rio and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {Softw. Test. Verification Reliab.},
  volume = {27},
  number = {3},
  year = {2017},
  doi = {10.1002/stvr.1632},
  url = {https://doi.org/10.1002/stvr.1632}
}

Classificação Automática de Modulações Mono e Multiportadoras utilizando Método de Extração de Características e Classificadores SVM

D. A Amoedo, W. C Melo, L. C Cordeiro, and 3 more authors

In 35th Brazilian Symposium on Telecommunications and Signal Processing (SBrT), pp, 2017

Bib PDF

@inproceedings{cordeiro2017classifica,
  title = {Classificação Automática de Modulações Mono e Multiportadoras utilizando Método de Extração de Características e Classificadores SVM},
  author = {Amoedo, D. A and Melo, W. C and Cordeiro, L. C and Lima Filho, E. B and da Silva Júnior, W. S and Carvalho, C. B},
  booktitle = {35th Brazilian Symposium on Telecommunications and Signal Processing (SBrT), pp},
  year = {2017},
}

Counterexample guided inductive optimization applied to mobile robots path planning

Rodrigo F. Araujo, Alexandre Ribeiro, Iury Valente Bessa, and 2 more authors

In 2017 Latin American Robotics Symposium (LARS) and 2017 Brazilian Symposium on Robotics (SBR), Curitiba, Brazil, November 8-11, 2017, 2017

DOI Bib HTML Slides

@inproceedings{araujo2017counterexample,
  title = {Counterexample guided inductive optimization applied to mobile robots path planning},
  author = {Araujo, Rodrigo F. and Ribeiro, Alexandre and de Bessa, Iury Valente and Cordeiro, Lucas C. and Filho, Jo{\~{a}}o Edgar Chaves},
  booktitle = {2017 Latin American Robotics Symposium {(LARS)} and 2017 Brazilian Symposium on Robotics (SBR), Curitiba, Brazil, November 8-11, 2017},
  pages = {1--6},
  year = {2017},
  publisher = {{IEEE}},
  doi = {10.1109/SBR-LARS-R.2017.8215336},
  editor = {Todt, Eduardo and Tonidandel, Flavio},
  url = {https://doi.org/10.1109/SBR-LARS-R.2017.8215336}
}

ASE

DSSynth: an automated digital controller synthesis tool for physical plants

Alessandro Abate, Iury Bessa, Dario Cattaruzza, and 6 more authors

In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, 2017

DOI Bib PDF Poster Slides

@inproceedings{abate2017dssynth,
  title = {DSSynth: an automated digital controller synthesis tool for physical plants},
  author = {Abate, Alessandro and Bessa, Iury and Cattaruzza, Dario and Chaves, Lennon C. and Cordeiro, Lucas C. and David, Cristina and Kesseli, Pascal and Kroening, Daniel and Polgreen, Elizabeth},
  booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November 03, 2017},
  pages = {919--924},
  year = {2017},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ASE.2017.8115705},
  editor = {Rosu, Grigore and Penta, Massimiliano Di and Nguyen, Tien N.},
  url = {https://doi.org/10.1109/ASE.2017.8115705}
}

TACAS

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution)

Williame Rocha, Herbert Rocha, Hussama Ismail, and 2 more authors

In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, 2017

DOI Bib PDF Slides

@inproceedings{rocha2017depthk,
  title = {DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution)},
  author = {Rocha, Williame and Rocha, Herbert and Ismail, Hussama and Cordeiro, Lucas C. and Fischer, Bernd},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, {TACAS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {II}},
  volume = {10206},
  pages = {360--364},
  year = {2017},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-662-54580-5_23},
  editor = {Legay, Axel and Margaria, Tiziana},
  url = {https://doi.org/10.1007/978-3-662-54580-5\_23}
}

Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks

Mikhail Y. R. Gadelha, Lucas C. Cordeiro, and Denis A. Nicole

In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, 2017

DOI Bib PDF Slides

@inproceedings{gadelha2017encoding,
  title = {Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks},
  author = {Gadelha, Mikhail Y. R. and Cordeiro, Lucas C. and Nicole, Denis A.},
  booktitle = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium, {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},
  volume = {10623},
  pages = {91--106},
  year = {2017},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-70848-5_7},
  editor = {da Costa Cavalheiro, Simone Andr{\'{e}} and Fiadeiro, Jos{\'{e}} Luiz},
  url = {https://doi.org/10.1007/978-3-319-70848-5\_7}
}

Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty

Iury Bessa, Hussama Ismail, Reinaldo M. Palhares, and 2 more authors

IEEE Trans. Computers, 2017

DOI Bib PDF

@article{bessa2017formal,
  title = {Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty},
  author = {Bessa, Iury and Ismail, Hussama and Palhares, Reinaldo M. and Cordeiro, Lucas C. and Filho, Joao Edgar Chaves},
  journal = {{IEEE} Trans. Computers},
  volume = {66},
  number = {3},
  pages = {545--552},
  year = {2017},
  doi = {10.1109/TC.2016.2601328},
  url = {https://doi.org/10.1109/TC.2016.2601328}
}

Handling loops in bounded model checking of C programs via k-induction

Mikhail Y. R. Gadelha, Hussama Ibrahim Ismail, and Lucas C. Cordeiro

Int. J. Softw. Tools Technol. Transf., 2017

DOI Bib PDF

@article{gadelha2017handling,
  title = {Handling loops in bounded model checking of C programs via k-induction},
  author = {Gadelha, Mikhail Y. R. and Ismail, Hussama Ibrahim and Cordeiro, Lucas C.},
  journal = {Int. J. Softw. Tools Technol. Transf.},
  volume = {19},
  number = {1},
  pages = {97--114},
  year = {2017},
  doi = {10.1007/s10009-015-0407-9},
  url = {https://doi.org/10.1007/s10009-015-0407-9}
}

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, and 3 more authors

Int. J. Embed. Syst., 2017

DOI Bib PDF

@article{trindade2017multi,
  title = {Multi-core model checking and maximum satisfiability applied to hardware-software partitioning},
  author = {Trindade, Alessandro Bezerra and Degelo, Renato De Faria and Junior, Edilson Galv{\~{a}}o Dos Santos and Ismail, Hussama Ibrahim and Silva, Helder Cruz Da and Cordeiro, Lucas Carvalho},
  journal = {Int. J. Embed. Syst.},
  volume = {9},
  number = {6},
  pages = {570--582},
  year = {2017},
  doi = {10.1504/IJES.2017.10008947},
  url = {https://doi.org/10.1504/IJES.2017.10008947}
}

OptCE: A Counterexample-Guided Inductive Optimization Solver

Higo F. Albuquerque, Rodrigo F. Araujo, Iury Valente Bessa, and 2 more authors

In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, 2017

DOI Bib PDF Slides

@inproceedings{albuquerque2017optce,
  title = {OptCE: A Counterexample-Guided Inductive Optimization Solver},
  author = {Albuquerque, Higo F. and Araujo, Rodrigo F. and de Bessa, Iury Valente and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  booktitle = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium, {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},
  volume = {10623},
  pages = {125--141},
  year = {2017},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-70848-5_9},
  editor = {da Costa Cavalheiro, Simone Andr{\'{e}} and Fiadeiro, Jos{\'{e}} Luiz},
  url = {https://doi.org/10.1007/978-3-319-70848-5\_9}
}

Planning and Evaluation of UAV Mission Planner for Intralogistics Problems

Thiago Rodrigo Felix Cavalcante, Iury Valente Bessa, and Lucas Carvalho Cordeiro

In VII Brazilian Symposium on Computing Systems Engineering, SBESC 2017, Curitiba, PR, Brazil, November 6-10, 2017, 2017

DOI Bib PDF Slides

@inproceedings{cavalcante2017planning,
  title = {Planning and Evaluation of UAV Mission Planner for Intralogistics Problems},
  author = {Cavalcante, Thiago Rodrigo Felix and de Bessa, Iury Valente and Cordeiro, Lucas Carvalho},
  booktitle = {{VII} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2017, Curitiba, PR, Brazil, November 6-10, 2017},
  pages = {9--16},
  year = {2017},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2017.8},
  url = {https://doi.org/10.1109/SBESC.2017.8}
}

SMT-based context-bounded model checking for CUDA programs

Phillipe A. Pereira, Higo F. Albuquerque, Isabela Silva, and 4 more authors

Concurr. Comput. Pract. Exp., 2017

DOI Bib PDF

@article{pereira2017context,
  title = {SMT-based context-bounded model checking for CUDA programs},
  author = {Pereira, Phillipe A. and Albuquerque, Higo F. and da Silva, Isabela and Marques, Hendrio and Monteiro, Felipe R. and Ferreira, Ricardo and Cordeiro, Lucas C.},
  journal = {Concurr. Comput. Pract. Exp.},
  volume = {29},
  number = {22},
  year = {2017},
  doi = {10.1002/cpe.3934},
  url = {https://doi.org/10.1002/cpe.3934}
}

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Alessandro Abate, Iury Bessa, Dario Cattaruzza, and 4 more authors

In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017, 2017

DOI Bib PDF Slides

@inproceedings{abate2017sound,
  title = {Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants},
  author = {Abate, Alessandro and Bessa, Iury and Cattaruzza, Dario and Cordeiro, Lucas C. and David, Cristina and Kesseli, Pascal and Kroening, Daniel},
  booktitle = {Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, {HSCC} 2017, Pittsburgh, PA, USA, April 18-20, 2017},
  pages = {197--206},
  year = {2017},
  publisher = {{ACM}},
  doi = {10.1145/3049797.3049802},
  editor = {Frehse, Goran and Mitra, Sayan},
  url = {https://doi.org/10.1145/3049797.3049802}
}

Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters

Daniel P. M. Mello, Mauro L. Freitas, Lucas C. Cordeiro, and 4 more authors

CoRR, 2017

Bib PDF

@article{mello2017verification,
  title = {Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters},
  author = {de Mello, Daniel P. M. and de Freitas, Mauro L. and Cordeiro, Lucas C. and J{\'{u}}nior, Waldir S. S. and de Bessa, Iury Valente and Filho, Eddie B. L. and Clavier, Laurent},
  journal = {CoRR},
  volume = {abs/1706.05088},
  year = {2017},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1706.05088}
}

ISSTA

Verifying digital systems with MATLAB

Lennon C. Chaves, Iury Bessa, Lucas C. Cordeiro, and 2 more authors

In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10 - 14, 2017, 2017

DOI Bib PDF Poster Slides

@inproceedings{chaves2017verifying,
  title = {Verifying digital systems with MATLAB},
  author = {Chaves, Lennon C. and Bessa, Iury and Cordeiro, Lucas C. and Kroening, Daniel and de Lima Filho, Eddie Batista},
  booktitle = {Proceedings of the 26th {ACM} {SIGSOFT} International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10 - 14, 2017},
  pages = {388--391},
  year = {2017},
  publisher = {{ACM}},
  doi = {10.1145/3092703.3098228},
  editor = {Bultan, Tevfik and Sen, Koushik},
  url = {https://doi.org/10.1145/3092703.3098228}
}

2016

Applying SMT-based verification to hardware/software partitioning in embedded systems

Alessandro Trindade and Lucas C. Cordeiro

Des. Autom. Embed. Syst., 2016

DOI Bib

@article{trindade2016applying,
  title = {Applying SMT-based verification to hardware/software partitioning in embedded systems},
  author = {Trindade, Alessandro and Cordeiro, Lucas C.},
  journal = {Des. Autom. Embed. Syst.},
  volume = {20},
  number = {1},
  pages = {1--19},
  year = {2016},
  doi = {10.1007/s10617-015-9163-z},
  url = {https://doi.org/10.1007/s10617-015-9163-z}
}

Bounded model checking for fixed-point digital filters

Renato B. Abreu, Mikhail Y. R. Gadelha, Lucas C. Cordeiro, and 2 more authors

J. Braz. Comput. Soc., 2016

DOI Bib PDF

@article{abreu2016bounded,
  title = {Bounded model checking for fixed-point digital filters},
  author = {Abreu, Renato B. and Gadelha, Mikhail Y. R. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista and J{\'{u}}nior, Waldir S. S.},
  journal = {J. Braz. Comput. Soc.},
  volume = {22},
  number = {1},
  pages = {1:1--1:20},
  year = {2016},
  doi = {10.1186/s13173-016-0041-8},
  url = {https://doi.org/10.1186/s13173-016-0041-8}
}

Complementary training programme for electrical and computer engineering students through an industrial-academic collaboration

Felipe R. Monteiro, Phillipe A. Pereira, Lucas C. Cordeiro, and 2 more authors

In 2016 IEEE Frontiers in Education Conference, FIE 2015, Eire, PA, USA, October 12-15, 2016, 2016

DOI Bib PDF

@inproceedings{monteiro2016complementary,
  title = {Complementary training programme for electrical and computer engineering students through an industrial-academic collaboration},
  author = {Monteiro, Felipe R. and Pereira, Phillipe A. and Cordeiro, Lucas C. and Filho, Cicero Ferreira Fernandes Costa and Costa, Marly Guimar{\~{a}}es Fernandes},
  booktitle = {2016 {IEEE} Frontiers in Education Conference, {FIE} 2015, Eire, PA, USA, October 12-15, 2016},
  pages = {1--9},
  year = {2016},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/FIE.2016.7757421},
  url = {https://doi.org/10.1109/FIE.2016.7757421}
}

ESBMC-QtOM: A Bounded Model Checking Tool to Verify Qt Applications

Mário Garcia, Felipe R. Monteiro, Lucas C. Cordeiro, and 1 more author

In Model Checking Software - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings, 2016

DOI Bib PDF Slides

@inproceedings{garcia2016esbmcqtom,
  title = {ESBMC-QtOM: A Bounded Model Checking Tool to Verify Qt Applications},
  author = {Garcia, M{\'{a}}rio and Monteiro, Felipe R. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  booktitle = {Model Checking Software - 23rd International Symposium, {SPIN} 2016, Co-located with {ETAPS} 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings},
  volume = {9641},
  pages = {97--103},
  year = {2016},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-32582-8_6},
  editor = {Bosnacki, Dragan and Wijs, Anton},
  url = {https://doi.org/10.1007/978-3-319-32582-8\_6}
}

TACAS

Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution)

Herbert O. Rocha, Raimundo S. Barreto, and Lucas C. Cordeiro

In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, 2016

DOI Bib PDF Slides

@inproceedings{rocha2016hunting,
  title = {Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution)},
  author = {Rocha, Herbert O. and Barreto, Raimundo S. and Cordeiro, Lucas C.},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, {TACAS} 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings},
  volume = {9636},
  pages = {934--937},
  year = {2016},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-662-49674-9_64},
  editor = {Chechik, Marsha and Raskin, Jean{-}Fran{\c{c}}ois},
  url = {https://doi.org/10.1007/978-3-662-49674-9\_64}
}

SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends

Lucas C. Cordeiro and Eddie Batista Lima Filho

ACM SIGSOFT Softw. Eng. Notes, 2016

DOI Bib PDF

@article{cordeiro2016context,
  title = {SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends},
  author = {Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  journal = {{ACM} {SIGSOFT} Softw. Eng. Notes},
  volume = {41},
  number = {3},
  pages = {1--6},
  year = {2016},
  doi = {10.1145/2934240.2934247},
  url = {https://doi.org/10.1145/2934240.2934247}
}

SMT-based Verification Applied to Non-convex Optimization Problems

Rodrigo F. Araujo, Iury Bessa, Lucas Carvalho Cordeiro, and 1 more author

In VI Brazilian Symposium on Computing Systems Engineering, SBESC 2026, João Pessoa, Paraı́ba, Brazil, November 1-4, 2016, 2016

DOI Bib PDF Slides

@inproceedings{araujo2016verification,
  title = {SMT-based Verification Applied to Non-convex Optimization Problems},
  author = {Araujo, Rodrigo F. and Bessa, Iury and Cordeiro, Lucas Carvalho and Filho, Joao Edgar Chaves},
  booktitle = {{VI} Brazilian Symposium on Computing Systems Engineering, {SBESC} 2026, Jo{\~{a}}o Pessoa, Para{\'{\i}}ba, Brazil, November 1-4, 2016},
  pages = {1--8},
  year = {2016},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2016.010},
  url = {https://doi.org/10.1109/SBESC.2016.010}
}

Verification of fixed-point digital controllers using direct and delta forms realizations

Iury Valente Bessa, Hussama Ismail, Lucas C. Cordeiro, and 1 more author

Des. Autom. Embed. Syst., 2016

DOI Bib PDF

@article{bessa2016verification,
  title = {Verification of fixed-point digital controllers using direct and delta forms realizations},
  author = {de Bessa, Iury Valente and Ismail, Hussama and Cordeiro, Lucas C. and Filho, Jo{\~{a}}o Edgar Chaves},
  journal = {Des. Autom. Embed. Syst.},
  volume = {20},
  number = {2},
  pages = {95--126},
  year = {2016},
  doi = {10.1007/s10617-016-9173-5},
  url = {https://doi.org/10.1007/s10617-016-9173-5}
}

Verificação de Programas Multi-Threads Baseados no Framework Multiplataforma Qt

A. S Souza, L. C Cordeiro, and F. A. P Januário

In IV Regional Meeting of Engineering (ENCOENG), 2016

Bib PDF

@inproceedings{cordeiro2016verifica,
  title = {Verificação de Programas Multi-Threads Baseados no Framework Multiplataforma Qt},
  author = {Souza, A. S and Cordeiro, L. C and Januário, F. A. P},
  booktitle = {IV Regional Meeting of Engineering (ENCOENG)},
  pages = {131--140},
  year = {2016},
}

Verifying CUDA programs using SMT-based context-bounded model checking

Phillipe A. Pereira, Higo F. Albuquerque, Hendrio Marques, and 5 more authors

In Proceedings of the 31st Annual ACM Symposium on Applied Computing, Pisa, Italy, April 4-8, 2016, 2016

DOI Bib PDF Slides

@inproceedings{pereira2016verifying,
  title = {Verifying CUDA programs using SMT-based context-bounded model checking},
  author = {Pereira, Phillipe A. and Albuquerque, Higo F. and Marques, Hendrio and da Silva, Isabela and Carvalho, Celso B. and Cordeiro, Lucas C. and Santos, Vanessa and Ferreira, Ricardo},
  booktitle = {Proceedings of the 31st Annual {ACM} Symposium on Applied Computing, Pisa, Italy, April 4-8, 2016},
  pages = {1648--1653},
  year = {2016},
  publisher = {{ACM}},
  doi = {10.1145/2851613.2851830},
  editor = {Ossowski, Sascha},
  url = {https://doi.org/10.1145/2851613.2851830}
}

2015

Model Checking Embedded C Software Using k-Induction and Invariants

Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, and 1 more author

In 2015 Brazilian Symposium on Computing Systems Engineering, SBESC 2015, Foz do Iguacu, Brazil, November 3-6, 2015, 2015

DOI Bib PDF

@inproceedings{rocha2017model,
  title = {Model Checking Embedded C Software Using k-Induction and Invariants},
  author = {Rocha, Herbert and Ismail, Hussama and Cordeiro, Lucas C. and Barreto, Raimundo S.},
  booktitle = {2015 Brazilian Symposium on Computing Systems Engineering, {SBESC} 2015, Foz do Iguacu, Brazil, November 3-6, 2015},
  pages = {90--95},
  year = {2015},
  publisher = {{IEEE} Computer Society},
  doi = {10.1007/978-1-4614-2266-2_7},
  url = {https://doi.org/10.1109/SBESC.2015.24}
}

ICCE

Bounded model checking of C++ programs based on the Qt framework

Felipe Rodrigues Monteiro Sousa, Lucas C. Cordeiro, and Eddie Batista Lima Filho

In IEEE 4th Global Conference on Consumer Electronics, GCCE 2015, Osaka, Japan, 27-30 October 2015, 2015

DOI Bib PDF Poster

@inproceedings{sousa2015bounded,
  title = {Bounded model checking of C++ programs based on the Qt framework},
  author = {Sousa, Felipe Rodrigues Monteiro and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  booktitle = {{IEEE} 4th Global Conference on Consumer Electronics, {GCCE} 2015, Osaka, Japan, 27-30 October 2015},
  pages = {179--180},
  year = {2015},
  publisher = {{IEEE}},
  doi = {10.1109/GCCE.2015.7398699},
  url = {https://doi.org/10.1109/GCCE.2015.7398699}
}

DSVerifier: A Bounded Model Checking Tool for Digital Systems

Hussama Ismail, Iury Bessa, Lucas C. Cordeiro, and 2 more authors

In Model Checking Software - 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings, 2015

DOI Bib PDF Slides

@inproceedings{ismail2015dsverifier,
  title = {DSVerifier: A Bounded Model Checking Tool for Digital Systems},
  author = {Ismail, Hussama and Bessa, Iury and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista and Filho, Joao Edgar Chaves},
  booktitle = {Model Checking Software - 22nd International Symposium, {SPIN} 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings},
  volume = {9232},
  pages = {126--131},
  year = {2015},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-23404-5_9},
  editor = {Fischer, Bernd and Geldenhuys, Jaco},
  url = {https://doi.org/10.1007/978-3-319-23404-5\_9}
}

Fault Localization in Multi-threaded C Programs Using Bounded Model Checking

Erickson H. S. Alves, Lucas C. Cordeiro, and Eddie Batista Lima Filho

In 2015 Brazilian Symposium on Computing Systems Engineering, SBESC 2015, Foz do Iguacu, Brazil, November 3-6, 2015, 2015

DOI Bib PDF Slides

@inproceedings{alves2015fault,
  title = {Fault Localization in Multi-threaded C Programs Using Bounded Model Checking},
  author = {da S. Alves, Erickson H. and Cordeiro, Lucas C. and de Lima Filho, Eddie Batista},
  booktitle = {2015 Brazilian Symposium on Computing Systems Engineering, {SBESC} 2015, Foz do Iguacu, Brazil, November 3-6, 2015},
  pages = {96--101},
  year = {2015},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2015.25},
  url = {https://doi.org/10.1109/SBESC.2015.25}
}

ICCE

Hardware reconfiguration based on broadcasted digital TV signal

Rodrigo R. Oliveira, Lucas C. Cordeiro, and Vicente Ferreira Lucena Jr.

In IEEE International Conference on Consumer Electronics, ICCE 2015, Las Vegas, NV, USA, January 9-12, 2015, 2015

DOI Bib

@inproceedings{oliveira2015hardware,
  title = {Hardware reconfiguration based on broadcasted digital TV signal},
  author = {Oliveira, Rodrigo R. and Cordeiro, Lucas C. and de Lucena Jr., Vicente Ferreira},
  booktitle = {{IEEE} International Conference on Consumer Electronics, {ICCE} 2015, Las Vegas, NV, USA, January 9-12, 2015},
  pages = {596--598},
  year = {2015},
  publisher = {{IEEE}},
  doi = {10.1109/ICCE.2015.7066542},
  url = {https://doi.org/10.1109/ICCE.2015.7066542}
}

Memory Management Test-Case Generation of C Programs Using Bounded Model Checking

Herbert Rocha, Raimundo S. Barreto, and Lucas C. Cordeiro

In Software Engineering and Formal Methods - 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings, 2015

DOI Bib PDF Slides

@inproceedings{rocha2015memory,
  title = {Memory Management Test-Case Generation of C Programs Using Bounded Model Checking},
  author = {Rocha, Herbert and Barreto, Raimundo S. and Cordeiro, Lucas C.},
  booktitle = {Software Engineering and Formal Methods - 13th International Conference, {SEFM} 2015, York, UK, September 7-11, 2015. Proceedings},
  volume = {9276},
  pages = {251--267},
  year = {2015},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-22969-0_18},
  editor = {Calinescu, Radu and Rumpe, Bernhard},
  url = {https://doi.org/10.1007/978-3-319-22969-0\_18}
}

Model Checking Embedded C Software Using k-Induction and Invariants

Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, and 1 more author

In 2015 Brazilian Symposium on Computing Systems Engineering, SBESC 2015, Foz do Iguacu, Brazil, November 3-6, 2015, 2015

Awarded DOI Bib PDF Slides

Best Paper Award

@inproceedings{rocha2015model,
  title = {Model Checking Embedded C Software Using k-Induction and Invariants},
  author = {Rocha, Herbert and Ismail, Hussama and Cordeiro, Lucas C. and Barreto, Raimundo S.},
  booktitle = {2015 Brazilian Symposium on Computing Systems Engineering, {SBESC} 2015, Foz do Iguacu, Brazil, November 3-6, 2015},
  pages = {90--95},
  year = {2015},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2015.24},
  url = {https://doi.org/10.1109/SBESC.2015.24}
}

Model checking LTL properties over ANSI-C programs with bounded traces

Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, and 1 more author

Softw. Syst. Model., 2015

DOI Bib PDF

@article{morse2015model,
  title = {Model checking LTL properties over ANSI-C programs with bounded traces},
  author = {Morse, Jeremy and Cordeiro, Lucas C. and Nicole, Denis A. and Fischer, Bernd},
  journal = {Softw. Syst. Model.},
  volume = {14},
  number = {1},
  pages = {65--81},
  year = {2015},
  doi = {10.1007/s10270-013-0366-0},
  url = {https://doi.org/10.1007/s10270-013-0366-0}
}

Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems

Alessandro Trindade, Hussama Ismail, and Lucas C. Cordeiro

In 2015 Brazilian Symposium on Computing Systems Engineering, SBESC 2015, Foz do Iguacu, Brazil, November 3-6, 2015, 2015

DOI Bib PDF Slides

@inproceedings{trindade2015multi,
  title = {Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems},
  author = {Trindade, Alessandro and Ismail, Hussama and Cordeiro, Lucas C.},
  booktitle = {2015 Brazilian Symposium on Computing Systems Engineering, {SBESC} 2015, Foz do Iguacu, Brazil, November 3-6, 2015},
  pages = {102--105},
  year = {2015},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2015.26},
  url = {https://doi.org/10.1109/SBESC.2015.26}
}

Verificação de Kernels em Programas CUDA usando Bounded Model Checking

P. A Pereira, H Albuquerque, H Marques, and 5 more authors

In To appear in XV Brazilian Symposium on High-Performance Computing (WSCAD-SSC), pp. 24-35, 2015

Bib PDF Slides

@inproceedings{cordeiro2015verifica,
  title = {Verificação de Kernels em Programas CUDA usando Bounded Model Checking},
  author = {Pereira, P. A and Albuquerque, H and Marques, H and Silva, I and Santos, V and Carvalho, C. B and Ferreira, R. S and Cordeiro, L. C},
  booktitle = {To appear in XV Brazilian Symposium on High-Performance Computing (WSCAD-SSC), pp. 24-35},
  year = {2015},
}

Verificação de Modelos Aplicada aos Filtros Espaciais em Processamento Digital de Imagens

M. S Lima, E. S Silva, and L. C Cordeiro

In IV Regional Meeting of Computer and Information Systems (ENCOSIS), 2015

Bib PDF

@inproceedings{cordeiro2015verifica2,
  title = {Verificação de Modelos Aplicada aos Filtros Espaciais em Processamento Digital de Imagens},
  author = {Lima, M. S and Silva, E. S and Cordeiro, L. C},
  booktitle = {IV Regional Meeting of Computer and Information Systems (ENCOSIS)},
  pages = {136--145},
  year = {2015},
}

Verificação de Programas C++ Baseados no Framework Multiplataforma QT

F Rodrigues, L. C Cordeiro, and E. B Lima Filho

In IV Regional Meeting of Computer and Information Systems (ENCOSIS), 2015

Bib PDF Slides

@inproceedings{cordeiro2015verifica3,
  title = {Verificação de Programas C++ Baseados no Framework Multiplataforma QT},
  author = {Rodrigues, F and Cordeiro, L. C and Lima Filho, E. B},
  booktitle = {IV Regional Meeting of Computer and Information Systems (ENCOSIS)},
  pages = {181--190},
  year = {2015},
}

2014

ICCE

A secondary screen architecture to accurately capture viewers’ interactions in an iTV environment

Ricardo Erikson Veras De Sena Rosa, Lucas C. Cordeiro, and Vicente Ferreira Lucena Jr.

In IEEE 3rd Global Conference on Consumer Electronics, GCCE 2014, Tokyo, Japan, 7-10 October 2014, 2014

DOI Bib PDF Slides

@inproceedings{rosa2014secondary,
  title = {A secondary screen architecture to accurately capture viewers' interactions in an iTV environment},
  author = {Rosa, Ricardo Erikson Veras De Sena and Cordeiro, Lucas C. and de Lucena Jr., Vicente Ferreira},
  booktitle = {{IEEE} 3rd Global Conference on Consumer Electronics, {GCCE} 2014, Tokyo, Japan, 7-10 October 2014},
  pages = {264--265},
  year = {2014},
  publisher = {{IEEE}},
  doi = {10.1109/GCCE.2014.7031328},
  url = {https://doi.org/10.1109/GCCE.2014.7031328}
}

Aplicando Verificação de Modelos para o Particionamento de Hardware/Software

A. B Trindade and L. C Cordeiro

In 4th Brazilian Symposium on Computing Systems Engineering (SBESC), 2014

Bib PDF

@inproceedings{cordeiro2014aplicando,
  title = {Aplicando Verificação de Modelos para o Particionamento de Hardware/Software},
  author = {Trindade, A. B and Cordeiro, L. C},
  booktitle = {4th Brazilian Symposium on Computing Systems Engineering (SBESC)},
  pages = {1--6},
  year = {2014},
}

Applying symbolic bounded model checking to the 2012 RERS greybox challenge

Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, and 1 more author

Int. J. Softw. Tools Technol. Transf., 2014

DOI Bib PDF

@article{morse2014applying,
  title = {Applying symbolic bounded model checking to the 2012 RERS greybox challenge},
  author = {Morse, Jeremy and Cordeiro, Lucas C. and Nicole, Denis A. and Fischer, Bernd},
  journal = {Int. J. Softw. Tools Technol. Transf.},
  volume = {16},
  number = {5},
  pages = {519--529},
  year = {2014},
  doi = {10.1007/s10009-014-0335-0},
  url = {https://doi.org/10.1007/s10009-014-0335-0}
}

ICCE

BMCLua: Verification of Lua programs in digital TV interactive applications

Francisco A. P. Januário, Lucas C. Cordeiro, Vicente Ferreira Lucena Jr., and 1 more author

In IEEE 3rd Global Conference on Consumer Electronics, GCCE 2014, Tokyo, Japan, 7-10 October 2014, 2014

DOI Bib PDF Slides

@inproceedings{januario2014bmclua,
  title = {BMCLua: Verification of Lua programs in digital TV interactive applications},
  author = {Janu{\'{a}}rio, Francisco A. P. and Cordeiro, Lucas C. and de Lucena Jr., Vicente Ferreira and de Lima Filho, Eddie Batista},
  booktitle = {{IEEE} 3rd Global Conference on Consumer Electronics, {GCCE} 2014, Tokyo, Japan, 7-10 October 2014},
  pages = {707--708},
  year = {2014},
  publisher = {{IEEE}},
  doi = {10.1109/GCCE.2014.7031344},
  url = {https://doi.org/10.1109/GCCE.2014.7031344}
}

BMCLua: Verificação de Programas Lua em Aplicações Interativas de TV Digital

F. A. P Januario, L. C Cordeiro, and E. B. ; Lucena Jr V. F Lima Filho

In 4th Brazilian Symposium on Computing Systems Engineering (SBESC), 2014

Bib PDF

@inproceedings{cordeiro2014bmclua,
  title = {BMCLua: Verificação de Programas Lua em Aplicações Interativas de TV Digital},
  author = {Januario, F. A. P and Cordeiro, L. C and Lima Filho, E. B. ; Lucena Jr V. F},
  booktitle = {4th Brazilian Symposium on Computing Systems Engineering (SBESC)},
  pages = {1--6},
  year = {2014},
}

TACAS

ESBMC 1.22 - (Competition Contribution)

Jeremy Morse, Mikhail Ramalho, Lucas C. Cordeiro, and 2 more authors

In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, 2014

DOI Bib PDF Slides

@inproceedings{morse2014esbmc,
  title = {ESBMC 1.22 - (Competition Contribution)},
  author = {Morse, Jeremy and Ramalho, Mikhail and Cordeiro, Lucas C. and Nicole, Denis A. and Fischer, Bernd},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, {TACAS} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings},
  volume = {8413},
  pages = {405--407},
  year = {2014},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-642-54862-8_31},
  editor = {{\'{A}}brah{\'{a}}m, Erika and Havelund, Klaus},
  url = {https://doi.org/10.1007/978-3-642-54862-8\_31}
}

SMT-based bounded model checking of fixed-point digital controllers

Iury Bessa, Renato B. Abreu, João Edgar Chaves Filho, and 1 more author

In IECON 2014 - 40th Annual Conference of the IEEE Industrial Electronics Society, Dallas, TX, USA, October 29 - November 1, 2014, 2014

DOI Bib PDF Slides

@inproceedings{bessa2014bounded,
  title = {SMT-based bounded model checking of fixed-point digital controllers},
  author = {Bessa, Iury and Abreu, Renato B. and Filho, Jo{\~{a}}o Edgar Chaves and Cordeiro, Lucas C.},
  booktitle = {{IECON} 2014 - 40th Annual Conference of the {IEEE} Industrial Electronics Society, Dallas, TX, USA, October 29 - November 1, 2014},
  pages = {295--301},
  year = {2014},
  publisher = {{IEEE}},
  doi = {10.1109/IECON.2014.7048514},
  url = {https://doi.org/10.1109/IECON.2014.7048514}
}

Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking

Iury Valente Bessa, Hussama Ibrahim Ismail, Lucas Carvalho Cordeiro, and 1 more author

In 2014 Brazilian Symposium on Computing Systems Engineering, SBESC 2014, Manaus, Amazonas, Brazil, November 3-7, 2014, 2014

DOI Bib PDF

@inproceedings{bessa2014verification,
  title = {Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking},
  author = {de Bessa, Iury Valente and Ismail, Hussama Ibrahim and Cordeiro, Lucas Carvalho and Filho, Joao Edgar Chaves},
  booktitle = {2014 Brazilian Symposium on Computing Systems Engineering, {SBESC} 2014, Manaus, Amazonas, Brazil, November 3-7, 2014},
  pages = {49--54},
  year = {2014},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/SBESC.2014.14},
  url = {https://doi.org/10.1109/SBESC.2014.14}
}

2013

Dynamic and automated product derivation for consumer electronics software applications

Ricardo Erikson Veras De Sena Rosa, Vicente Ferreira Lucena Jr., Lucas C. Cordeiro, and 1 more author

IEEE Trans. Consumer Electron., 2013

DOI Bib PDF

@article{rosa2013dynamic,
  title = {Dynamic and automated product derivation for consumer electronics software applications},
  author = {Rosa, Ricardo Erikson Veras De Sena and de Lucena Jr., Vicente Ferreira and Cordeiro, Lucas C. and Filho, Joao Edgar Chaves},
  journal = {{IEEE} Trans. Consumer Electron.},
  volume = {59},
  number = {4},
  pages = {883--891},
  year = {2013},
  doi = {10.1109/TCE.2013.6689703},
  url = {https://doi.org/10.1109/TCE.2013.6689703}
}

TACAS

Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution)

Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, and 1 more author

In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, 2013

DOI Bib PDF Slides

@inproceedings{morse2013handling,
  title = {Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution)},
  author = {Morse, Jeremy and Cordeiro, Lucas C. and Nicole, Denis A. and Fischer, Bernd},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, {TACAS} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
  volume = {7795},
  pages = {619--622},
  year = {2013},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-642-36742-7_47},
  editor = {Piterman, Nir and Smolka, Scott A.},
  url = {https://doi.org/10.1007/978-3-642-36742-7\_47}
}

SMT-Based Bounded Model Checking of C++ Programs

Mikhail Ramalho, Mauro Freitas, Felipe Rodrigues Monteiro Sousa, and 3 more authors

In 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems, ECBS 2013, Scottsdale, AZ, USA, April 22-24, 2013, 2013

DOI Bib PDF Slides

@inproceedings{ramalho2013bounded,
  title = {SMT-Based Bounded Model Checking of C++ Programs},
  author = {Ramalho, Mikhail and Freitas, Mauro and Sousa, Felipe Rodrigues Monteiro and Marques, Hendrio and Cordeiro, Lucas C. and Fischer, Bernd},
  booktitle = {20th {IEEE} International Conference and Workshops on Engineering of Computer Based Systems, {ECBS} 2013, Scottsdale, AZ, USA, April 22-24, 2013},
  pages = {147--156},
  year = {2013},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ECBS.2013.15},
  editor = {Rozenblit, Jerzy W.},
  url = {https://doi.org/10.1109/ECBS.2013.15}
}

Verificação Baseada em Indução Matemática de Programas C/C++

M Ramalho, L. C Cordeiro, A Cavalcante, and 1 more author

In 3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013. 106. Silva, V. Cordeiro, L. C., Lucena Jr, V, 2013

Bib PDF

@inproceedings{cordeiro2013verifica,
  title = {Verificação Baseada em Indução Matemática de Programas C/C++},
  author = {Ramalho, M and Cordeiro, L. C and Cavalcante, A and Lucena Jr, V},
  booktitle = {3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013. 106. Silva, V. Cordeiro, L. C., Lucena Jr, V},
  year = {2013},
}

Verificação de Aplicações AmI Usando Java PathFinder

V. Cordeiro L. C Silva and V Lucena Jr

In 3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013. 107. Abreu, R., Cordeiro, L. C., Lima Filho, E, 2013

Bib PDF

@inproceedings{cordeiro2013verifica2,
  title = {Verificação de Aplicações AmI Usando Java PathFinder},
  author = {Silva, V. Cordeiro L. C and Lucena Jr, V},
  booktitle = {3rd Brazilian Symposium on Computing Systems Engineering (SBESC), 2013. 107. Abreu, R., Cordeiro, L. C., Lima Filho, E},
  year = {2013},
}

Verificação de Códigos Lua Utilizando BMCLua

F Januario, L. C Cordeiro, and E. B Lima Filho

In 31st Brazilian Symposium on Telecommunications (SBrT), 2013. 109. Freitas, M., Ramalho, M., Cordeiro, L. C., Silva Jr., W., Lima Filho, E, 2013

Bib PDF Slides

@inproceedings{cordeiro2013verifica3,
  title = {Verificação de Códigos Lua Utilizando BMCLua},
  author = {Januario, F and Cordeiro, L. C and Lima Filho, E. B},
  booktitle = {31st Brazilian Symposium on Telecommunications (SBrT), 2013. 109. Freitas, M., Ramalho, M., Cordeiro, L. C., Silva Jr., W., Lima Filho, E},
  year = {2013},
}

Verificação de Propriedades de Filtros Digitais Implementados com Aritmética de Ponto Fixo

M Freitas, M Ramalho, L. C Cordeiro, and 2 more authors

In 31st Brazilian Symposium on Telecommunications (SBrT), 2013. DOI:10.14209/sbrt.2013.226 110. Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L. C., and Fischer, B, 2013

Bib PDF Poster

@inproceedings{cordeiro2013verifica4,
  title = {Verificação de Propriedades de Filtros Digitais Implementados com Aritmética de Ponto Fixo},
  author = {Freitas, M and Ramalho, M and Cordeiro, L. C and Silva Jr, W and Lima Filho, E},
  booktitle = {31st Brazilian Symposium on Telecommunications (SBrT), 2013. DOI:10.14209/sbrt.2013.226 110. Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L. C., and Fischer, B},
  year = {2013},
}

Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking

Renato B. Abreu, Lucas C. Cordeiro, and Eddie B. L. Filho

CoRR, 2013

Bib PDF Poster

@article{abreu2013verifying,
  title = {Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking},
  author = {Abreu, Renato B. and Cordeiro, Lucas C. and Filho, Eddie B. L.},
  journal = {CoRR},
  volume = {abs/1305.2892},
  year = {2013},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1305.2892}
}

2012

A Distributed Extension of the Hybrid PRS System using Video Processing to Command a Robot via Bluetooth

M Freitas, V Valenzuela, M Gadelha, and 3 more authors

Intl. Journal of Computer Science and Network Security, 2012

Bib HTML PDF

@article{cordeiro2012distributed,
  title = {A Distributed Extension of the Hybrid PRS System using Video Processing to Command a Robot via Bluetooth},
  author = {Freitas, M and Valenzuela, V and Gadelha, M and SILVA JUNIOR, W. S and Cordeiro, L. C and LUCENA JUNIOR, V},
  journal = {Intl. Journal of Computer Science and Network Security},
  pages = {29--35},
  year = {2012},
}

A car racing based strategy for the Dynamic Voltage and Frequency Scaling technique

David Cohen, Eduardo Valentin, Raimundo S. Barreto, and 2 more authors

In 21st IEEE International Symposium on Industrial Electronics, ISIE 2012, Hangzhou, China, 28-31 May, 2012, 2012

DOI Bib Slides

@inproceedings{cohen2012racing,
  title = {A car racing based strategy for the Dynamic Voltage and Frequency Scaling technique},
  author = {Cohen, David and Valentin, Eduardo and Barreto, Raimundo S. and de Oliveira, Horacio A. B. F. and Cordeiro, Lucas C.},
  booktitle = {21st {IEEE} International Symposium on Industrial Electronics, {ISIE} 2012, Hangzhou, China, 28-31 May, 2012},
  pages = {774--779},
  year = {2012},
  publisher = {{IEEE}},
  doi = {10.1109/ISIE.2012.6237186},
  url = {https://doi.org/10.1109/ISIE.2012.6237186}
}

TACAS

Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution)

Lucas C. Cordeiro, Jeremy Morse, Denis A. Nicole, and 1 more author

In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, 2012

DOI Bib PDF Slides

@inproceedings{cordeiro2012context,
  title = {Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution)},
  author = {Cordeiro, Lucas C. and Morse, Jeremy and Nicole, Denis A. and Fischer, Bernd},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, {TACAS} 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
  volume = {7214},
  pages = {534--537},
  year = {2012},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-642-28756-5_42},
  editor = {Flanagan, Cormac and K{\"{o}}nig, Barbara},
  url = {https://doi.org/10.1007/978-3-642-28756-5\_42}
}

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

Lucas C. Cordeiro, Bernd Fischer, and João Marques-Silva

IEEE Trans. Software Eng., 2012

DOI Bib HTML PDF

@article{cordeiro2012bounded,
  title = {SMT-Based Bounded Model Checking for Embedded ANSI-C Software},
  author = {Cordeiro, Lucas C. and Fischer, Bernd and Marques{-}Silva, Jo{\~{a}}o},
  journal = {{IEEE} Trans. Software Eng.},
  volume = {38},
  number = {4},
  pages = {957--974},
  year = {2012},
  doi = {10.1109/TSE.2011.59},
  url = {https://doi.org/10.1109/TSE.2011.59}
}

Sistema de Monitoramento a Distância para Unidade de Célula a Combustível

F. S Lima, L. C Cordeiro, and R. C. R Souza

In 8th Brazilian Congress of Energy Planning (CBPE), 2012. 115. Rocha, H., Barreto, R., Cordeiro, L. C., and Dias-Neto, A, 2012

Bib PDF

@inproceedings{cordeiro2012sistema,
  title = {Sistema de Monitoramento a Distância para Unidade de Célula a Combustível},
  author = {Lima, F. S and Cordeiro, L. C and Souza, R. C. R},
  booktitle = {8th Brazilian Congress of Energy Planning (CBPE), 2012. 115. Rocha, H., Barreto, R., Cordeiro, L. C., and Dias-Neto, A},
  year = {2012},
}

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples

Herbert Rocha, Raimundo S. Barreto, Lucas C. Cordeiro, and 1 more author

In Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings, 2012

DOI Bib PDF Slides

@inproceedings{rocha2012understanding,
  title = {Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples},
  author = {Rocha, Herbert and Barreto, Raimundo S. and Cordeiro, Lucas C. and Neto, Arilo Dias},
  booktitle = {Integrated Formal Methods - 9th International Conference, {IFM} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  volume = {7321},
  pages = {128--142},
  year = {2012},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-642-30729-4_10},
  editor = {Derrick, John and Gnesi, Stefania and Latella, Diego and Treharne, Helen},
  url = {https://doi.org/10.1007/978-3-642-30729-4\_10}
}

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

Lucas C. Cordeiro, Bernd Fischer, and João Marques-Silva

IEEE Trans. Software Eng., 2012

DOI Bib PDF

@article{cordeiro2009bounded,
  title = {SMT-Based Bounded Model Checking for Embedded ANSI-C Software},
  author = {Cordeiro, Lucas C. and Fischer, Bernd and Marques{-}Silva, Jo{\~{a}}o},
  journal = {{IEEE} Trans. Software Eng.},
  volume = {38},
  number = {4},
  pages = {957--974},
  year = {2012},
  doi = {10.1109/TSE.2011.59},
  url = {https://doi.org/10.1109/TSE.2011.59}
}

2011

A Formal Method for Modeling, Verification and Synthesis of Embedded Reactive Systems

R. B Caldas, R. S Barreto, L. C Cordeiro, and 1 more author

In Proc. Intl. Conf. on Applied Computing (AC), 2011

Bib PDF

@inproceedings{cordeiro2011formal,
  title = {A Formal Method for Modeling, Verification and Synthesis of Embedded Reactive Systems},
  author = {Caldas, R. B and Barreto, R. S and Cordeiro, L. C and Campos, S},
  booktitle = {Proc. Intl. Conf. on Applied Computing (AC)},
  pages = {379--386},
  year = {2011},
}

Context-Bounded Model Checking of LTL Properties for ANSI-C Software

Jeremy Morse, Lucas C. Cordeiro, Denis A. Nicole, and 1 more author

In Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, 2011

DOI Bib PDF Slides

@inproceedings{morse2011context,
  title = {Context-Bounded Model Checking of LTL Properties for ANSI-C Software},
  author = {Morse, Jeremy and Cordeiro, Lucas C. and Nicole, Denis A. and Fischer, Bernd},
  booktitle = {Software Engineering and Formal Methods - 9th International Conference, {SEFM} 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings},
  volume = {7041},
  pages = {302--317},
  year = {2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-642-24690-6_21},
  editor = {Barthe, Gilles and Pardo, Alberto and Schneider, Gerardo},
  url = {https://doi.org/10.1007/978-3-642-24690-6\_21}
}

Gift young engineers: An extra-curricular initiative for updating computer and electrical engineering courses

Vicente Ferreira Lucena, José Pinheiro Queiroz Neto, Joao Edgar Chaves Filho, and 2 more authors

In 2011 Frontiers in Education Conference, FIE 2011, Rapid City, SD, USA, October 12-15, 2011, 2011

DOI Bib PDF

@inproceedings{lucena2011gift,
  title = {Gift young engineers: An extra-curricular initiative for updating computer and electrical engineering courses},
  author = {de Lucena, Vicente Ferreira and de Queiroz Neto, Jos{\'{e}} Pinheiro and Filho, Joao Edgar Chaves and da Silva Jr., Waldir Sabino and Cordeiro, Lucas Carvalho},
  booktitle = {2011 Frontiers in Education Conference, {FIE} 2011, Rapid City, SD, USA, October 12-15, 2011},
  pages = {S1},
  year = {2011},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/FIE.2011.6143056},
  url = {https://doi.org/10.1109/FIE.2011.6143056}
}

SMT-based bounded model checking of multi-threaded software in embedded systems

Lucas C. Cordeiro

University of Southampton, 2011

Bib PDF Slides

@phdthesis{cordeiro2011bounded,
  title = {SMT-based bounded model checking of multi-threaded software in embedded systems},
  author = {Cordeiro, Lucas C.},
  school = {University of Southampton},
  year = {2011},
  url = {http://eprints.soton.ac.uk/186011/}
}

Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker

Raimundo S. Barreto, Lucas C. Cordeiro, and Bernd Fischer

CoRR, 2011

Bib PDF Slides

@article{barreto2011verifying,
  title = {Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker},
  author = {Barreto, Raimundo S. and Cordeiro, Lucas C. and Fischer, Bernd},
  journal = {CoRR},
  volume = {abs/1106.2320},
  year = {2011},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1106.2320}
}

ICSE

Verifying multi-threaded software using smt-based context-bounded model checking

Lucas C. Cordeiro and Bernd Fischer

In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, 2011

Awarded DOI Bib PDF Slides

ACM SIGSOFT Distinguished Paper Award

@inproceedings{cordeiro2011verifying,
  title = {Verifying multi-threaded software using smt-based context-bounded model checking},
  author = {Cordeiro, Lucas C. and Fischer, Bernd},
  booktitle = {Proceedings of the 33rd International Conference on Software Engineering, {ICSE} 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011},
  pages = {331--340},
  year = {2011},
  publisher = {{ACM}},
  doi = {10.1145/1985793.1985839},
  editor = {Taylor, Richard N. and Gall, Harald C. and Medvidovic, Nenad},
  url = {https://doi.org/10.1145/1985793.1985839}
}

2010

Bounded Model Checking of Multi-threaded Software using SMT solvers

Lucas C. Cordeiro and Bernd Fischer

CoRR, 2010

Bib PDF Slides

@article{cordeiro2010bounded,
  title = {Bounded Model Checking of Multi-threaded Software using SMT solvers},
  author = {Cordeiro, Lucas C. and Fischer, Bernd},
  journal = {CoRR},
  volume = {abs/1003.3830},
  year = {2010},
  eprinttype = {arXiv},
  url = {http://arxiv.org/abs/1003.3830}
}

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking

Lucas C. Cordeiro, Bernd Fischer, and João Marques-Silva

In 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, ECBS 2010, Oxford, England, UK, 22-26 March 2010, 2010

DOI Bib PDF

@inproceedings{cordeiro2010continuous,
  title = {Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking},
  author = {Cordeiro, Lucas C. and Fischer, Bernd and Marques{-}Silva, Jo{\~{a}}o},
  booktitle = {17th {IEEE} International Conference and Workshops on the Engineering of Computer-Based Systems, {ECBS} 2010, Oxford, England, UK, 22-26 March 2010},
  pages = {160--169},
  year = {2010},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ECBS.2010.24},
  editor = {Sterritt, Roy and Eames, Brandon and Sprinkle, Jonathan},
  url = {https://doi.org/10.1109/ECBS.2010.24}
}

Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs

H Rocha, L. C Cordeiro, R. S Barreto, and 1 more author

In Proc. 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), pp.121-130, 2010. 12. Cordeiro, L. C. and Fischer, B, 2010

Bib PDF

@inproceedings{cordeiro2010exploiting,
  title = {Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs},
  author = {Rocha, H and Cordeiro, L. C and Barreto, R. S and José, Netto},
  booktitle = {Proc. 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), pp.121-130, 2010. 12. Cordeiro, L. C. and Fischer, B},
  pages = {121--130},
  year = {2010},
}

ICSE

SMT-based bounded model checking for multi-threaded software in embedded systems

Lucas C. Cordeiro

In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2, ICSE 2010, Cape Town, South Africa, 1-8 May 2010, 2010

DOI Bib PDF Slides

@inproceedings{cordeiro2010bounded2,
  title = {SMT-based bounded model checking for multi-threaded software in embedded systems},
  author = {Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 32nd {ACM/IEEE} International Conference on Software Engineering - Volume 2, {ICSE} 2010, Cape Town, South Africa, 1-8 May 2010},
  pages = {373--376},
  year = {2010},
  publisher = {{ACM}},
  doi = {10.1145/1810295.1810396},
  editor = {Kramer, Jeff and Bishop, Judith and Devanbu, Premkumar T. and Uchitel, Sebasti{\'{a}}n},
  url = {https://doi.org/10.1145/1810295.1810396}
}

2009

Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints

Lucas C. Cordeiro, Bernd Fischer, Huan Chen, and 1 more author

In International Conference on Embedded Software and Systems, ICESS ’09, Hangzhou, Zhejiang, P. R. China, May 25-27, 2009, 2009

DOI Bib PDF Slides

@inproceedings{cordeiro2009semiformal,
  title = {Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints},
  author = {Cordeiro, Lucas C. and Fischer, Bernd and Chen, Huan and Marques{-}Silva, Jo{\~{a}}o},
  booktitle = {International Conference on Embedded Software and Systems, {ICESS} '09, Hangzhou, Zhejiang, P. R. China, May 25-27, 2009},
  pages = {396--403},
  year = {2009},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ICESS.2009.82},
  editor = {Chen, Tianzhou and Serpanos, Dimitrios N. and Taha, Walid},
  url = {https://doi.org/10.1109/ICESS.2009.82}
}

2008

A Platform-Based Software Design Methodology for Embedded Control Systems: An Agile Toolkit

Lucas C. Cordeiro, Carlos Mar, Eduardo Valentin, and 4 more authors

In 15th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2008), 31 March - 4 April 2008, Belfast, Northern Ireland, 2008

DOI Bib PDF

@inproceedings{cordeiro2008platform,
  title = {A Platform-Based Software Design Methodology for Embedded Control Systems: An Agile Toolkit},
  author = {Cordeiro, Lucas C. and Mar, Carlos and Valentin, Eduardo and Cruz, Fabiano and Patrick, Daniel and Barreto, Raimundo S. and Lucena, Vicente},
  booktitle = {15th Annual {IEEE} International Conference and Workshop on Engineering of Computer Based Systems {(ECBS} 2008), 31 March - 4 April 2008, Belfast, Northern Ireland},
  pages = {408--417},
  year = {2008},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ECBS.2008.19},
  url = {https://doi.org/10.1109/ECBS.2008.19}
}

An agile development methodology applied to embedded control software under stringent hardware constraints

Lucas C. Cordeiro, Carlos Mar, Eduardo Valentin, and 4 more authors

ACM SIGSOFT Softw. Eng. Notes, 2008

DOI Bib PDF

@article{cordeiro2008agile,
  title = {An agile development methodology applied to embedded control software under stringent hardware constraints},
  author = {Cordeiro, Lucas C. and Mar, Carlos and Valentin, Eduardo and Cruz, Fabiano and Patrick, Daniel and Barreto, Raimundo S. and Lucena, Vicente},
  journal = {{ACM} {SIGSOFT} Softw. Eng. Notes},
  volume = {33},
  number = {1},
  year = {2008},
  doi = {10.1145/1344452.1344459},
  url = {https://doi.org/10.1145/1344452.1344459}
}

Mandos: A User Interaction Method in Embedded Applications for Mobile Telephony

Mauro Teófilo, Lucas C. Cordeiro, Raimundo S. Barreto, and 3 more authors

In First International Conference on Advances in Computer-Human Interaction, ACHI 2008, February 10-15, 2008, Sainte Luce, Martinique, France, 2008

DOI Bib

@inproceedings{teofilo2008mandos,
  title = {Mandos: A User Interaction Method in Embedded Applications for Mobile Telephony},
  author = {Te{\'{o}}filo, Mauro and Cordeiro, Lucas C. and Barreto, Raimundo S. and Pereira, Jos{\'{e}} Raimundo and Mardem, Ayres and Freitas, Pedro},
  booktitle = {First International Conference on Advances in Computer-Human Interaction, {ACHI} 2008, February 10-15, 2008, Sainte Luce, Martinique, France},
  pages = {271--276},
  year = {2008},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ACHI.2008.25},
  url = {https://doi.org/10.1109/ACHI.2008.25}
}

Towards a model-driven engineering approach for developing embedded hard real-time software

Fabiano Cruz, Raimundo S. Barreto, and Lucas C. Cordeiro

In Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008, 2008

Awarded DOI Bib

Best Paper Award

@inproceedings{cruz2008model,
  title = {Towards a model-driven engineering approach for developing embedded hard real-time software},
  author = {Cruz, Fabiano and Barreto, Raimundo S. and Cordeiro, Lucas C.},
  booktitle = {Proceedings of the 2008 {ACM} Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008},
  pages = {308--314},
  year = {2008},
  publisher = {{ACM}},
  doi = {10.1145/1363686.1363765},
  editor = {Wainwright, Roger L. and Haddad, Hisham},
  url = {https://doi.org/10.1145/1363686.1363765}
}

Towards a Semiformal Development Methodology for Embedded Systems

Lucas C. Cordeiro, Raimundo S. Barreto, and Meuse N. Oliveira Jr.

In ENASE 2008 - Proceedings of the 3rd International Conference on Evaluation of Novel Approaches to Software Engineering, Funchal, Madeira, Portugal, May 4-7, 2008, 2008

Bib PDF

@inproceedings{cordeiro2008semiformal,
  title = {Towards a Semiformal Development Methodology for Embedded Systems},
  author = {Cordeiro, Lucas C. and Barreto, Raimundo S. and Jr., Meuse N. Oliveira},
  booktitle = {{ENASE} 2008 - Proceedings of the 3rd International Conference on Evaluation of Novel Approaches to Software Engineering, Funchal, Madeira, Portugal, May 4-7, 2008},
  pages = {5--12},
  year = {2008},
  publisher = {{INSTICC} Press},
  editor = {Gonzalez{-}Perez, Cesar and Jablonski, Stefan}
}

ezRealtime: A Domain-Specific Modeling Tool for Embedded Hard Real-Time Software Synthesis

Fabiano Cruz, Raimundo S. Barreto, Lucas C. Cordeiro, and 1 more author

In Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008, 2008

DOI Bib PDF

@inproceedings{cruz2008ezrealtime,
  title = {ezRealtime: A Domain-Specific Modeling Tool for Embedded Hard Real-Time Software Synthesis},
  author = {Cruz, Fabiano and Barreto, Raimundo S. and Cordeiro, Lucas C. and Maciel, Paulo Romero Martins},
  booktitle = {Design, Automation and Test in Europe, {DATE} 2008, Munich, Germany, March 10-14, 2008},
  pages = {1510--1515},
  year = {2008},
  publisher = {{ACM}},
  doi = {10.1109/DATE.2008.4484888},
  editor = {Sciuto, Donatella},
  url = {https://doi.org/10.1109/DATE.2008.4484888}
}

2007

Agile Development Methodology for Embedded Systems: A Platform-Based Design Approach

Lucas C. Cordeiro, Raimundo S. Barreto, Rafael Barcelos, and 3 more authors

In 14th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2007), 26-29 March 2007, Tucson, Arizona, USA, 2007

DOI Bib PDF

@inproceedings{cordeiro2007agile,
  title = {Agile Development Methodology for Embedded Systems: A Platform-Based Design Approach},
  author = {Cordeiro, Lucas C. and Barreto, Raimundo S. and Barcelos, Rafael and Jr., Meuse N. Oliveira and Lucena, Vicente and Maciel, Paulo Romero Martins},
  booktitle = {14th Annual {IEEE} International Conference and Workshop on Engineering of Computer Based Systems {(ECBS} 2007), 26-29 March 2007, Tucson, Arizona, {USA}},
  pages = {195--202},
  year = {2007},
  publisher = {{IEEE} Computer Society},
  doi = {10.1109/ECBS.2007.16},
  url = {https://doi.org/10.1109/ECBS.2007.16}
}

Applying Scrum and Organizational Patterns to Multi Site Software Development

L. C Cordeiro, C. O Becker, and R. S Barreto

In Proc. 6th Latin American Conference on Pattern Languages of Programming (SugarLoafPlop), 2007

Bib PDF

@inproceedings{cordeiro2007applying,
  title = {Applying Scrum and Organizational Patterns to Multi Site Software Development},
  author = {Cordeiro, L. C and Becker, C. O and Barreto, R. S},
  booktitle = {Proc. 6th Latin American Conference on Pattern Languages of Programming (SugarLoafPlop)},
  pages = {46--67},
  year = {2007},
}

TXM - Uma Metodologia de Desenvolvimento de HW/SW Ágil para Sistemas Embarcados

L. C Cordeiro

Federal University of Amazonas, 2007

Bib PDF Slides

@mastersthesis{cordeiro2007metodologia,
  title = {TXM - Uma Metodologia de Desenvolvimento de HW/SW Ágil para Sistemas Embarcados},
  author = {Cordeiro, L. C},
  school = {Federal University of Amazonas},
  year = {2007},
}

TXM: an agile HW/SW development methodology for building medical devices

Lucas C. Cordeiro, Raimundo S. Barreto, Rafael Barcelos, and 3 more authors

ACM SIGSOFT Softw. Eng. Notes, 2007

DOI Bib HTML

@article{cordeiro2007agile2,
  title = {TXM: an agile HW/SW development methodology for building medical devices},
  author = {Cordeiro, Lucas C. and Barreto, Raimundo S. and Barcelos, Rafael and Jr., Meuse N. Oliveira and Lucena, Vicente and Maciel, Paulo Romero Martins},
  journal = {{ACM} {SIGSOFT} Softw. Eng. Notes},
  volume = {32},
  number = {6},
  year = {2007},
  doi = {10.1145/1317471.1317476},
  url = {https://doi.org/10.1145/1317471.1317476}
}

2005

Aplicando Padrões de Gerência de Configuração de Software em Projetos Geograficamente Distribuídos

L. C Cordeiro and D. A Louzado

In Proc. 5th Latin American Conference on Pattern Languages of Programming (SugarLoafPlop), 2005

Bib Slides

@inproceedings{cordeiro2005aplicando,
  title = {Aplicando Padrões de Gerência de Configuração de Software em Projetos Geograficamente Distribuídos},
  author = {Cordeiro, L. C and Louzado, D. A},
  booktitle = {Proc. 5th Latin American Conference on Pattern Languages of Programming (SugarLoafPlop)},
  pages = {207--221},
  year = {2005},
}

2004

Comparação entre mapas de isorresistividades elétricas aparentes do solo superficial de Manaus, a partir de séries de dados completos e estatísticos

A.C. de Melo Junior E.C. da Paz N.S. Campelo F.C.R Souza Cordeiro J.T.D. Alkmin, Carvalho L. C, and J. S A.F. Aragão

In 1st Regional Symposium of Brazilian Geophysical Society, 2004. 134. Alkmin J., de Melo Junior, A., da Paz, E., Campelo, N., Souza, F., Cordeiro, L. C., Carvalho, J., and Aragão, A, 2004

Bib PDF

@inproceedings{cordeiro2004compara,
  title = {Comparação entre mapas de isorresistividades elétricas aparentes do solo superficial de Manaus, a partir de séries de dados completos e estatísticos},
  author = {J.T.D. Alkmin, A.C. de Melo Junior E.C. da Paz N.S. Campelo F.C.R Souza Cordeiro and L. C, Carvalho and Aragão, J. S A.F.},
  booktitle = {1st Regional Symposium of Brazilian Geophysical Society, 2004. 134. Alkmin J., de Melo Junior, A., da Paz, E., Campelo, N., Souza, F., Cordeiro, L. C., Carvalho, J., and Aragão, A},
  year = {2004},
}

Developing Real-Time Applications with LEGO Mindstorms

L. C Cordeiro

2004

Bib PDF

@mastersthesis{cordeiro2004developing,
  title = {Developing Real-Time Applications with LEGO Mindstorms},
  author = {Cordeiro, L. C},
  school = {Federal University of Amazonas},
  type = {Bachelor's thesis},
  year = {2004},
}

Mapas de isorresistividades elétricas aparentes do solo superficial da cidade de Manaus

L. C Cordeiro, A.C. Melo Junior, D.S. Paz Jr, and 4 more authors

Revista Brasileira de Geociências, 2004

Bib

@article{cordeiro2004mapas,
  title = {Mapas de isorresistividades elétricas aparentes do solo superficial da cidade de Manaus},
  author = {Cordeiro, L. C and de Melo Junior, A.C. and Jr, D.S. Paz and da Paz, E.C. and Alkmin, F.C.R Souza; J.T.D. and Aragão, A.F. and Campelo, N.S.},
  journal = {Revista Brasileira de Geociências},
  year = {2004},
}

2003

Malhas de Aterramento do Sistema Elétrico da Manaus Energia: um Estudo de Caso

J.T.D. Alkmin, A.C. Melo Junior, F.C.R Souza, and 4 more authors

In Second Conf. on Technological Innovation in Energy, 2003

Bib PDF

@inproceedings{cordeiro2003malhas,
  title = {Malhas de Aterramento do Sistema Elétrico da Manaus Energia: um Estudo de Caso},
  author = {Alkmin, J.T.D. and de Melo Junior, A.C. and Souza, F.C.R and Campelo, N.S. and Cordeiro, L. C and da Paz, E.C. and Aragão, A.F.},
  booktitle = {Second Conf. on Technological Innovation in Energy},
  year = {2003},
}