Paper Info
Title
Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
Abstract
Deagle is an SMT-based multi-threaded program verification tool. It is built on top of CBMC (front-end) and MiniSAT (back-end). The basic idea of Deagle is to integrate into the SMT solver an ordering consistency theory that handles ordering relations over the shared variable accesses in the program. The front-end encodes the input program into an extended propositional formula that contains ordering constraints. The back-end is reinforced with a solver for the ordering consistency theory. This paper presents the basic idea, architecture, installation, and usage of Deagle.
Year
DOI
Venue
2022
10.1007/978-3-030-99527-0_25
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II
Keywords
DocType
Volume
Program verification, Satisfiability modulo theories, Concurrency
Conference
13244
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Fei He117528.32
Zhihang Sun200.34
Hongyu Fan300.34