SMT Solving for the Theory of Ordering Constraints Conference Paper

abstract

• Springer International Publishing Switzerland 2016. Constraint solving and satisfiability checking play an important role in various tasks such as formal verification, software analysis and testing. In this paper, we identify a particular kind of constraints called ordering constraints, and study the problem of deciding satisfiability modulo such constraints. The theory of ordering constraints can be regarded as a special case of difference logic, and is essential for many important problems in symbolic analysis of concurrent programs. We propose a new approach for checking satisfiability modulo ordering constraints based on the DPLL(T) framework, and present our experimental results compared with state-of-the-art SMT solvers on both benchmarks and instances of real symbolic constraints.

authors

• Huang, Jeff

published proceedings

• Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

author list (cited authors)

• Ge, C., Ma, F., Huang, J., & Zhang, J.

citation count

• 1

complete list of authors

• Ge, Cunjing||Ma, Feifei||Huang, Jeff||Zhang, Jian

publication date

• February 2016

publisher

• Springer Nature  Publisher

published in

• Lecture Notes in Artificial Intelligence  Journal

Digital Object Identifier (DOI)

• 10.1007/978-3-319-29778-1_18

International Standard Book Number (ISBN) 13

• 9783319297774

start page

• 287

end page

• 302

volume

• 9519