Trabalho em anais de eventoOpen Access
ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction
WU, T.; SONG, S.; MANINO, E.; STOCKWELL, G.; CORDEIRO, L. C
Resumo
Resumo
Abstract ESBMC v7.7 improves the verification of concurrent C programs by incorporating techniques such as dynamic thread scheduling, incremental SMT solving, and partial order reduction (POR). These improvements enhance the tool’s performance, particularly in exploring complex multi-threaded executions. The new scheduler prioritizes higher-thread identifiers during context switches, which helps explore deeper program states. The use of incremental SMT solving and a refined POR algorithm reduces the exploration of unreachable interleavings and redundant states. These updates enable ESBMC to detect bugs faster, making it a more effective tool for ensuring the safety of multi-threaded applications.
palavras-chave
Palavras-chave
ESBMCpartial order reductioncontext switchingstate space explorationbug detectionmodel checking
Status
Published
links
Links e arquivos
Trabalho em anais de evento