SMT Solving for the Theory of Ordering Constraints Conference Paper uri icon


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

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