Publications

  1. 2019
  2. Accepted/In press

    Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants

    Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D. & Polgreen, E., 18 Oct 2019, (Accepted/In press) In : Acta Informatica.

    Research output: Contribution to journalArticle

  3. Accepted/In press

    Ontology Extraction for Large Ontologies via Modularity and Forgetting

    Chen, J., Alghamdi, G., Schmidt, R., Walther, D. & Gao, Y., 21 Sep 2019, (Accepted/In press) International Conference on Knowledge Capture (K-CAP) .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Accepted/In press

    Incremental Bounded Model Checking of Artificial Neural Networks in CUDA

    Sena, L. H., Bessa, I. V., Gadelha, M. R., Cordeiro, L. & Mota, E., 19 Sep 2019, (Accepted/In press) IX Brazilian Symposium on Computing Systems Engineering.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Published

    The Fluted Fragment Revisited

    Pratt-Hartmann, I., Swast, W. & Tendera, L., 16 Sep 2019, In : The Journal of Symbolic Logic. p. 1020-1048 29 p.

    Research output: Contribution to journalArticle

  6. Published

    A CDCL-Style Calculus for Solving Non-linear Constraints

    Franz Brausse, Korovin, K., Margarita Korovina & Norbert Mueller, Sep 2019, Frontiers of Combining Systems, 12th International Symposium: FroCoS 2019, Proceedings. Herzig, A. & Popescu, A. (eds.). Springer Nature, Vol. 11715. p. 131-148 18 p. (LNCS; vol. 11715).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  7. Accepted/In press

    Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification

    Alhawi, O., Mustafa, M. A. & Cordeiro, L., 26 Aug 2019, (Accepted/In press) IEEE International Workshop on Secure Internet of Things (SIoT) .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  8. Published

    Old or Heavy? Decaying Gracefully with Age/Weight Shapes.

    Rawson, M. & Reger, G., 20 Aug 2019, Automated Deduction – CADE 27. (Lecture Notes in Computer Science; vol. 11716).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  9. Published

    The Fluted Fragment with Transitivity

    Pratt-Hartmann, I. & Tendera, L., 20 Aug 2019, p. 18:1-18:15. 15 p.

    Research output: Contribution to conferencePaper

  10. Accepted/In press

    Boost the Impact of Continuous Formal Verification in Industry

    Monteiro, F. R., Gadelha, M. Y. R. & Cordeiro, L., 15 Aug 2019, (Accepted/In press) 10th Workshop on Tools for Automatic Program Analysis .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  11. Accepted/In press

    Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX

    Banach, R., Razavi, J., Debicki, O. & Lesecq, S., 12 Aug 2019, (Accepted/In press) Lecture Notes in Computer Science : Formal Methods.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  12. E-pub ahead of print

    A Survey on Automated Symbolic Verification and its Application for Synthesizing Cyber-Physical Systems

    Cordeiro, L., de Lima Filho, E. B. & Bessa, I., 5 Aug 2019, In : IET Cyber-Physical Systems: Theory & Applications .

    Research output: Contribution to journalArticle

  13. E-pub ahead of print

    Punishment not Reward: Disincentivising Blockchain Application Misbehaviour

    Banach, R., 1 Jul 2019, IEEE International Conference on Blockchain and Cryptocurrency.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  14. Published

    SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

    Gadelha, M. Y. R., Steffinlongo, E., Cordeiro, L., Fischer, B. & Nicole, D. A., 25 May 2019, 41st ACM/IEEE International Conference on Software Engineering .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  15. Accepted/In press

    Restricted Combinatory Unification

    Bhayat, A. & Reger, G., 19 Apr 2019, (Accepted/In press) Automated Deduction – CADE 27. (Lecture Notes in Computer Science; vol. 11716).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  16. Published

    International Competition on Runtime Verification (CRV)

    Bartocci, E., Falcone, Y. & Reger, G., 4 Apr 2019, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings. Steffen, B., Kordon, F., Beyer, D. & Huisman, M. (eds.). Springer Nature, p. 41-49 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11429 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  17. Published

    JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)

    Cordeiro, L., Kroening, D. & Schrammel, P., 4 Apr 2019, International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  18. Published

    VyPR2: A framework for runtime verification of python web services

    Dawes, J. H., Reger, G., Franzoni, G., Pfeiffer, A. & Govi, G., 3 Apr 2019, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Vojnar, T. & Zhang, L. (eds.). Springer Nature, p. 98-114 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11428 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  19. Published

    Blocking and Other Enhancements for Bottom-Up ModelGeneration Methods

    Baumgartner, P. & Schmidt, R., 1 Mar 2019, In : Journal of Automated Reasoning.

    Research output: Contribution to journalArticle

  20. Accepted/In press

    A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms

    Razavi, J. & Schalk, A., 1 Feb 2019, (Accepted/In press) Electronic Proceedings in Theoretical Computer Science.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  21. Accepted/In press

    Verication-Led Smart Contracts

    Banach, R., 30 Jan 2019, (Accepted/In press) 3rd Workshop on Trusted Smart Contracts.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  22. Accepted/In press

    Coloured graphlet profiles as a predictor of career length in scientific co-authorship networks

    Blanthorn, O. & Navarro Lopez, E., 14 Jan 2019, (Accepted/In press) 4th World Conference on Complex Systems: Emergence, Self-organization, Nonlinear Dynamics and Complexity. IEEE, p. 1 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  23. Published

    A Neurally-Guided, Parallel Theorem Prover

    Rawson, M. & Reger, G., 2019, FroCoS 2019: Frontiers of Combining Systems. (Lecture Notes in Computer Science ; vol. 11715).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  24. Published

    ABox Abduction via Forgetting in ALC

    Del-Pinto, W. & Schmidt, R., 2019, Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  25. Published

    Automated Formal Verification of Stand-alone Solar Photovoltaic Systems

    Trindade, A. B. & Cordeiro, L., 2019, In : Solar Energy.

    Research output: Contribution to journalArticle

  26. Published

    Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools

    Zohar, Y., Tishkovsky, D., Schmidt, R. A. & Zamansky, A., 2019, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Nature, p. 610-638 29 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11560 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  27. Published

    Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP)

    Cordeiro, L., Kroening, D. & Schrammel, P., 2019, In : ACM SigSoft Software Engineering Notes .

    Research output: Contribution to journalArticle

  28. Published

    ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference

    Gadelha, M. Y. R., Monteiro, F. R., Cordeiro, L. & Nicole, D., 2019, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  29. Published

    Extending Forgetting-Based Abduction Using Nominals

    Del-Pinto, W. & Schmidt, R., 2019, Frontiers of Combining Systems: FroCoS 2019. Springer Nature, (Lecture Notes in Computer Science; vol. 11715).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  30. Published

    FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions

    Zhao, Y. & Schmidt, R., 2019, Automated Deduction: CADE-27. Fontaine, P. (ed.). Springer Nature, Vol. 11716. (Lecture Notes in Computer Science; vol. 11716).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  31. Published

    Induction in Saturation-Based Proof Search

    Reger, G. & Voronkov, A., 2019, Automated Deduction – CADE 27 . (Lecture Notes in Computer Science; vol. 11716).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  32. Published

    INSPEX: Optimize Range Sensors for Environment Perception as a Portable System

    Foucault, J., Lesecq, S., Dudnik, G., Correvon, M., O’keeffe, R., Di Palma, V., Passoni, M., Quaglia, F., Ouvry, L., Buckley, S., Herveg, J., Di Matteo, A., Rakotovao, T., Debicki, O., Mareau, N., Barrett, J., Rea, S., Mcgibney, A., Birot, F., De Chaumont, H. & 3 others, Banach, R., Razavi, J. & Ó’murchú, C., 2019, In : Sensors. 19, 19, p. 4350

    Research output: Contribution to journalArticle

  33. Published

    Specification of temporal properties of functions for runtime verification

    Dawes, J. H. & Reger, G., 2019, p. 2206-2214. 9 p.

    Research output: Contribution to conferencePaper

  34. Published

    Symmetry Avoidance in MACE-Style Finite Model Finding

    Reger, G., Riener, M. & Suda, M., 2019, Frontiers of Combining Systems: 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings. ( Lecture Notes in Computer Science; vol. 11715).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  35. Published

    Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach

    Zhao, Y., Alghamdi, G., Schmidt, R., Feng, H., Stoilos, G., Juric, D. & Khodadadi, M., 2019, Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019). AAAI Press

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  36. Published

    Verifying Fragility in Digital Systems with Uncertainties using DSVerier v2:0

    Chaves, L. C., Ismail, H. I., Bessa, I. V., Cordeiro, L. & de Lima Filho, E. B., 2019, In : The Journal of Systems and Software.

    Research output: Contribution to journalArticle

  37. 2018
  38. Accepted/In press

    Exploring Applications of Formal Methods in the INSPEX Project

    Razavi, J., Banach, R., Debicki, O., Mareau, N., Lesecq, S. & Foucault, J., 12 Nov 2018, (Accepted/In press) STAFF-18 Workshops post proceedings. (Lecture Notes in Computer Science ).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  39. Published

    Counterexample guided inductive optimization based on satisfiability modulo theories

    Araújo, R. F., Albuquerque, H. F., De Bessa, I. V., Cordeiro, L. C. & Chaves Filho, J. E., 1 Nov 2018, In : Science of Computer Programming. 165, p. 3-23 20 p.

    Research output: Contribution to journalArticle

  40. Published

    DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles

    Chaves, L., Bessa, I., Ismail, H., Frutuoso, A., Cordeiro, L. & de Lima Filho, E. B., 24 Oct 2018, In : IEEE Transactions on Reliability. 67, 4, p. 1420-1441

    Research output: Contribution to journalArticle

  41. Accepted/In press

    A Simple Hybrid Event-B Model of an Active Control System for Earthquake Protection

    Banach, R. & Baugh, J., 16 Oct 2018, (Accepted/In press) Astrophysics to Unconventional Computing : Essays presented to Susan Stepney on the occasion of her 60th birthday. (Emergence, Complexity and Computation).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  42. Published

    Finite Satisfiability for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

    Pratt-Hartmann, I., 3 Aug 2018, In : Mathematical Logic Quarterly. 64, 3, p. 218–248 31 p.

    Research output: Contribution to journalArticle

  43. Accepted/In press

    Bounded Model Checking of C++ Programs Based on the Qt Cross-Platform Framework (Journal-First Abstract)

    Monteiro, F. R., Cordeiro, L., Garcia, M. A. P. & de Lima Filho, E. B., 3 Jul 2018, (Accepted/In press).

    Research output: Contribution to conferenceAbstract

  44. Accepted/In press

    Formal Methods in Systems Integration: Deployment of Formal Techniques in INSPEX

    Banach, R., Razavi, J., Lesecq, S., Debicki, O., Mareau, N., Foucault, J., Correvon, M. & Dudnik, G., 28 Jun 2018, (Accepted/In press) Complex Systems Design and Management 2018 .

    Research output: Chapter in Book/Report/Conference proceedingChapter

  45. Accepted/In press

    Application of Formal Methods in the INSPEX Smart Systems Integration Project

    Banach, R., Razavi, J., Debicki, O., Mareau, N., Lesecq, S. & Foucault, J., 18 May 2018, (Accepted/In press) FMIS 2018.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  46. Published

    Modelling, Formal Refinement and Partitioning Strategies for a Small Aircraft Fuel Pump System in Hybrid Event-B

    Banach, R., 1 May 2018, In : Science of Computer Programming. 156, p. 21-44

    Research output: Contribution to journalArticle

  47. Published

    Cyberphysical Systems: A Behind-the-Scenes Foundational View

    Banach, R. & Su, W., 29 Mar 2018, College Publications Tribute Series. Mashkoor, A., Thalheim, B. & Wang, Q. (eds.). College Publications, Vol. 34. p. 177-201 (Dieter Schewe Festschrift, Tribute Series ).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  48. Published

    ESBMC-GPU A context-bounded model checking tool to verify CUDA programs

    Monteiro, F. R., Da S. Alves, E. H., Silva, I. S., Ismail, H. I., Cordeiro, L. C. & De Lima Filho, E. B., 15 Jan 2018, In : Science of Computer Programming. 152, p. 63-69 6 p.

    Research output: Contribution to journalArticle

  49. Published

    A Taxonomy for Classifying Runtime Verification Tools

    Falcone, Y., Krstic, S., Reger, G. & Traytel, D., 2018, The 18th International Conference on Runtime Verification. p. 241-262 21 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  50. Published

    An abstraction-refinement framework for reasoning with large theories.

    Lopez Hernandez, J. C. & Korovin, K., 2018, p. 663. 679 p.

    Research output: Contribution to conferencePaper

  51. Published

    Approximated Stability Analysis of Bi-Modal Hybrid Co-simulation Scenarios

    Gomes, C., Karalis, P., Navarro Lopez, E. & Vangheluwe, H., 2018. 15 p.

    Research output: Contribution to conferencePaper

  52. Published

    Assistive Smart, Structured 3D Environmental Information for the Visually Impaired and Blind: Leveraging the INSPEX Concept

    Banach, R., Razavi, J. & et al, 2018, 1st International Workshop on Biomedical & Health Engineering and Data Analysis (BEDA'18).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  53. Published

    COST action IC1402 runtime verification beyond monitoring

    Colombo, C., Falcone, Y., Leucker, M., Reger, G., Sanchez, C., Schneider, G. & Stolz, V., 2018, Runtime Verification- 18th International Conference, RV 2018, Proceedings. Leucker, M. & Colombo, C. (eds.). Springer Nature, p. 18-26 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11237).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  54. Published

    ESBMC 5.0: An industrial-strength C model checker

    Ramalho, M., Monteiro, F. R., Morse, J., Cordeiro, L., Fischer, B. & Nicole, D., 2018, 33rd IEEE/ACM International Conference on Automated Software Engineering .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  55. Published

    FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics

    Zhao, Y. & Schmidt, R., 2018, Automated Reasoning (IJCAR 2018). Cham: Springer Nature, Vol. 10900. p. 19-27 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  56. Published

    Formal Verification for Advanced Sensing Applications: Data Pre-processing in the INSPEX System

    Razavi, J., Banach, R., Lesecq, S., Debicki, O., Mareau, N., Foucault, J., Correvon, M. & Dudnik, G., 2018, Proceedings of the 13th International Conference on Software Technologies. Vol. 1.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  57. Published

    From Parametric Trace Slicing to Rule Systems

    Reger, G. & Rydeheard, D., 2018, The 18th International Conference on Runtime Verification.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  58. Published

    Issues in Automated Urban Train Control: ‘Tackling’ the Rugby Club Problem

    Banach, R., 2018, Proceedings of the 6th International ABZ Conference 2018. p. 171-186 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  59. Published

    JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

    Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P. & Trtik, M., 2018, 30th International Conference on Computer Aided Verification .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  60. Published

    Map2Check Using LLVM and KLEE

    Menezes, R., Rocha, H., Cordeiro, L. & Barreto, R., 2018, TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II. Vol. 10806. p. 437-441 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  61. Published

    On Concept Forgetting in Description Logics with Qualified Number Restrictions

    Zhao, Y. & Schmidt, R., 2018, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. p. 1984-1990 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  62. Published

    Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

    Beyersdorff, O., Blinkhorn, J., Leroy Chew, Schmidt, R. & Suda, M., 2018, In : Journal of Automated Reasoning. 27 p.

    Research output: Contribution to journalArticle

  63. Published

    Sim3Tanks: A Benchmark Model Simulator for Process Control and Monitoring

    Farias, A. O., Queiroz, G. A. C., Bessa, I. V., Medeiros, R. L. P., Cordeiro, L. & Palhares, R., 2018, In : IEEE Access.

    Research output: Contribution to journalArticle

  64. Published

    Towards Counterexample-guided k-Induction for Fast Bug Detection

    Gadelha, M. Y. R., Monteiro, F. R., Cordeiro, L. & Nicole, D. A., 2018, 25th ACM SIGSOFT International Symposium on the Foundations of Software Engineering.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  65. Published

    Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning

    Reger, G., Voronkov, A. & Suda, M., 2018, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer Nature, 17 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  66. 2017
  67. Published

    Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting

    Pratt-Hartmann, I. & Kourtis, G., 30 Oct 2017, In : Logical Methods in Computer Science. 13, 4, p. 1-39 39 p., 4.

    Research output: Contribution to journalArticle

  68. Published

    A method to localize faults in concurrent C programs

    S. Alves, E. H. D., Cordeiro, L. C. & L. Filho, E. B. D., 1 Oct 2017, In : The Journal of Systems and Software. 132, p. 336-352

    Research output: Contribution to journalArticle

  69. Published

    A Single Pyramidal-Cell and Network Computational Model of the Hippocampal CA3 Region

    Celikok, U., Navarro Lopez, E. & Sengor, N. S., 15 Jul 2017, 26th Annual Computational Neuroscience Meeting, CNS2017, (July 15–20, 2017, Antwerp, Belgium).. 1 ed. Vol. 1. 3 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  70. Published

    Set of Support for Theory Reasoning

    Reger, G. & Suda, M., 4 Jun 2017, 12th International Workshop on the Implementation of Logics .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  71. Published

    Bounded model checking of C plus plus programs based on the Qt cross-platform framework

    Monteiro, F. R., Garcia, M. A. P., Cordeiro, L. C. & de Lima Filho, E. B., May 2017, In : Software Testing, Verification and Reliability. 27, 3

    Research output: Contribution to journalArticle

  72. Published

    Handling loops in bounded model checking of C programs via k-induction

    Gadelha, M. Y. R., Ismail, H. I. & Cordeiro, L. C., 1 Feb 2017, In : International Journal on Software Tools for Technology Transfer. 19, 1, p. 97-114

    Research output: Contribution to journalArticle

  73. Accepted/In press

    Verifying Digital Systems with MATLAB

    Chaves, L., Bessa, I., Cordeiro, L., Kroening, D. & Lima, E., Feb 2017, (Accepted/In press) 26th ACM SIGSOFT International Symposium on Software Testing and Analysis .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  74. Published

    Instantiation and pretending to be an SMT solver with VAMPIRE

    Reger, G., Suda, M. & Voronkov, A., 1 Jan 2017, In : CEUR Workshop Proceedings. 1889

    Research output: Contribution to journalConference article

  75. Published

    Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

    Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D. & Polgreen, E., 2017, COMPUTER AIDED VERIFICATION, CAV 2017, PT I. Vol. 10426. p. 462-482 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  76. Published

    Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

    Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P., Kroening, D. & Polgreen, E., 2017, In : Lecture Notes in Computer Science.

    Research output: Contribution to journalArticle

  77. Published
  78. Published

    Bounded model checking of C++ programs based on the Qt cross-platform framework: BMC of C++ Programs based on Qt Cross-Platform Framework

    Monteiro, F. R., Garcia, M. A. P., Cordeiro, L. C. & De Lima Filho, E. B., 2017, In : Software Testing, Verification and Reliability. 27, 3, p. e1632

    Research output: Contribution to journalArticle

  79. Published

    Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning

    Araujo, R. F., Ribeiro, A., Bessa, I. V., Cordeiro, L. C. & Filho, J. E. C., 2017

    Research output: Other contribution

  80. Published

    DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs

    Rocha, W., Rocha, H., Ismail, H., Cordeiro, L. & Fischer, B., 2017, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, PT II. Vol. 10206. p. 360-364 4 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  81. Published

    DSSynth: An automated digital controller synthesis tool for physical plants

    Abate, A., Bessa, I., Cattaruzza, D., Chaves, L., Cordeiro, L., David, C., Kesseli, P., Kroening, D. & Polgreen, E., 2017, 32nd IEEE/ACM International Conference on Automated Software Engineering . p. 919-924

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  82. Published

    Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks

    Gadelha, M. Y. R., Cordeiro, L. C. & Nicole, D. A., 2017, Brazilian Symposium on Formal Methods. p. 91-106 Chapter 7. (Formal Methods: Foundations and Applications; vol. 10623).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  83. Published

    Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty

    Bessa, I., Ismail, H., Palhares, R., Cordeiro, L. & Filho, J. E. C., 2017, In : IEEE Transactions on Computers. 66, 3, p. 545-552

    Research output: Contribution to journalArticle

  84. Published

    Multi-core model checking and maximum satisfiability applied to hardware-software partitioning

    Trindade, A. B., Degelo, R. D. F., Galvao Dos Santos Junior, E., Ismail, H. I., Silva, H. C. D. & Cordeiro, L. C., 2017, In : International Journal of Embedded Systems. 9, 6, p. 570

    Research output: Contribution to journalArticle

  85. Published

    OptCE: A Counterexample-Guided Inductive Optimization Solver

    Albuquerque, H. F., Araújo, R. F., Bessa, I. V., Cordeiro, L. C. & De Lima Filho, E. B., 2017, Brazilian Symposium on Formal Methods. p. 125-141 16 p. (Formal Methods: Foundations and Applications; vol. 10623).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  86. Published

    Planning and Evaluation of UAV Mission Planner for Intralogistics Problems

    Cavalcante, T. R. F., Bessa, I. V. D. & Cordeiro, L. C., 2017, 2017 VII Brazilian Symposium on Computing Systems Engineering (SBESC). p. 9-16 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  87. Published

    Role Forgetting for ALCOQH(O)-Ontologies Using an Ackermann-Based Approach

    Zhao, Y. & Schmidt, R., 2017, The 26th International Joint Conference on Artificial Intelligence . Sierra, C. (ed.). International Joint Conferences on Artificial Intelligence, p. 1354-1361 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  88. Published

    Rule Refinement for Semantic Tableau Calculi

    Tishkovsky, D. & Schmidt, R., 2017, Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017 : proceedings . Schmidt, R. A. & Nalon, C. (eds.). Springer Nature, Vol. 10501. p. 228-244 (Lecture Notes in Artificial Intelligence Series ; vol. 10501).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  89. Published

    Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

    Abate, A., Bessa, I., Cattaruzza, D., Cordeiro, L., David, C., Kesseli, P. & Kroening, D., 2017, 20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). p. 197-206

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  90. Published

    Testing a Saturation-Based Theorem Prover: Experiences and Challenges

    Reger, G., Suda, M. & Voronkov, A., 2017, 11th International Conference on Tests & Proofs .

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  91. 2016
  92. Published

    Verification of fixed-point digital controllers using direct and delta forms realizations

    Bessa, I. V., Ismail, H. I., Cordeiro, L. C. & Filho, J. E. C., 10 Mar 2016, In : Design Automation for Embedded Systems. 20, 2, p. 95-126

    Research output: Contribution to journalArticle

  93. Published

    Selecting the selection

    Hoder, K., Reger, G., Suda, M. & Voronkov, A., 1 Jan 2016, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Olivetti, N. & Tiwari, A. (eds.). Springer Nature, p. 313-329 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9706).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  94. Published

    Complementary Training Programme for Electrical and Computer Engineering Students Through an Industrial-Academic Collaboration

    Monteiro, F. R., Pereira, P. A., Cordeiro, L. C., Costa Filho, C. F. F. & Costa, M. G. F., 2016, In : Frontiers in Education Conference. Conference Proceedings .

    Research output: Contribution to journalArticle

  95. Published

    Hunting Memory Bugs in C Programs with Map2Check

    Rocha, H. O., Barreto, R. S. & Cordeiro, L. C., 2016, Algorithms for the Construction and Analysis of Systems ( TACAS 2016). Vol. 9636. p. 934-937 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  96. Published

    SMT-based context-bounded model checking for CUDA programs

    Pereira, P., Albuquerque, H., Da silva, I., Marques, H., Monteiro, F., Ferreira, R. & Cordeiro, L., 2016, In : Concurrency and Computation: Practice and Experience. 29, 22

    Research output: Contribution to journalArticle

  97. Published

    SMT-based Verification Applied to Non-convex Optimization Problems

    Araujo, R., Bessa, I., Cordeiro, L. C. & Chaves Filho, J. E., 2016, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 1-8

    Research output: Contribution to journalArticle

  98. 2015
  99. Published

    Playing with AVATAR

    Reger, G., Suda, M. & Voronkov, A., 1 Aug 2015, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Felty, A. & Middeldorp, A. (eds.). Springer Nature, p. 399-415 17 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  100. Published

    Applying SMT-based verification to hardware/software partitioning in embedded systems

    Trindade, A. B. & Cordeiro, L. C., 22 Apr 2015, In : Design Automation for Embedded Systems. 20, 1, p. 1-19

    Research output: Contribution to journalArticle

  101. Published

    Model checking LTL properties over ANSI-C programs with bounded traces

    Morse, J., Cordeiro, L., Nicole, D. & Fischer, B., Feb 2015, In : Software and Systems Modeling . 14, 1, p. 65-81

    Research output: Contribution to journalArticle

  102. Published

    Automata-based Pattern Mining from Imperfect Traces

    Reger, G., Barringer, H. & Rydeheard, D., Jan 2015, ACM SIGSOFT Software Engineering Notes. USA: Association for Computing Machinery, p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  103. Published

    Applying multi-core model checking to hardware-software partitioning in embedded systems

    Trindade, A., Ismail, H. & Cordeiro, L., 2015, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 102-105

    Research output: Contribution to journalArticle

  104. Published

    Bounded Model Checking of C plus plus Programs Based on the Qt Framework

    Sousa, F. R. M., Cordeiro, L. C. & de Lima Filho, E. B., 2015

    Research output: Other contribution

  105. Published

    DSVerifier: A Bounded Model Checking Tool for Digital Systems

    Ismail, H. I., Bessa, I. V., Cordeiro, L. C., de Lima Filho, E. B. & Chaves Filho, J. E., 2015, MODEL CHECKING SOFTWARE, SPIN 2015. Vol. 9232. p. 126-131 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  106. Published

    Fault Localization in Multi-Threaded C Programs using Bounded Model Checking

    Alves, E. H. D. S., Cordeiro, L. C. & de Lima Filho, E. B., 2015, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 96-101

    Research output: Contribution to journalArticle

  107. Published

    Hardware Reconfiguration Based on Broadcasted Digital TV Signal

    Oliveira, R. R., Cordeiro, L. C. & de Lucena, V. F. . J., 2015, In : IEEE International Symposium on Consumer Electronics Proceedings. p. 596-598

    Research output: Contribution to journalArticle

  108. Published

    Memory Management Test-Case Generation of C Programs Using Bounded Model Checking

    Rocha, H., Barreto, R. & Cordeiro, L., 2015, SOFTWARE ENGINEERING AND FORMAL METHODS. Vol. 9276. p. 251-267 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  109. Published

    Model Checking Embedded C Software using k-Induction and Invariants

    Rocha, H., Ismail, H., Cordeiro, L. & Barreto, R., 2015, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 90-95

    Research output: Contribution to journalArticle

  110. 2014
  111. Published

    Uniform Interpolation and Forgetting for ALC Ontologies with ABoxes - Long Version

    Koopmann, P. & Schmidt, R. A., 20 Nov 2014, No publisher name.

    Research output: Book/ReportCommissioned report

  112. Published

    Applying symbolic bounded model checking to the 2012 RERS greybox challenge

    Morse, J., Cordeiro, L., Nicole, D. & Fischer, B., Oct 2014, In : International Journal on Software Tools for Technology Transfer. 16, 5, p. 519-529

    Research output: Contribution to journalArticle

  113. Published

    A Secondary Screen Architecture to Accurately Capture Viewers' Interactions in an iTV Environment

    Rosa, R. E. V. D. S., Cordeiro, L. C. & de Lucena Junior, V. F., 2014, 2 p.

    Research output: Other contribution

  114. Published

    BMCLua: Verification of Lua Programs in Digital TV Interactive Applications

    Januario, F. A. P., Cordeiro, L. C., de Lucena, V. F. . J. & de Lima Filho, E. B., 2014, 2 p.

    Research output: Other contribution

  115. Published

    SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers

    Bessa, I., Abreu, R., Edgar Filho, J. & Cordeiro, L., 2014, In : IEEE Industrial Electronics Society. Annual Conference. Proceedings . p. 295-301

    Research output: Contribution to journalArticle

  116. Published

    Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking

    Bessa, I., Ibrahim, H., Cordeiro, L. & Chaves Filho, J. E., 2014, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 49-54 6 p.

    Research output: Contribution to journalArticle

  117. 2013
  118. Published

    Forgetting concept and role symbols in ALCH-ontologies

    Koopmann, P. & Schmidt, R. A., Dec 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. McMillan, K., Middeldorp, A. & Voronkov, A. (eds.). Springer Nature, Vol. 8312. p. 552-567 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  119. Published

    Dynamic and automated product derivation for consumer electronics software applications

    Rosa, R. E. V. D. S., de Lucena, V. F. . J., Cordeiro, L. C. & Chaves Filho, J. E., Nov 2013, In : IIEEE Transactions on Consumer Electronics . 59, 4, p. 883-891 9 p.

    Research output: Contribution to journalArticle

  120. Published

    A pattern-based approach to parametric specification mining

    Reger, G., Barringer, H. & Rydeheard, D., 2013, 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings|IEEE/ACM Int. Conf. Autom. Softw. Eng., ASE - Proc.. IEEE, p. 658-663 5 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  121. Published

    A Tutorial on Runtime Verification

    Reger, G., Falcone, Y. & Havelund, K., 2013, Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. NATO Science for Peace and Security Series - D: Information and Communication Security: IOS Press, Vol. 34.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  122. Published

    Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution)

    Morse, J., Cordeiro, L., Nicole, D. & Fischer, B., 2013, Tools and algorithms for the construction and analysis of systems, TACAS 2013. Vol. 7795. p. 619-622 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  123. Published

    SMT-Based Bounded Model Checking of C plus plus Programs

    Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L. & Fischer, B., 2013

    Research output: Other contribution

  124. Published

    Uniform interpolation of ALC-ontologies using fixpoints

    Koopmann, P. & Schmidt, R. A., 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Springer Nature, Vol. 8152. p. 87-102 15 p. (Lecture Notes in Artificial Intelligence).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  125. Published

    Uniform Interpolation of ALC-Ontologies Using Fixpoints

    Koopmann, P., Fontaine, P. (ed.), Ringeissen, C. (ed.) & Schmidt, R. A. (ed.), 2013, Frontiers of Combining Systems. Fontaine, P., Ringeissen, C. & Schmidt, R. A. (eds.). Springer Nature, p. 87-102 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  126. 2012
  127. Published

    A Car Racing Based Strategy for the Dynamic Voltage and Frequency Scaling Technique

    Cohen, D., Valentin, E., Barreto, R., Oliveira, H. & Cordeiro, L., 2012

    Research output: Other contribution

  128. Published

    Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution)

    Cordeiro, L., Morse, J., Nicole, D. & Fischer, B., 2012, In : Lecture Notes in Computer Science. 7214, p. 534-537

    Research output: Contribution to journalArticle

  129. Published

    Quantified event automata: Towards expressive and efficient runtime monitors

    Barringer, H., Falcone, Y., Havelund, K., Reger, G. & Rydeheard, D., 2012, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 7436. p. 68-84 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  130. Published

    SMT-Based Bounded Model Checking for Embedded ANSI-C Software

    Cordeiro, L., Fischer, B. & Marques-Silva, J., 2012, In : IEEE Transactions on Software Engineering. 38, 4, p. 957-974 18 p.

    Research output: Contribution to journalArticle

  131. 2011
  132. Published

    Context-Bounded Model Checking of LTL Properties for ANSI-C Software

    Morse, J., Cordeiro, L., Nicole, D. & Fischer, B., 2011, SOFTWARE ENGINEERING AND FORMAL METHODS. Vol. 7041. p. 302 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  133. Published

    Gift Young Engineers: An Extra-Curricular Initiative for Updating Computer and Electrical Engineering Courses

    de Lucena Junior, V. F., de Queiroz Neto, J. P., Chaves Filho, J. E., da Silva Junior, W. S. & Cordeiro, L. C., 2011, In : Frontiers in Education Conference. Conference Proceedings . 6 p.

    Research output: Contribution to journalArticle

  134. Published

    Verifying Embedded C Software with Timing Constraints using an Untimed Bounded Model Checker

    Barreto, R., Cordeiro, L. & Fischer, B., 2011, In : Brazilian Symposium on Computing System Engineering : proceedings. p. 46-52 7 p.

    Research output: Contribution to journalArticle

  135. Published
  136. 2009
  137. Published

    Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints

    Cordeiro, L., Fischer, B., Chen, H. & Marques-Silva, J., 2009, 2009 INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  138. 2008
  139. Published

    A platform-based software design methodology for embedded control systems: An agile toolkit

    Cordeiro, L., Mar, C., Valentin, E., Cruz, F., Patrick, D., Barreto, R. & Lucena, V., 2008, FIFTEENTH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS. p. 408-417 10 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  140. Published

    ezRealtime: A Domain-Specific Modeling tool for Embedded Hard Real-Time software synthesis

    Cruz, F., Barreto, R., Cordeiro, L. & Maciel, P., 2008, 2008 DESIGN, AUTOMATION AND TEST IN EUROPE, VOLS 1-3. p. 1314-1319 5 p. (Design Automation and Test in Europe Conference and Expo).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  141. Published

    Towards a Model-Driven Engineering Approach for Developing Embedded Hard Real-Time Software

    Cruz, F., Barreto, R., Cordeiro, L. & Maciel, P., 2008, Applied Computing, 2008.. Vol. 1-3. p. 308-314

    Research output: Chapter in Book/Report/Conference proceedingChapter

  142. Published

    Towards a semiformal development methodology for embedded systems

    Cordeiro, L., Barreto, R. & Oliveira, M., 2008, ENASE 2008: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING. p. 5-12 7 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  143. 2007
  144. Published

    Agile development methodology for embedded systems: A platform-based design approach

    Cordeiro, L., Barreto, R., Barcelos, R., Oliveira, M., Lucena, V. & Maciel, P., 2007, ECBS 2007: 14TH ANNUAL IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS. p. 195-202

    Research output: Chapter in Book/Report/Conference proceedingChapter

Return to faculty and school overview