Proving Termination by Divergence.

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Domagoj Babic Articles by Alan J. Hu Articles by Zvonimir Rakamaric Articles by Byron Cook

Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)

London, England

September 10-September 14

ISBN: 0-7695-2884-8

	ASCII Text	x
	Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook, "Proving Termination by Divergence.," Software Engineering and Formal Methods, International Conference on, pp. 93-102, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007.

	BibTex	x
	@article{ 10.1109/SEFM.2007.32, author = {Domagoj Babic and Alan J. Hu and Zvonimir Rakamaric and Byron Cook}, title = {Proving Termination by Divergence.}, journal ={Software Engineering and Formal Methods, International Conference on}, volume = {0}, year = {2007}, isbn = {0-7695-2884-8}, pages = {93-102}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.32}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering and Formal Methods, International Conference on TI - Proving Termination by Divergence. SN - 0-7695-2884-8 SP93 EP102 A1 - Domagoj Babic, A1 - Alan J. Hu, A1 - Zvonimir Rakamaric, A1 - Byron Cook, PY - 2007 KW - null VL - 0 JA - Software Engineering and Formal Methods, International Conference on ER -

Domagoj Babic, University of British Columbia

Alan J. Hu, University of British Columbia

Zvonimir Rakamaric, University of British Columbia

Byron Cook, Microsoft Research

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.32

We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop?s termination condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. The paper closes with experimental results using short examples drawn from industrial code.

Citation:

Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook, "Proving Termination by Divergence.," sefm, pp.93-102, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.