Automated verification of loops with assignments only by recurrence solving and optimization problems

Jianying Xing; Mengjun Li; Zhoujun Li

doi:10.1109/ICFCC.2010.5497670

Automated verification of loops with assignments only by recurrence solving and optimization problems

Jianying Xing^*
, Mengjun Li
, Zhoujun Li

^*Corresponding author for this work

School of Computer Science and Engineering

National University of Defense Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Based on techniques of solving recurrence equations and optimization problems, we present a practical approach for verifying program including loops with assignments only. We implement this approach on the platform of Mathmatica. The experimental results demonstrate the power of our approach.

Original language	English
Title of host publication	Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010
Pages	V331-V336
DOIs	https://doi.org/10.1109/ICFCC.2010.5497670
State	Published - 2010
Event	2010 2nd International Conference on Future Computer and Communication, ICFCC 2010 - Wuhan, China Duration: 21 May 2010 → 24 May 2010

Publication series

Name	Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010
Volume	3

Conference

Conference	2010 2nd International Conference on Future Computer and Communication, ICFCC 2010
Country/Territory	China
City	Wuhan
Period	21/05/10 → 24/05/10

Keywords

Optimization problem
Program verification
Recurrence equations
Termination

Access to Document

10.1109/ICFCC.2010.5497670

Cite this

Xing, J., Li, M., & Li, Z. (2010). Automated verification of loops with assignments only by recurrence solving and optimization problems. In Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010 (pp. V331-V336). Article 5497670 (Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010; Vol. 3). https://doi.org/10.1109/ICFCC.2010.5497670

Xing, Jianying ; Li, Mengjun ; Li, Zhoujun. / Automated verification of loops with assignments only by recurrence solving and optimization problems. Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010. 2010. pp. V331-V336 (Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010).

@inproceedings{a0d2e33504cd45a9b1e868ecc1c6f83c,

title = "Automated verification of loops with assignments only by recurrence solving and optimization problems",

abstract = "Based on techniques of solving recurrence equations and optimization problems, we present a practical approach for verifying program including loops with assignments only. We implement this approach on the platform of Mathmatica. The experimental results demonstrate the power of our approach.",

keywords = "Optimization problem, Program verification, Recurrence equations, Termination",

author = "Jianying Xing and Mengjun Li and Zhoujun Li",

year = "2010",

doi = "10.1109/ICFCC.2010.5497670",

language = "英语",

isbn = "9781424458226",

series = "Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010",

pages = "V331--V336",

booktitle = "Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010",

note = "2010 2nd International Conference on Future Computer and Communication, ICFCC 2010 ; Conference date: 21-05-2010 Through 24-05-2010",

}

Xing, J, Li, M & Li, Z 2010, Automated verification of loops with assignments only by recurrence solving and optimization problems. in Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010., 5497670, Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010, vol. 3, pp. V331-V336, 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010, Wuhan, China, 21/05/10. https://doi.org/10.1109/ICFCC.2010.5497670

Automated verification of loops with assignments only by recurrence solving and optimization problems. / Xing, Jianying; Li, Mengjun; Li, Zhoujun.
Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010. 2010. p. V331-V336 5497670 (Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010; Vol. 3).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Automated verification of loops with assignments only by recurrence solving and optimization problems

AU - Xing, Jianying

AU - Li, Mengjun

AU - Li, Zhoujun

PY - 2010

Y1 - 2010

N2 - Based on techniques of solving recurrence equations and optimization problems, we present a practical approach for verifying program including loops with assignments only. We implement this approach on the platform of Mathmatica. The experimental results demonstrate the power of our approach.

AB - Based on techniques of solving recurrence equations and optimization problems, we present a practical approach for verifying program including loops with assignments only. We implement this approach on the platform of Mathmatica. The experimental results demonstrate the power of our approach.

KW - Optimization problem

KW - Program verification

KW - Recurrence equations

KW - Termination

UR - https://www.scopus.com/pages/publications/78049357470

U2 - 10.1109/ICFCC.2010.5497670

DO - 10.1109/ICFCC.2010.5497670

M3 - 会议稿件

AN - SCOPUS:78049357470

SN - 9781424458226

T3 - Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010

SP - V331-V336

BT - Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010

T2 - 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010

Y2 - 21 May 2010 through 24 May 2010

ER -

Xing J, Li M, Li Z. Automated verification of loops with assignments only by recurrence solving and optimization problems. In Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010. 2010. p. V331-V336. 5497670. (Proceedings of the 2010 2nd International Conference on Future Computer and Communication, ICFCC 2010). doi: 10.1109/ICFCC.2010.5497670

Automated verification of loops with assignments only by recurrence solving and optimization problems

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this