JBernstein: A Validity Checker for Generalized Polynomial Constraints

SRI author:

Citation

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.

↓ View online

Read more from SRI

  • surgeons around a surgical robot

    The SRI research behind today’s surgical robotics

    Intuitive’s da Vinci 5 system represents a major leap in robotic-assisted medicine. It all started at SRI, which continues to advance teleoperation technologies.

  • a collage of digital graphs

    A banner year for quantum

    SRI-managed QED-C’s annual report on quantum trends captures an industry accelerating rapidly from technical promise toward major global impact.

  • ICE Cube containing SRI’s aerogel experiment, photographed prior to launch. Source: Aerospace Applications North America

    An SRI carbon capture experiment launches into space

    By synthesizing carbon-absorbing aerogels in microgravity, SRI research will give us a rare glimpse into how these materials could be radically improved.