Regression verification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Regression verification

Full text

Pdf (138 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 46th Annual Design Automation Conference table of contents

San Francisco, California

SESSION: Jumping the high-level verification hurdle table of contents

Pages 466-471

Year of Publication: 2009

ISBN:978-1-60558-497-3

Authors

Benny Godlin	CS, Technion, Haifa, Israel
Ofer Strichman	IE, Technion, Haifa, Israel

Sponsors

EDAC : Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS : Circuits & Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 8, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629911.1630034 What is a DOI?

ABSTRACT

Proving the equivalence of successive, closely related versions of a program has the potential of being easier in practice than functional verification, although both problems are undecidable. There are two main reasons for this claim: it circumvents the problem of specifying what the program should do, and in many cases it is computationally easier. We study theoretical and practical aspects of this problem, which we call regression verification.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	T. Arons, E. Elster, L. Fix, S. MadorHaim, M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, M. Y. Vardi, and L. D. Zuck. Formal verification of backward compatibility of microcode. In CAV05, volume 3576 of LNCS. Springer, 2005.
	2	B. Godlin. Regression verification: Theoretical and implementation aspects. Master's thesis, Technion, Israel Institute of Technology, 2008.
	3	B. Godlin and O. Strichman. Inference rules for proving the equivalence of recursive procedures. Acta Informatica, 45(6):403--439, 2008.
	4	A. Groce, D. Kroening, and F. Lerda. Understanding counterexamples with explain. In CAV, pages 453--456, 2004.
	5	M. Haroud and A. Biere. SDL versus C equivalence checking. In SDL Forum, pages 323--338, 2005.
	6	C. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576--580, 1969.
	7	C. Hoare. Procedures and parameters: an axiomatic approach. In Proc. Sym. on semantics of algorithmic languages, (188), 1971.
	8	T. Hoare. The verifying compiler: A grand challenge for computing research. J. ACM, 50(1):63--69, 2003.
	9	D. Kroening, E. Clarke, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of DAC 2003, pages 368--371. ACM Press, 2003.
	10	D. Kroening and O. Strichman. Decision procedures -- an algorithmic point of view. Theoretical computer science. Springer, May 2008.
	11	P. Manolios and M. Kaufmann. Adding a total order to acl2. In The Third International Workshop on the ACL2 Theorem Prover, 2002.
	12	P. Manolios and D. Vroon. Ordinal arithmetic: Algorithms and mechanization. Journal of Automated Reasoning, 2006. to appear.
	13	A. Pnueli, M. Siegel, and O. Shtrichman. Translation validation for synchronous languages. In Proc. 25th Int. Colloq. on Automata, Languages and Programming (ICALP'98), volume 1443 of LNCS, pages 235--246. Springer, 1998.
	14	A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In TACAS'08, volume 1384 of LNCS, pages 151--166. Springer, 1998.