Lucas C. Cordeiro

icon indicating a website link https://ssvlab.github.io/lucasccordeiro/ icon indicating an email [email protected]

icon company The University of Manchester, UK icon location Manchester icon location Lucas C. Cordeiro is a Full Professor in the Department of Computer Science at the University of Manchester/UK and an Associate Professor at UFAM/Brazil.

Results 215 comments of Lucas C. Cordeiro

Floating point violation witness validation

@fbrausse: are you going to submit a PR for this issue?

[Python] Shall we really invoke the SMT solver for this simple Python program?

It looks like we don't propagate the store operations involving constants: ```` Program constraints: // 0 file main.py line 3 column 8 function MyClass /* 1 */ obj1&0#1 == (obj1&0#0...

[Solidity] Support Continue Keyword

@JacobYiu: Can I ask you for the status of this issue?

ESBMC Segmentation Fault

@Yiannis128: we will be able to check this issue just after the SV-COMP 2024 deadline.

Unable to verify solidity smart contract code

@ChenfengWei0: can I ask you to update our documentation at https://ssvlab.github.io/esbmc/documentation.html?

Unable to verify solidity smart contract code

Thank you.

[C++ verification] Incorrect result in case of initialization by the most derived class

@kunjsong01: can I ask you for the status of this issue?

Segmentation fault on VLA

@rafaelsamenezes: I remember that you did some work on this VLA support. Could you please take a look at this issue?

Segmentation fault on VLA

@rafaelsamenezes: This VLA example still seems unsupported in ESBMC. It fails with: ``` esbmc: /home/lucas/ESBMC_Project/esbmc/src/util/migrate.cpp:528: expr2tc sym_name_to_symbol(irep_idt, type2tc): Assertion `endatptr != atstr.c_str()' failed. Aborted ```` Can I ask you please...

Segmentation fault on VLA

ESBMC still fails with this example: ```` ESBMC version 7.2.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing Converting esbmc: /home/lucas/ESBMC_Project/esbmc/src/util/migrate.cpp:544: expr2tc sym_name_to_symbol(irep_idt, type2tc): Assertion `endatptr != atstr.c_str()'...