verification

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and …
PDF Cite Code Slides DOI
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
Decidability of the Reachability for a Family of Linear Vector Fields
The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of …
PDF Cite Code Slides DOI
Decidability of the Reachability for a Family of Linear Vector Fields