ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution)

Tong Wu; Xianzhiyu Li; Edoardo Manino; Rafael  Sa Menezes; Mikhail R.  Gadelha; Shale  Xiong; Norbert Tihanyi; Pavlos Petoumenos; Lucas C. Cordeiro

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution)

Tong Wu, Xianzhiyu Li, Edoardo Manino, Rafael Sa Menezes, Mikhail R. Gadelha, Shale Xiong, Norbert Tihanyi, Pavlos Petoumenos, Lucas C. Cordeiro

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Publication status	Accepted/In press - 21 Jan 2025

Embargoed Document

tacas2025
Accepted author manuscript, 236 KB
Licence: CC BY
Embargo ends: 27/01/26

1 Finished
1 Active

EnnCore: End-to-End Conceptual Guarding of Neural Architectures
Cordeiro, L. (PI), Brown, G. (CoI), Freitas, A. (CoI), Luján, M. (CoI) & Mustafa, M. (CoI)
1/02/21 → 31/12/25
Project: Research
SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research

Cite this

Wu, T., Li, X., Manino, E., Sa Menezes, R., Gadelha, M. R., Xiong, S., Tihanyi, N., Petoumenos, P., & Cordeiro, L. C. (Accepted/In press). ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution). In 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems

@inproceedings{f8604c15015e4a01ac10099a6527f2f0,

title = "ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution)",

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{\textquoteright}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.",

author = "Tong Wu and Xianzhiyu Li and Edoardo Manino and {Sa Menezes}, Rafael and Gadelha, {Mikhail R.} and Shale Xiong and Norbert Tihanyi and Pavlos Petoumenos and Cordeiro, {Lucas C.}",

year = "2025",

month = jan,

day = "21",

language = "English",

booktitle = "31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems",

}

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution). / Wu, Tong; Li, Xianzhiyu; Manino, Edoardo et al.
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2025.

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution)

AU - Wu, Tong

AU - Li, Xianzhiyu

AU - Manino, Edoardo

AU - Sa Menezes, Rafael

AU - Gadelha, Mikhail R.

AU - Xiong, Shale

AU - Tihanyi, Norbert

AU - Petoumenos, Pavlos

AU - Cordeiro, Lucas C.

PY - 2025/1/21

Y1 - 2025/1/21

N2 - 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.

AB - 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.

M3 - Conference contribution

BT - 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems

ER -

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction (Competition Contribution)

Abstract

Embargoed Document

Fingerprint

Projects

EnnCore: End-to-End Conceptual Guarding of Neural Architectures

SCorCH: Secure Code for Capability Hardware

Cite this