
Pereira, P. A., Albuquerque, H., Marques, H., Silva, I., Carvalho, C. B., Santos, V., Ferreira, R. S., Cordeiro, L. C. Verifying CUDA Programs using SMTBased ContextBounded Model Checking. To appear in ACM Symposium on Applied Computing (SAC), Software Verification and Testing, 2016.
Gadelha, M. Y. R., Ismail, H. I., Cordeiro, L. C. Handling Loops in Bounded Model Checking of C Programs via kInduction. 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 kInduction and Invariants. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 16, 2015. (SBC Best Paper Award )
Alves, E. H. S., Cordeiro, L. C., Lima Filho, E. B. Fault Localization in MultiThreaded C Programs using Bounded Model Checking. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 16, 2015.
Trindade, A. B., Ismail, H. I., Cordeiro, L. C. MultiCore Model Checking to HardwareSoftware Partitioning in Embedded Systems. To appear in V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 14, 2015.
Rocha, H. O., Barreto, R. S., Cordeiro, L. C. Memory Management TestCase Generation of C Programs using Bounded Model Checking. In 13th International Conference on Software Engineering and Formal Methods (SEFM), LNCS 9276, pp. 251267, 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 SMTbased 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. 519529, 2014.
Bessa, I. V., Ismail, H. I., Cordeiro, L., Chaves Filho, J. E. Verification of Delta Form Realization in FixedPoint 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. SMTBased Bounded Model Checking of FixedPoint Digital Controllers. In 40th Annual Conference of the IEEE Industrial Electronics Society, pp. 295301, 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. 405407, 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 FixedPoint Digital Filters using SMTBased Bounded Model Checking. In Brazilian Symposium on Telecommunications (SBrT), 2013. [ePoster]
Ramalho, M., Lopes, M., Rodrigues, F., Marques, H., Cordeiro, L., Fischer, B. SMTBased Bounded Model Checking of C++ Programs. In Intl. Conf. and Workshops on the Engineering of ComputerBased Systems (ECBS), pp. 147156, 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. 619622, SpringerVerlag, 2013 (won the Bronze Medal in the overall ranking of the Second Intl. Competition on Software Verification). [Presentation]
Cordeiro, L., Fischer, B., and MarquesSilva, J. SMTBased Bounded Model Checking for Embedded ANSIC Software. In IEEE Transactions on Software Engineering (TSE), v. 38, pp. 957974, IEEE, 2012. [Bibtex]
Rocha, H., Barreto, R., Cordeiro, L. and DiasNeto, A. Understanding Programming Bugs in ANSIC Software Using Bounded Model Checking CounterExamples. In Intl. Conf. on Integrated Formal Methods (iFM), LNCS 7321, pp. 128142, SpringerVerlag, 2012. [Presentation]
Cordeiro, L., Morse, J., Nicole, D. and Fischer, B. ContextBounded 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. 533536, SpringerVerlag, 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 Realtime Systems (as part of the Brazilian Symp. on Computing System Engineering), pp.4652, IEEE, 2011. [Presentation]
Morse, J., Cordeiro, L., Nicole, D. and Fischer, B. ContextBounded Model Checking of LTL Properties for ANSIC Software. In Intl. Conf. on Software Engineering and Formal Methods (SEFM), LNCS 7041, pp. 302317, SpringerVerlag, 2011. [Bibtex] [Presentation]
Cordeiro, L. SMTBased Bounded Model Checking of Multithreaded Software in Embedded Systems. PhD thesis, University of Southampton, 2011.
Cordeiro, L. and Fischer, B. Verifying Multithreaded Software using SMTbased ContextBounded Model Checking. In Intl. Conf. on Software Engineering (ICSE), pp. 331340, 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. 121130, SBC, 2010. [Bibtex] [Presentation]
Cordeiro, L. and Fischer, B. Bounded Model Checking of Multithreaded Software using SMT solvers. Technical Report, Dependable Systems and Software Engineering, University of Southampton, 2010. (Presentationonly paper in 8th Intl. Workshop on Satisfiability Modulo Theories). [BibTex] [Presentation]
Cordeiro, L. SMTBased Bounded Model Checking for Multithreaded Software in Embedded Systems. In Intl. Conf. on Software Engineering (ICSE), Doctoral Symposium, pp. 373376, IEEE/ACM, 2010. [BibTex] [Presentation]
Cordeiro, L., Fischer, B. and MarquesSilva, J. Continuous Verification of Large Embedded Software using SMTBased Bounded Model Checking. In Intl. Conf. and Workshops on the Engineering of ComputerBased Systems (ECBS), pp. 160169, IEEE, 2010. [BibTex] [Presentation]
Cordeiro, L., Fischer, B. and MarquesSilva, J. SMTBased Bounded Model Checking for Embedded ANSIC Software. In Intl. Conf. on Automated Software Engineering (ASE), pp. 137148, IEEE/ACM, 2009. [BibTex] [Presentation]
Cordeiro, L., Fischer, B., Chen, H. and MarquesSilva, J. Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. In Intl. Conf. on Embedded Software and Systems (ICESS), pp. 396403, IEEE, 2009. [BibTex][Presentation] 
