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

Undefined behaviour for 43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

@mutilin: How could we write models if we do not have a standard to follow? What is the standard for the hardware-dependent functions from `include/linux/string.h`? It seems that we have...

Undefined behavior in tasks due to division by zero

I also agree with this solution. Do we have already a PR that implements this solution?

Undefined behavior in tasks due to division by zero

Ok, let's break this task into categories. @danieldietsch: May I ask you to take care about the `ldv-*` benchmarks? @leostrakosch: May I ask you to take care about the `loop-*`...

Undefined behavior in tasks due to division by zero

I started adding assume statements to avoid undefined behavior in the `seq-mthreaded` benchmarks: PR https://github.com/sosy-lab/sv-benchmarks/pull/517 @danieldietsch and @leostrakosch: May I ask you to update this issue as soon as you...

Add type assertions when creating irep2s

@fbrausse: This issue might be interest to you :-)

ESBMC terminates after throwing an instance of 'std::length_error'

@fbrausse: Can I ask you to check this issue?

ESBMC terminates after throwing an instance of 'std::length_error'

Hi Franz, Your suggested approach looks okay to me. Best, Lucas Sent from my iPhone > On 1 Sep 2022, at 12:47, Franz Brauße ***@***.***> wrote: > >  >...

[Concurrency] Experimental results

* **Context-bound 2, --no-por, --timelimit 10s:** the current master (https://github.com/esbmc/esbmc/commit/251c80f570c9433242f74232a047b6a5bc24055b) produced the following results using 6GB: ``` Statistics: 768 Files correct: 102 correct true: 37 correct false: 65 incorrect: 4...

[Concurrency] Experimental results

* **--incremental-bmc --no-por --smt-during-symex --smt-symex-guard --smt-thread-guard --smt-symex-assert --z3 --timeout 30s:** the current master (https://github.com/esbmc/esbmc/commit/6d7ba105174dda1b792d79b1fb0fcb366b6720ea) produced the following results with 6GB: ``` Statistics: 768 Files correct: 35 correct true: 11 correct...

[Concurrency] Experimental results

The current version of the ESBMC master (https://github.com/esbmc/esbmc/commit/66dbfff29ca19a3948e5942c6a4a02f76a9b68f3) using the benchmarks from SV-COMP 2021: ``` Statistics: 1130 Files correct: 921 correct true: 150 correct false: 771 incorrect: 1 incorrect true:...