NEW! 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 ACM Symposium on Applied Computing (SAC), Software Verification and Testing, 2016.

NEW! 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, 2015. The final publication is available at Springer via DOI.

Rocha, H., Ismail, H. I., Cordeiro, L. C., Barreto, R. S. Model Checking Embedded C Software using k-Induction and Invariants. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 1-6, 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. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 1-6, 2015.

Trindade, A. B., Ismail, H. I., Cordeiro, L. C. Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 1-4, 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). [Presentation]

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).

Cordeiro, L. Model Checking Embedded Systems. Invited Talk, Institute of Industrial Automation and Software Engineering (IAS), University of Stuttgart, Stuttgart, Germany, October 2013.

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., Rodrigues, F., 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, Springer-Verlag, 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. [Bibtex]

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, Springer-Verlag, 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, Springer-Verlag, 2011. [Bibtex] [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 ) . [Bibtex] [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. [Bibtex] [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). [BibTex] [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. [BibTex] [Presentation]

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. [BibTex] [Presentation]

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. [BibTex] [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. [BibTex][Presentation]