Publications

[1] 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. 1-6, 2017.

[2] Chaves, C. L., Bessa, I. V., Cordeiro, L. C., Kroening, D. DSValidator: An Automated Reproducibility Tool for Digital Systems. In Technical Report published as an arXiv Document. DOI: https://arxiv.org/abs/1610.07066

[3] 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]

[4] 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] DOI: http://dx.doi.org/10.1007/978-3-319-63387-9_23

[5] 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

[6] 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

[7]  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

[8] 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

[9] 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

[10] 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

[11] 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

[12] 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

[13] 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

[14] 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