Lucas C. Cordeiro

Orcid: 0000-0002-6235-4272

Affiliations:
  • University of Manchester, UK
  • University of Oxford, UK (former)
  • Federal University of Amazonas (UFAM), Brazil (former)
  • University of Southampton, UK (former)


According to our database1, Lucas C. Cordeiro authored at least 164 papers between 2007 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Counterexample Guided Neural Network Quantization Refinement.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., April, 2024

Revolutionizing Cyber Threat Detection With Large Language Models: A Privacy-Preserving BERT-Based Lightweight Model for IoT/IIoT Devices.
IEEE Access, 2024

ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023
Towards global neural network abstractions with locally-exact reconstruction.
Neural Networks, August, 2023

A fuzzing-based test-creation approach for evaluating digital TV receivers via transport streams.
Softw. Test. Verification Reliab., 2023

ESBMC v7.4: Harnessing the Power of Intervals.
CoRR, 2023

Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking.
CoRR, 2023

NeuroCodeBench: a plain C neural network benchmark for software verification.
CoRR, 2023

SecureFalcon: The Next Cyber Reasoning System for Cyber Security.
CoRR, 2023

A Privacy-Preserving and Accountable Billing Protocol for Peer-to-Peer Energy Trading Markets.
CoRR, 2023

Revolutionizing Cyber Threat Detection with Large Language Models.
CoRR, 2023

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification.
CoRR, 2023

JBMC: A Bounded Model Checking Tool for Java Bytecode.
CoRR, 2023

LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution).
CoRR, 2023

Edge Learning for 6G-Enabled Internet of Things: A Comprehensive Survey of Vulnerabilities, Datasets, and Defenses.
IEEE Commun. Surv. Tutorials, 2023

EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

QNNRepair: Quantized Neural Network Repair.
Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

ESBMC v7.3: Model Checking C++ Programs Using Clang AST.
Proceedings of the Formal Methods: Foundations and Applications - 26th Brazilian Symposium, 2023

Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration.
Proceedings of the XIII Brazilian Symposium on Computing Systems Engineering, 2023

The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification.
Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering, 2023

AIREPAIR: A Repair Platform for Neural Networks.
Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023

Evaluation of Ginga's CC-Web-Service Module.
Proceedings of the International Conference on Consumer Electronics - Taiwan, 2023

Poisoning Attacks in Federated Edge Learning for Digital Twin 6G-Enabled IoTs: An Anticipatory Study.
Proceedings of the IEEE International Conference on Communications, 2023

FuSeBMC_IA: Interval Analysis and Methods for Test Case Generation - (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2023

Interventional Probing in High Dimensions: An NLI Case Study.
Proceedings of the Findings of the Association for Computational Linguistics: EACL 2023, 2023

2022
Model checking C++ programs.
Softw. Test. Verification Reliab., 2022

Montague semantics and modifier consistency measurement in neural language models.
CoRR, 2022

FuSeBMC v4: Improving code coverage with smart seeds via fuzzing and static analysis.
CoRR, 2022

Privacy-Friendly Peer-to-Peer Energy Trading: A Game Theoretical Approach.
CoRR, 2022

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs.
IEEE Access, 2022

Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities.
Proceedings of the IEEE Secure Development Conference, 2022

ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation.
Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022

ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC.
Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022

Summary of Model Checking C++ Programs.
Proceedings of the 15th IEEE Conference on Software Testing, Verification and Validation, 2022

ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts.
Proceedings of the 44th IEEE/ACM International Conference on Software Engineering: Companion Proceedings, 2022

FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing - (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2022

CEG4N: Counter-Example Guided Neural Network Quantization Refinement.
Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

Systematicity, Compositionality and Transitivity of Deep NLP Models: a Metamorphic Testing Perspective.
Proceedings of the Findings of the Association for Computational Linguistics: ACL 2022, 2022

EnnCore: End-to-End Conceptual Guarding of Neural Architectures.
Proceedings of the Workshop on Artificial Intelligence Safety 2022 (SafeAI 2022) co-located with the Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI2022), 2022

2021
ESBMC 6.1: automated test case generation using bounded model checking.
Int. J. Softw. Tools Technol. Transf., 2021

Verification and refutation of C programs based on k-induction and invariant inference.
Int. J. Softw. Tools Technol. Transf., 2021

FuSeBMC v.4: Smart Seed Generation for Hybrid Fuzzing.
CoRR, 2021

QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking.
CoRR, 2021

Verifying Quantized Neural Networks using SMT-Based Model Checking.
CoRR, 2021

EBF: A Hybrid Verification Tool for Finding Software Vulnerabilities in IoT Cryptographic Protocols.
CoRR, 2021

Verifying Security Vulnerabilities in Large Software Systems using Multi-Core k-Induction.
CoRR, 2021

FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs.
Proceedings of the Tests and Proofs - 15th International Conference, 2021

Verifying Security Vulnerabilities for Blockchain-based Smart Contracts.
Proceedings of the XI Brazilian Symposium on Computing Systems Engineering, 2021

Assisted Counterexample-Guided Inductive Optimization for Robot Path Planning.
Proceedings of the XI Brazilian Symposium on Computing Systems Engineering, 2021

Exploiting the SAT Revolution for Automated Software Verification: Report from an Industrial Case Study.
Proceedings of the 10th Latin-American Symposium on Dependable Computing, 2021

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2021

2020
Survey on automated symbolic verification and its application for synthesising cyber-physical systems.
IET Cyper-Phys. Syst.: Theory & Appl., 2020

Bounded Model Checking of Software Using Interval Methods via Contractors.
CoRR, 2020

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs.
CoRR, 2020

Incremental Verification of Fixed-Point Implementations of Neural Networks.
CoRR, 2020

Generating Adversarial Inputs Using A Black-box Differential Technique.
CoRR, 2020

Verifying Software Vulnerabilities in IoT Cryptographic Protocols.
CoRR, 2020

Finding Security Vulnerabilities in Network Protocol Implementations.
CoRR, 2020

Automated formal synthesis of provably safe digital controllers for continuous plants.
Acta Informatica, 2020

Synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison.
Proceedings of the Software Verification - 12th International Conference, 2020

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs.
Proceedings of the Software Verification - 12th International Conference, 2020

Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory - (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2020

2019
Experimental Data for Model Checking C++03 Programs.
Dataset, September, 2019

Verifying fragility in digital systems with uncertainties using DSVerifier <i>v</i>2.0.
J. Syst. Softw., 2019

Optimal Sizing of Stand-alone Solar PV Systems via Automated Formal Synthesis.
CoRR, 2019

Boost the Impact of Continuous Formal Verification in Industry.
CoRR, 2019

Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space.
CoRR, 2019

ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Finding Security Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification.
Proceedings of the 2019 International Workshop on Secure Internet of Things, 2019

Incremental Bounded Model Checking of Artificial Neural Networks in CUDA.
Proceedings of the IX Brazilian Symposium on Computing Systems Engineering, 2019

SMT-based refutation of spurious bug reports in the clang static analyzer.
Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, 2019

2018
DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles.
IEEE Trans. Reliab., 2018

Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP).
ACM SIGSOFT Softw. Eng. Notes, 2018

ESBMC-GPU A context-bounded model checking tool to verify CUDA programs.
Sci. Comput. Program., 2018

Counterexample guided inductive optimization based on satisfiability modulo theories.
Sci. Comput. Program., 2018

Automated Verification of Stand-alone Solar Photovoltaic Systems.
CoRR, 2018

Sim3Tanks: A Benchmark Model Simulator for Process Control and Monitoring.
IEEE Access, 2018

Map2Check Using LLVM and KLEE - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Towards counterexample-guided k-induction for fast bug detection.
Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract).
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

ESBMC 5.0: an industrial-strength C model checker.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems.
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2018

JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty.
IEEE Trans. Computers, 2017

Bounded model checking of C++ programs based on the Qt cross-platform framework.
Softw. Test. Verification Reliab., 2017

Handling loops in bounded model checking of C programs via k-induction.
Int. J. Softw. Tools Technol. Transf., 2017

BMCLua: A Translator for Model Checking Lua Programs.
ACM SIGSOFT Softw. Eng. Notes, 2017

A method to localize faults in concurrent C programs.
J. Syst. Softw., 2017

Multi-core model checking and maximum satisfiability applied to hardware-software partitioning.
Int. J. Embed. Syst., 2017

Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning (Extended Version).
CoRR, 2017

Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters.
CoRR, 2017

Counterexample-Guided k-Induction Verification for Fast Bug Detection.
CoRR, 2017

Automated Verification and Synthesis of Embedded Systems using Machine Learning.
CoRR, 2017

Counterexample Guided Inductive Optimization.
CoRR, 2017

SMT-based context-bounded model checking for CUDA programs.
Concurr. Comput. Pract. Exp., 2017

DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks.
Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

OptCE: A Counterexample-Guided Inductive Optimization Solver.
Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

Planning and Evaluation of UAV Mission Planner for Intralogistics Problems.
Proceedings of the VII Brazilian Symposium on Computing Systems Engineering, 2017

Counterexample guided inductive optimization applied to mobile robots path planning.
Proceedings of the 2017 Latin American Robotics Symposium (LARS) and 2017 Brazilian Symposium on Robotics (SBR), 2017

DSSynth: an automated digital controller synthesis tool for physical plants.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Verifying digital systems with MATLAB.
Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10, 2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends.
ACM SIGSOFT Softw. Eng. Notes, 2016

Bounded model checking for fixed-point digital filters.
J. Braz. Comput. Soc., 2016

Applying SMT-based verification to hardware/software partitioning in embedded systems.
Des. Autom. Embed. Syst., 2016

Verification of fixed-point digital controllers using direct and delta forms realizations.
Des. Autom. Embed. Syst., 2016

Application of Global Route-Planning Algorithms with Geodesy.
CoRR, 2016

Complementary Training Programme for Electrical and Computer Engineering Students Through an Industrial-Academic Collaboration (Extended Version).
CoRR, 2016

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration).
CoRR, 2016

Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

ESBMC<sup>QtOM</sup>: A Bounded Model Checking Tool to Verify Qt Applications.
Proceedings of the Model Checking Software - 23rd International Symposium, 2016

SMT-based Verification Applied to Non-convex Optimization Problems.
Proceedings of the VI Brazilian Symposium on Computing Systems Engineering, 2016

Verifying CUDA programs using SMT-based context-bounded model checking.
Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

Complementary training programme for electrical and computer engineering students through an industrial-academic collaboration.
Proceedings of the 2016 IEEE Frontiers in Education Conference, 2016

2015
Model checking LTL properties over ANSI-C programs with bounded traces.
Softw. Syst. Model., 2015

Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version).
CoRR, 2015

Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version).
CoRR, 2015

Model Checking Embedded C Software using k-Induction and Invariants (extended version).
CoRR, 2015

Model Checking C Programs with Loops via k-Induction and Invariants.
CoRR, 2015

Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version).
CoRR, 2015

DSVerifier: A Bounded Model Checking Tool for Digital Systems.
Proceedings of the Model Checking Software - 22nd International Symposium, 2015

Memory Management Test-Case Generation of C Programs Using Bounded Model Checking.
Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems.
Proceedings of the 2015 Brazilian Symposium on Computing Systems Engineering, 2015

Model Checking Embedded C Software Using k-Induction and Invariants.
Proceedings of the 2015 Brazilian Symposium on Computing Systems Engineering, 2015

Fault Localization in Multi-threaded C Programs Using Bounded Model Checking.
Proceedings of the 2015 Brazilian Symposium on Computing Systems Engineering, 2015

Hardware reconfiguration based on broadcasted digital TV signal.
Proceedings of the IEEE International Conference on Consumer Electronics, 2015

Bounded model checking of C++ programs based on the Qt framework.
Proceedings of the IEEE 4th Global Conference on Consumer Electronics, 2015

2014
Applying symbolic bounded model checking to the 2012 RERS greybox challenge.
Int. J. Softw. Tools Technol. Transf., 2014

ESBMC 1.22 - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking.
Proceedings of the 2014 Brazilian Symposium on Computing Systems Engineering, 2014

SMT-based bounded model checking of fixed-point digital controllers.
Proceedings of the IECON 2014 - 40th Annual Conference of the IEEE Industrial Electronics Society, Dallas, TX, USA, October 29, 2014

A secondary screen architecture to accurately capture viewers' interactions in an iTV environment.
Proceedings of the IEEE 3rd Global Conference on Consumer Electronics, 2014

BMCLua: Verification of Lua programs in digital TV interactive applications.
Proceedings of the IEEE 3rd Global Conference on Consumer Electronics, 2014

2013
Dynamic and automated product derivation for consumer electronics software applications.
IEEE Trans. Consumer Electron., 2013

Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
CoRR, 2013

Handling Unbounded Loops with ESBMC 1.20 - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

SMT-Based Bounded Model Checking of C++ Programs.
Proceedings of the 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems, 2013

2012
SMT-Based Bounded Model Checking for Embedded ANSI-C Software.
IEEE Trans. Software Eng., 2012

Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

A car racing based strategy for the Dynamic Voltage and Frequency Scaling technique.
Proceedings of the 21st IEEE International Symposium on Industrial Electronics, 2012

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples.
Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

2011
SMT-based bounded model checking of multi-threaded software in embedded systems.
PhD thesis, 2011

Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker
CoRR, 2011

Context-Bounded Model Checking of LTL Properties for ANSI-C Software.
Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker.
Proceedings of the Brazilian Symposium on Computing System Engineering, 2011

Verifying multi-threaded software using smt-based context-bounded model checking.
Proceedings of the 33rd International Conference on Software Engineering, 2011

Gift young engineers: An extra-curricular initiative for updating computer and electrical engineering courses.
Proceedings of the 2011 Frontiers in Education Conference, 2011

2010
Bounded Model Checking of Multi-threaded Software using SMT solvers
CoRR, 2010

SMT-based bounded model checking for multi-threaded software in embedded systems.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking.
Proceedings of the 17th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems, 2010

2009
Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints.
Proceedings of the International Conference on Embedded Software and Systems, 2009

2008
An agile development methodology applied to embedded control software under stringent hardware constraints.
ACM SIGSOFT Softw. Eng. Notes, 2008

Towards a model-driven engineering approach for developing embedded hard real-time software.
Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), 2008

Towards a Semiformal Development Methodology for Embedded Systems.
Proceedings of the ENASE 2008, 2008

A Platform-Based Software Design Methodology for Embedded Control Systems: An Agile Toolkit.
Proceedings of the 15th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2008), 31 March, 2008

ezRealtime: A Domain-Specific Modeling Tool for Embedded Hard Real-Time Software Synthesis.
Proceedings of the Design, Automation and Test in Europe, 2008

Mandos: A User Interaction Method in Embedded Applications for Mobile Telephony.
Proceedings of the First International Conference on Advances in Computer-Human Interaction, 2008

2007
TXM: an agile HW/SW development methodology for building medical devices.
ACM SIGSOFT Softw. Eng. Notes, 2007

Agile Development Methodology for Embedded Systems: A Platform-Based Design Approach.
Proceedings of the 14th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2007), 2007


  Loading...