Verification

Interior Search for Nonlinear SMT and Application in Verification

Interior Search for Nonlinear SMT and Application in Verification Surface-mount technology (SMT) formulas over the real numbers can encode a wide range of problems in theorem proving and formal verification. Currently, constraint solving and verification in nonlinear theories over the reals use strategies that are similar to SAT solving. The current algorithms perform top-down global […]

Better Search Methods for Derivative-free Optimization

By Angela Berti12 August 2024ChipsChips-Systems Design, Verification

Better Search Methods for Derivative-free Optimization Non-convex global optimization problems are well-known to be NP-hard, and the practical challenge lies in distinguishing the global optimum from exponentially many potential local optima. Existing approaches to non-convex optimization can be largely categorized into sampling-based methods and tree-search methods. Sampling-based approaches explore the solution space through random sampling […]