–
2020
[1] Cavalcante, T., Bessa, I., de Lima Filho, E. Cordeiro, L. Formal Non-fragile Verification of Step Response Requirements for Digital State-Feedback Control Systems.. In Journal of Control, Automation and Electrical Systems, pp. 1-21, 2020 (to appear). DOI
2019
[2] Chaves, L. C., Ismail, H. I., Bessa, I. V., Cordeiro, L. C., De Lima Filho, E. B. Verifying Fragility in Digital Systems with Uncertainties using DSVerifier v2.0. In Journal of Systems and Software, v. 153, pp. 22-43, 2019.
2018
[3] Chaves, L., Bessa, I., Ismail, H., Frutuoso, A., Cordeiro, L. C., de Lima Filho, E. B. DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles In IEEE Transactions on Reliability, v. 67(4), pp. 1420-1441, 2018.
[4] Abate, A., Bessa, I.; Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., Polgreen, E. Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants. In 7th Workshop on Synthesis (SYNT), 2018.
[5] Chaves, L. Formal Verification Applied to Attitude Control Software of Unmanned Aerial Vehicles. M.Sc. Thesis, Federal University of Amazonas, 2018.
[6] Chaves, L., Bessa, I. V., Cordeiro, L. C., Kroening, D. DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems. In 21st ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 253–258, 2018. [Presentation]
2017
[7] Abate, A., Bessa, I., Cattaruzza, D., Chaves, L., Cordeiro, L., David, C., Kesseli, P., Kroening, D., Polgreen, E. DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants. In 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 919-924, 2017. [Presentation] [Poster]
[8] Chaves, L., Bessa, I., Cordeiro, L., Kroening, D., and Lima Filho, E. Verifying Digital Systems with MATLAB. In 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pp. 388-391, 2017. [Presentation] [Poster]
[9] Abate, A., Bessa, I.; Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D., Polgreen, E. Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In 29th International Conference on Computer-Aided Verification (CAV), LNCS 10426, pp. 462-482, 2017. [Presentation] [Video] DOI: http://dx.doi.org/10.1007/978-3-319-63387-9_23
[10] Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D. Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. In 20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 197-206, 2017. [Presentation] DOI: http://dx.doi.org/10.1145/3049797.3049802
[11] Bessa, I. V., Ismail, H. I., Palhares, R., Cordeiro, L. C., Chaves Filho, J. E. Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty. In IEEE Transactions on Computers, 66(3): pp. 545-552, 2017. DOI: http://dx.doi.org/10.1109/TC.2016.2601328
2016
[12] Monteiro, F. R. Bounded Model Checking of State-Space Digital Systems: The Impact of Finite Word-Length Effects on the Implementation of Fixed-Point Digital Controllers Based on State-Space Modeling. In ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 1151-1153, 2016. DOI: http://dx.doi.org/10.1145/2950290.2983979
[13] 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.20(1), pp. 1-20, Springer, 2016. DOI: http://dx.doi.org/10.1186/s13173-016-0041-8
[14] 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(2), pp. 95-126, Springer, 2016. DOI: http://dx.doi.org/10.1007/s10617-016-9173-5
2015
[15] Ismail, H. I., Bessa, I. V., Cordeiro, L. C., Chaves Filho, J. E., Lima Filho, E. B. DSVerifier: A Bounded Model Checking Tool for Digital Systems. In 22nd International SPIN Symposium on Model Checking of Software (SPIN), LNCS 9232, pp. 126-131, 2015 [Presentation] [Demonstration] DOI: http://dx.doi.org/10.1007/978-3-319-23404-5_9
2014
[16] Bessa, I. V., Ibrahim, H., Cordeiro, L., Chaves Filho, J. E. Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking. In IV Brazilian Symposium on Computing System Engineering (SBESC), pp. 49-54, 2014. DOI: http://dx.doi.org/10.1109/SBESC.2014.14
[17] 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 (IECON), pp. 295-301, 2014. [Presentation] DOI: http://dx.doi.org/10.1109/IECON.2014.7048514
2013
[18] Abreu, R., Cordeiro, L., Lima Filho, E. Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking. In 31st Brazilian Symposium on Telecommunications (SBrT), 2013. DOI: http://dx.doi.org/10.14209/sbrt.2013.57
[19] Freitas, M., Ramalho, M., Cordeiro, L. C., Silva Jr., W., Lima Filho, E. Verificação de Propriedades de Filtros Digitais Implementados com Aritmética de Ponto Fixo. In 31st Brazilian Symposium on Telecommunications (SBrT), 2013. DOI: http://dx.doi.org/10.14209/sbrt.2013.226