
Gadelha, M., Monteiro, F., Morse, J., Cordeiro, L., Fischer, B., Nicole, D. ESBMC 5.0: An IndustrialStrength C Model Checker. In 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE). [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 floatingpoints using the SMT theory in ESBMC: An empirical evaluation over the SVCOMP benchmarks. In 20th Brazilian Symposium on Formal Methods (SBMF), LNCS 10623, pp. 91106, 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. 336352, 2017. The final publication is available at Elsevier via DOI.
Sousa, F. R. M., Garcia, M. A. P., Cordeiro, L. C., Lima Filho, E. B. Bounded Model Checking of C++ Programs based on the Qt CrossPlatform Framework. In Software Testing, Verification and Reliability, v.27(3), pp. 124, 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 kInduction. In International Journal on Software Tools for Technology Transfer, v.19(1), pp. 97114, 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 NonFragile Stability Verification of Digital Control Systems with Uncertainty. In IEEE Transactions on Computers, v.66, n.3, pp. 545552, 2017. The final publication is available at IEEE Explore via DOI.
Pereira, P. , Albuquerque, H., Silva, I., Marques, H., Rodrigues, F., Ferreira, R. S., Cordeiro, L. C. SMTBased ContextBounded Model Checking for CUDA Programs. In Concurrency and Computation: Practice and Experience (to appear), 2016. 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. MultiCore Model Checking and Maximum Satisfiability Applied to HardwareSoftware Partitioning. In International Journal of Embedded Systems (to appear), Inderscience, 2016.
Cordeiro, L. C. and Lima Filho, E. B. SMTBased ContextBounded Model Checking for Embedded Systems: Challenges and Future Trends.. In Software Engineering Notes, v.41, n.3, pp. 16, 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 FixedPoint Digital Filters.. In Journal of The Brazilian Computer Society, v.22, n.1, pp. 120, 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 fixedpoint digital controllers using direct and delta forms realizations.. In Design Automation for Embedded Systems, v. 20, n. 2, pp. 95126, 2016. The final publication is available at Springer via DOI.
Garcia, M. A. P., Sousa, F. R. M., 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. 97103, 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. 934937, 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 SMTBased ContextBounded 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 kInduction and Invariants. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 9095, 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. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 96101, 2015.
Trindade, A. B., Ismail, H. I., Cordeiro, L. C. MultiCore Model Checking to HardwareSoftware Partitioning in Embedded Systems. In V Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 102105, 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] 
