Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
Fei He, Zhihang Sun, Hongyu Fan
Abstract
Abstract is an SMT-based multi-threaded program verification tool. It is built on top of (front-end) and (back-end). The basic idea of 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 .
Topics & Concepts
Computer scienceConsistency (knowledge bases)SolverFront and back endsSatisfiability modulo theoriesProgramming languageArchitectureTheoretical computer scienceAlgorithmArtificial intelligenceVisual artsArtFormal Methods in VerificationSoftware Testing and Debugging TechniquesLogic, programming, and type systems