Title:
raSAT - an SMT for Polynomial Constraints

Speaker:
XUAN, Tung Vu (JAIST)

Abstract:
raSAT is an SMT solver for polynomial constraints, which aims to handle them over both reals and integers with simple unified methodologies: (1) raSAT loop for inequations, which extends the Interval Constraint Propagation with testing to accelerate SAT detection, and (2) a non-constructive reasoning for equations over reals, based on the Intermediate Value Theorem. This presentation focuses only on (1). Part (2) will be presented upon requests.