Computer Science ETDs

Publication Date

Spring 5-16-2026

Abstract

Polynomials have been found to be a powerful tool over hundreds of years for modeling problems in numerous applications in science, engineering, medicine, and other domains. In the context of formal methods, polynomials arise in modeling in aerospace software and robotics, cyber-physical and hybrid systems, autonomous vehicles and controllers based on neural networks.

A quadratic module is a linear combination of polynomials in a set of generators (including the constant 1) with sum of squares polynomials as multipliers. The membership problem for a finitely generated quadratic module can be decided; however, computing a certificate exhibiting why it is nonnegative under the assumption that the generators are nonnegative, can be nontrivial.

A new symbolic algorithm is presented to compute sums of squares multipliers (certificates) to witness the membership of univariate polynomials in Archimedean quadratic modules. An algorithm is presented to compute a certificate for $-1$ in inconsistent quadratic modules in $\aXY$.

Language

English

Keywords

Archimedean Quadratic modules, Preorderings, Verification

Document Type

Dissertation

Degree Name

Computer Science

Level of Degree

Doctoral

Department Name

Department of Computer Science

First Committee Member (Chair)

Prof. Deepak Kapur

Second Committee Member

Prof. Chenqi Mou

Third Committee Member

Prof. Naijun Zhan

Fourth Committee Member

Prof. Shuang Luan

Project Sponsors

National Science Foundation under Grant CCF-2513374

Download

Share

COinS