An Efficient SMT-based Bounded Model Checker.
Documentation
News
Publications
SV-COMP
Test-Comp
People
Applications
Download Archive
Third Party Contributions
Index of /benchmarks
Acknowledgments
Monteiro, F., Gadelha, M., Cordeiro, L. Model Checking C++ Programs. In Software Testing, Verification and Reliability, v32(1), pp. 1-30, 2022. DOI
Aljaafari, F., Menezes, R., Manino, E., Shmarov, F., Mustafa, M., Cordeiro, L. Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs. In IEEE Access, v.10, pp.1-20, 2022. DOI
Song, K., Matulevicius, N., de Lima Filho, E., Cordeiro, L. C. ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts. In 44th International Conference on Software Engineering (ICSE 2022), pp. 65-69, 2022.
Monteiro, F., Gadelha, M., Cordeiro, L. C. Summary of Model Checking C++ Programs. In 15th IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 461, 2022.
Menezes, R., Moura, D., Cavalcante, H., de Freitas, H., Cordeiro, L. C. ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 777-780, 2022.
Brausse, F., Shmarov, F., Menezes, R., Gadelha, M., Korovin, K., Reger, G., Cordeiro, L. C. ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 773-776, 2022.
Alshmrany, K., Bhayat, A., Brausse, F., Cordeiro, L., Korovin, K., Melham, T., Mustafa, M., Olivier, P., Reger, G., Shmarov, F. Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. In IEEE Secure Development Conference, 2022 (to appear) [Presentation]
.Alshmrany, K., Aldughaim, M., Bhayat, A., Cordeiro, L. FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing (Competition Contribution). In 24th International Conference on Fundamental Approaches to Software Engineering (FASE), LNCS 13241, pp. 336-340, 2022. [Presentation]
Alshmrany, K., Menezes, R., Gadelha, M., Cordeiro, L. FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution). In 24th International Conference on Fundamental Approaches to Software Engineering (FASE), LNCS 12649, pp. 363-367, 2021.[Presentation] [Video]
Alshmrany, K., Aldughaim, M, Bhayat, A., Cordeiro, L. FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs. In 15th International Conference on Tests and Proofs (TAP), LNCS 12740, pp. 85-105, 2021.
Cordeiro, L. Exploiting the SAT Revolution for Automated Software Verification: Report from an Industrial Case Study. In 10th Latin-American Symposium on Dependable Computing (LADC), pp. 1-2, 2021. [Video]
Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole. An Efficient Floating-Point Bit-Blasting API for Verifying C Programs. 13th International Workshop on Numerical Software Verification (NSV), LNCS 12549, pp. 178-195, 2020.
Gadelha, M., Menezes, R., Monteiro, F., Cordeiro, L., Nicole, D. ESBMC: Scalable and Precise Test-Case Generation based on the Floating-Point Theory (Competition Contribution). In 23rd International Conference on Fundamental Approaches to Software Engineering (FASE), LNCS 12076, pp. 525-529, 2020.
Gadelha, M. Scalable and Precise Verification based on k-induction, Symbolic Execution and Floating-Point Theory. PhD thesis, University of Southampton, 2019.
Gadelha, M., Monteiro, F. R., Cordeiro, L., Nicole, D. ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference. In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 11429, pp. 209-213, 2019.
Breytenbach, J. Design and Evaluation of a Formula Cache for SMT-based Bounded Model Checking Tools. MSc thesis, University of Stellenbosch, 2018.
Gadelha, M., Monteiro, F. R., Cordeiro, L., Nicole, D. Towards Counterexample-Guided k-Induction for Fast Bug Detection. In 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 765-769, 2018.
Monteiro, F. R., Garcia, M. A. P., Cordeiro, L. C., de Lima Filho, E. B. Bounded Model Checking of C++ Programs Based on the Qt Cross-Platform Framework (Journal-First Abstract). In 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 954, 2018. [Demo] and [Website].
Gadelha, M., Monteiro, F. R., Morse, J., Cordeiro, L., Fischer, B., Nicole, D. ESBMC 5.0: An Industrial-Strength C Model Checker. In 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 888-891, 2018. [Poster] [Demo].
Gadelha, M. Y. R., Morse, J., Cordeiro, L. C., Nicole, D. Using clang as a Frontend on a Formal Verification Tool. In European LLVM Developers Meeting (EuroLLVM), 2018. [Poster] [Talk].
Gadelha, M. Y. R., Cordeiro, L. C., Nicole, D. Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks. In 20th Brazilian Symposium on Formal Methods (SBMF), LNCS 10623, pp. 91-106, 2017. The final publication is available at Springer via DOI. [Presentation]
Alves, E. H. S., Cordeiro, L. C., Lima Filho, E. B. A method to localize faults in concurrent C programs. In Journal of Software and Systems, v.132, pp. 336-352, 2017. The final publication is available at Elsevier via DOI.
Monteiro, F. R., Garcia, M. A. P., Cordeiro, L. C., Lima Filho, E. B. Bounded Model Checking of C++ Programs based on the Qt Cross-Platform Framework. In Software Testing, Verification and Reliability, v.27(3), pp. 1-24, 2017. The final publication is available at John Whiley via DOI.
Gadelha, M. Y. R., Ismail, H. I., Cordeiro, L. C. Handling Loops in Bounded Model Checking of C Programs via k-Induction. In International Journal on Software Tools for Technology Transfer, v.19(1), pp. 97-114, 2017. The final publication is available at Springer via DOI.
Bessa, I. V., Ismail, H. I., Palhares, R. M., Cordeiro, L. C., Chaves Filho, J. E. Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty. In IEEE Transactions on Computers, v.66, n.3, pp. 545-552, 2017. The final publication is available at IEEE Explore via DOI.
Pereira, P. , Albuquerque, H., Silva, I., Marques, H., Monteiro, F. R., Ferreira, R. S., Cordeiro, L. C. SMT-Based Context-Bounded Model Checking for CUDA Programs. In Concurrency and Computation: Practice and Experience, v.29 (22), pp. 1-20, 2017. The final publication is available at John Wiley via DOI.
Trindade, A. B., Degelo, R. F., dos Santos, E. G., Ismail, H. I., da Silva, H. C., Cordeiro, L. C. Multi-Core Model Checking and Maximum Satisfiability Applied to Hardware-Software Partitioning. In International Journal of Embedded Systems, Inderscience, v.9(6), pp. 570--582, 2017.
Cordeiro, L. C. and Lima Filho, E. B. SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends.. In Software Engineering Notes, v.41, n.3, pp. 1-6, 2016. The final publication is available at ACM Digital Library via DOI.
Abreu, R. B., Gadelha, M. Y. R., Cordeiro, L. C. ; Lima Filho, E. B., Silva Jr., W. S. Bounded Model Checking for Fixed-Point Digital Filters.. In Journal of The Brazilian Computer Society, v.22, n.1, pp. 1-20, 2016. The final publication is available at Springer via DOI.
Bessa, I. V., Ismail, H. I., Cordeiro, L. C., Chaves Filho, J. E. Verification of fixed-point digital controllers using direct and delta forms realizations.. In Design Automation for Embedded Systems, v. 20, n. 2, pp. 95-126, 2016. The final publication is available at Springer via DOI.
Garcia, M. A. P., Monteiro, F. R., Cordeiro, L. C., Lima Filho, E. B. ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications. In 23rd International SPIN symposium on Model Checking of Software (SPIN), LNCS 9641, pp. 97-103, 2016.
Rocha, H. O., Cordeiro L. C., Barreto, R. S. Hunting Memory Bugs in C Programs with Map2Check (Competition Contribution). In 22th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 9636, pp. 934-937, 2016.
Pereira, P. A., Albuquerque, H., Marques, H., Silva, I., Carvalho, C. B., Santos, V., Ferreira, R. S., Cordeiro, L. C. Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking. To appear in the ACM Symposium on Applied Computing (SAC), Software Verification and Testing, 2016.
Rocha, H., Ismail, H. I., Cordeiro, L. C., Barreto, R. S. Model Checking Embedded C Software using k-Induction and Invariants. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 90-95, 2015. (SBC Best Paper Award)
Alves, E. H. S., Cordeiro, L. C., Lima Filho, E. B. Fault Localization in Multi-Threaded C Programs using Bounded Model Checking. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 96-101, 2015.
Trindade, A. B., Ismail, H. I., Cordeiro, L. C. Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 102-105, 2015.
Rocha, H. O., Barreto, R. S., Cordeiro, L. C. Memory Management Test-Case Generation of C Programs using Bounded Model Checking. In 13th International Conference on Software Engineering and Formal Methods (SEFM), LNCS 9276, pp. 251-267, 2015.
Morse, J. Expressive and efficient bounded model checking of concurrent software. PhD thesis, University of Southampton, 2015.
Trindade, A. B. and Cordeiro, L. C. Applying SMT-based Verification to Hardware/Software Partitioning in Embedded Systems. In Design Automation for Embedded Systems, Springer, 2015.
Rocha, H., Ismail, H., Cordeiro, L., Barreto, R. Model Checking C Programs with Loops via k -Induction and Invariants. Technical Report, Federal University of Amazonas, February 9th 2015.
Morse, J., Cordeiro, L. C., Nicole, D., Fischer, B. Applying Symbolic Bounded Model Checking to the 2012 RERS Greybox Challenge. In International Journal on Software Tools for Technology Transfer (Print), v. 16, pp. 519-529, 2014.
Bessa, I. V., Ismail, H. I., Cordeiro, L., Chaves Filho, J. E. Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking. To appear in the IV Brazilian Symposium on Computing System Engineering (SBESC), 2014 (ranked within the top 5 papers with highest score according to technical program committee).
Bessa, I., Abreu, R., Filho, J. E., Cordeiro, L. SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers. In 40th Annual Conference of the IEEE Industrial Electronics Society, pp. 295-301, 2014. [Presentation]
Morse, J., Ramalho, M., Cordeiro, L., Nicole, D. and Fischer, B. ESBMC 1.22 (Competition Contribution) . In 20th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), v. 8413, pp. 405-407, 2014. (won the Gold Medal in the SequentializedConcurrent category of the Third Intl. Competition on Software Verification).
Morse, J, Cordeiro, L., Nicole, D., Fischer, B. Model Checking LTL Properties over C Programs with Bounded Traces. In Journal of Software and Systems Modeling, Springer, v. 13, pp. 366, 2013.
Abreu, R., Cordeiro, L., Lima Filho, E. Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking. In Brazilian Symposium on Telecommunications (SBrT), 2013. [e-Poster]
Ramalho, M., Lopes, M., Monteiro, F. R., Marques, H., Cordeiro, L., Fischer, B. SMT-Based Bounded Model Checking of C++ Programs. In Intl. Conf. and Workshops on the Engineering of Computer-Based Systems (ECBS), pp. 147-156, IEEE, 2013. [Presentation]
Morse, J., Cordeiro, L., Nicole, D. and Fischer, B. Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) . In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 7795, pp. 619-622, 2013 (won the Bronze Medal in the overall ranking of the Second Intl. Competition on Software Verification). [Presentation]
Cordeiro, L., Fischer, B., and Marques-Silva, J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In IEEE Transactions on Software Engineering (TSE), v. 38, pp. 957-974, IEEE, 2012.
Rocha, H., Barreto, R., Cordeiro, L. and Dias-Neto, A. Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. In Intl. Conf. on Integrated Formal Methods (iFM), LNCS 7321, pp. 128-142, 2012. [Presentation]
Cordeiro, L., Morse, J., Nicole, D. and Fischer, B. Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution) . In Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 7214., pp. 533-536, Springer-Verlag, 2012 (won the Bronze Medal in the overall ranking of the First Intl. Competition on Software Verification). [Presentation]
Barreto, R., Cordeiro, L. and Fischer, B. Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker. In 8th Brazilian Workshop on Real-time Systems (as part of the Brazilian Symp. on Computing System Engineering), pp.46-52, IEEE, 2011. [Presentation]
Morse, J., Cordeiro, L., Nicole, D. and Fischer, B. Context-Bounded Model Checking of LTL Properties for ANSI-C Software. In Intl. Conf. on Software Engineering and Formal Methods (SEFM), LNCS 7041, pp. 302-317, 2011. [Presentation]
Cordeiro, L. SMT-Based Bounded Model Checking of Multi-threaded Software in Embedded Systems. PhD thesis, University of Southampton, 2011.
Cordeiro, L. and Fischer, B. Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. In Intl. Conf. on Software Engineering (ICSE), pp. 331-340, IEEE/ACM, 2011. (ACM SIGSOFT Distinguished Paper Award ) [Presentation ]
Rocha, H., Cordeiro, L., Barreto, R. and Netto, J. Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs. In 4th Brazilian Workshop on Systematic and Automated Software Testing, pp. 121-130, SBC, 2010. [Presentation]
Cordeiro, L. and Fischer, B. Bounded Model Checking of Multi-threaded Software using SMT solvers. Technical Report, Dependable Systems and Software Engineering, University of Southampton, 2010. (Presentation-only paper in 8th Intl. Workshop on Satisfiability Modulo Theories). [Presentation]
Cordeiro, L. SMT-Based Bounded Model Checking for Multi-threaded Software in Embedded Systems. In Intl. Conf. on Software Engineering (ICSE), Doctoral Symposium, pp. 373-376, IEEE/ACM, 2010.
Cordeiro, L., Fischer, B. and Marques-Silva, J. Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. In Intl. Conf. and Workshops on the Engineering of Computer-Based Systems (ECBS), pp. 160-169, IEEE, 2010.
Cordeiro, L., Fischer, B. and Marques-Silva, J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In Intl. Conf. on Automated Software Engineering (ASE), pp. 137-148, IEEE/ACM, 2009. [Presentation]
Cordeiro, L., Fischer, B., Chen, H. and Marques-Silva, J. Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. In Intl. Conf. on Embedded Software and Systems (ICESS), pp. 396-403, IEEE, 2009. [Presentation]