线性程序的Ranking函数自动合成

李骏; 李轶; 冯勇; 秦小林

您当前的位置：

首页 >

文章列表页 >

线性程序的Ranking函数自动合成

信息工程 | 更新时间：2023-11-28

- 线性程序的Ranking函数自动合成
- Automatic Synthesis of Linear Program Ranking Functions
- 工程科学与技术 2009年41卷第5期页码：176-181
- 作者机构：
  
  中国科学院成都计算机应用研究所
- 作者简介：
- 基金信息：
  
  国家科委973资助项目(2004CB318003);中国科学院知识创新重要方向项目（KJCX2-YW-S02）;国家自然科学基金（10771205）;国家自然科学基金（90718041）
- DOI：
  中图分类号：
- 纸质出版日期：2009，
  
  网络出版日期：2009-6-3，
扫描看全文
李骏,李轶,冯勇,秦小林.线性程序的Ranking函数自动合成[J].工程科学与技术,2009,41(5):176-181.

Li Jun, LI Yl, Feng Yong, et al. Automatic Synthesis of Linear Program Ranking Functions[J]. Advanced Engineering Sciences, 2009,41(5):176-181.
李骏,李轶,冯勇,秦小林.线性程序的Ranking函数自动合成[J].工程科学与技术,2009,41(5):176-181. DOI：

Li Jun, LI Yl, Feng Yong, et al. Automatic Synthesis of Linear Program Ranking Functions[J]. Advanced Engineering Sciences, 2009,41(5):176-181. DOI：

摘要

中文摘要: 针对判定一个程序终止性的经典方法Ranking函数法，运用半代数转换系统的概念，把程序终止性问题转换为求半代数系统的Ranking函数。然后运用符号计算工具DISCOV- ERER和Farkas引理，求出函数参数存在的充分必要条件，并根据符号计算理论的方法自动合成Ranking函数。通过计算代数理论的证明和试验的验证，并与其他方法做了比较，这种方法是高效合理的。

Abstract

Abstract:Due to determining the classical ranking functions of program verification

a new approach was proposed based on the theory of semi-algebraic systems. It automatically converts the problem of program verification to solve the ranking function of semi-algebraic systems. The sufficient and necessary conditions on parameters in ranking functions can be obtained using symbolic computation tool

DISCOVERER and Farkas' Lemma

and then automatically synthesized the novel ranking function by symbolic computations. The method with other methods to do a comparative is reasonable theoretically

and experimental results show that it is efficient.

关键词

DISCOVERERFarkas' lemmaRanking函数半代数系统程序终止性程序验证

Keywords

DISCOVERERFarkas' LemmaRanking FunctionSemi-Algebraic SystemsTermination of Programprogram verification

references

Yang L;Hou X;Zeng Z,A complete discrimination system for polynomials,Science in China(Series E),1996.

Collins G E;Hong H,Partial cylindrical algebraic decomposition for quantifier elimination,Symbolic Computation,1991.

Andreas Dolzmann ；Thomas Sturm,RBDLOG: Computer Algebra Meets Computer Logic,SIGSAM Bulletin

Yang L;Xia B,Automated deduction in real geometry,Singapore:World Scientific Publishing Co.Ptc.Ltd,2004.

Clarke E M;Grumberg Q;Peled D A,Model checking,Cambridge,MA:The MIT Press,1999.

Yang L,Recent advances on determining the number of real roots of parametric polynomials,Symbolic Computation,1999(1-2).

Xia B;Zhang T,Real Solution Isolation Using Interval Arithmetic,Computers ＆ Mathematics with Applications,2006.

Yinghua Chen;Bican Xia;Lu Yang,Discovering nonlinear ranking functions by solving semi-algebraic systems,Heidelberg:SpringerVerlng,2007.

Podelski A;Rybalchenko A,A complete method for the synthesis of linear ranking functions,Heidelberg:Springer-Verlag,2004.

Cousot P,Proving program invarianee and termination by parametric abstraction,Langrangian Relaxation and semidefinite programming,Heidelberg:Springer-Verlag,2005.

Colon M;Sipma H B,Synthesis of linear ranking functions,Heidelberg:Springer-Verlag,2001.

Hoare C A R,An axiomatic basis for computer programming,Comm CM,1969(10).

Floyd R W,Assigning meanings to programs,Symphosia in Applied Mathematics,1967.

Dijkstra E W,A discipline of programming,Englewood Cliffs:Prentice-Hall,1976.

Aaron R Bradley;Zohar Manna;Henny Sipma,Linear Ranking with Reachability,Heidelberg:Springer-Verlag,2005.

Manna Z;Pnueli A,Temporal Verification of Reactive Systems,Heidelberg:Springer-Verlag,1995.

Sankaranarayanan S;Sipma H B;Manna Z,Non-linear loop invariant generation using Grobner bases,New York:ACM,2004.

Xia B;Yang L,An algorithm for isolating the real solutions of semi-algebraic systems,Symbolic Computation,2002.

Xia B;Xiao R;Yang L,Solving parametric semi-algebraic systems,2005.

Yang L;Xia B,Real solution classifications of a class of parametric semialgebraic systems,Heidelberg:Springer-Verlag,2005.

更多指标>

浏览量

268

下载量

CNKI被引量

文章被引用时，请邮件提醒。

提交

工具集

关联资源

一类循环条件非线性的程序终止性

多区间上非线性程序的终止性判定