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

1 Downloads (Pure)

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

Access to Document

tacas2025Accepted author manuscript, 236 KBLicence: CC BY

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

Access to Document

Fingerprint

Projects

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

SCorCH: Secure Code for Capability Hardware

Cite this