Cheng, C.-H., Ruess, H., & Shankar, N. (2013, 13-19 July). JBernstein: a validity checker for generalized polynomial constraints. Paper presented at the International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia.
Overview
Efficient and scalable verification of nonlinear real arithmetic constraints is essential in many automated verification and synthesis tasks for hybrid systems, control algorithms, digital signal processors, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures for nonlinear real arithmetic are still a major obstacle for formal verification of real-world applications.