2017年
Sharper and simpler nonlinear interpolants for program verification
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- ,
- ,
- ,
- ,
- ,
- 巻
- 10695
- 号
- 開始ページ
- 491
- 終了ページ
- 513
- 記述言語
- 英語
- 掲載種別
- 研究論文(国際会議プロシーディングス)
- DOI
- 10.1007/978-3-319-71237-6_24
- 出版者・発行元
- Springer Verlag
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent result by Dai et al. that combines real algebraic geometry and SDP optimization in synthesis of polynomial interpolants, the current paper contributes its enhancement that yields sharper and simpler interpolants. The enhancement is made possible by: theoretical observations in real algebraic geometry
and our continued fraction-based algorithm that rounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool’s effectiandveness
we also demonstrate the benefit of sharp and simple interpolants in program verification examples.
and our continued fraction-based algorithm that rounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool’s effectiandveness
we also demonstrate the benefit of sharp and simple interpolants in program verification examples.
- リンク情報
- ID情報
-
- DOI : 10.1007/978-3-319-71237-6_24
- ISSN : 1611-3349
- ISSN : 0302-9743
- DBLP ID : conf/aplas/OkudonoNKSKH17
- SCOPUS ID : 85034966399