Trabalho em anais de eventoOpen Access
Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution)
CORDEIRO, L. C.; Morse, Jeremy; Nicole, Denis; FISCHER, BERND
Resumo
Resumo
ESBMC is a context-bounded symbolic model checker that allows the verification of single- and multi-threaded C code with shared variables and locks. ESBMC supports full ANSI-C, and can verify programs that make use of bit-level operations, arrays, pointers, structs, unions, memory allocation and floating-point arithmetic. It can reason about arithmetic under- and overflows, pointer safety, memory leaks, array bounds violations, atomicity and order violations, local and global deadlocks, data races, and user-specified assertions. However, as other bounded model checkers, ESBMC is in general incomplete
palavras-chave
Palavras-chave
ESBMCsymbolic model checkingANSI Cmultithreaded programsverification conditionsSMT solversbackground theoryprogram verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento