File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Article: Semi-proving: An integrated method for program proving, testing, and debugging

TitleSemi-proving: An integrated method for program proving, testing, and debugging
Authors
Chen, TYTse, THZhou, ZQ
KeywordsSoftware/program verification
symbolic execution
testing and debugging
Issue Date2011
PublisherI E E E. The Journal's web site is located at http://www.computer.org/tse
Citation
Ieee Transactions On Software Engineering, 2011, v. 37 n. 1, p. 109-125 How to Cite?
DOI: http://dx.doi.org/10.1109/TSE.2010.23
AbstractWe present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For programs where global symbolic evaluation can be conducted and the constraint expressions involved can be solved, we can either prove that these necessary conditions for program correctness are satisfied or identify all inputs that violate the conditions. For other programs, our method can be converted into a symbolic-testing approach. Our method extrapolates from the correctness of a program for tested inputs to the correctness of the program for related untested inputs. The method supports automatic debugging through the identification of constraint expressions that reveal failures. © 2011 IEEE.
Persistent Identifierhttp://hdl.handle.net/10722/136222
ISSN
0098-5589
2021 Impact Factor: 9.322
2020 SCImago Journal Rankings: 0.857
ISI Accession Number ID
WOS:000286676700008
Funding AgencyGrant Number
Research Grants Council of Hong Kong717308
Australian Research CouncilDP 0771733
University of Wollongong
Funding Information:

All correspondence should be addressed to Dr. Zhi Quan Zhou at the address shown on the first page of this paper. The authors are grateful to Willem Visser for his helps and discussions on symbolic-execution techniques using the Java PathFinder model checker [1], [44]. They are also grateful to Giovanni Denaro and his group for providing the symbolic-execution tool SAVE [21]. They would like to thank Joxan Jaffar and Roland Yap for providing a constraint solver [42]. They would also like to thank Bernhard Scholz and Phyllis Frankl for their information and discussions on symbolic-evaluation techniques. This research is supported in part by the General Research Fund of the Research Grants Council of Hong Kong (project no. 717308), a Discovery Grant of the Australian Research Council (project no. DP 0771733), and a Small Grant of the University of Wollongong.

References
References in Scopus

 

DC FieldValueLanguage
dc.contributor.authorChen, TYen_HK
dc.contributor.authorTse, THen_HK
dc.contributor.authorZhou, ZQen_HK
dc.date.accessioned2011-07-27T02:04:59Z-
dc.date.available2011-07-27T02:04:59Z-
dc.date.issued2011en_HK
dc.identifier.citationIeee Transactions On Software Engineering, 2011, v. 37 n. 1, p. 109-125en_HK
dc.identifier.issn0098-5589en_HK
dc.identifier.urihttp://hdl.handle.net/10722/136222-
dc.description.abstractWe present an integrated method for program proving, testing, and debugging. Using the concept of metamorphic relations, we select necessary properties for target programs. For programs where global symbolic evaluation can be conducted and the constraint expressions involved can be solved, we can either prove that these necessary conditions for program correctness are satisfied or identify all inputs that violate the conditions. For other programs, our method can be converted into a symbolic-testing approach. Our method extrapolates from the correctness of a program for tested inputs to the correctness of the program for related untested inputs. The method supports automatic debugging through the identification of constraint expressions that reveal failures. © 2011 IEEE.en_HK
dc.languageengen_US
dc.publisherI E E E. The Journal's web site is located at http://www.computer.org/tseen_HK
dc.relation.ispartofIEEE Transactions on Software Engineeringen_HK
dc.rights©2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.-
dc.subjectSoftware/program verificationen_HK
dc.subjectsymbolic executionen_HK
dc.subjecttesting and debuggingen_HK
dc.titleSemi-proving: An integrated method for program proving, testing, and debuggingen_HK
dc.typeArticleen_HK
dc.identifier.openurlhttp://library.hku.hk:4550/resserv?sid=HKU:IR&issn=0098-5589&volume=37&issue=1&spage=109&epage=125&date=2011&atitle=Semi-proving:+an+integrated+method+for+program+proving,+testing,+and+debugging-
dc.identifier.emailTse, TH: thtse@cs.hku.hken_HK
dc.identifier.authorityTse, TH=rp00546en_HK
dc.description.naturepublished_or_final_version-
dc.identifier.doi10.1109/TSE.2010.23en_HK
dc.identifier.scopuseid_2-s2.0-79551537874en_HK
dc.identifier.hkuros184464en_US
dc.identifier.hkuros169030-
dc.relation.referenceshttp://www.scopus.com/mlt/select.url?eid=2-s2.0-79551537874&selection=ref&src=s&origin=recordpageen_HK
dc.identifier.volume37en_HK
dc.identifier.issue1en_HK
dc.identifier.spage109en_HK
dc.identifier.epage125en_HK
dc.identifier.isiWOS:000286676700008-
dc.publisher.placeUnited Statesen_HK
dc.identifier.scopusauthoridChen, TY=13104290200en_HK
dc.identifier.scopusauthoridTse, TH=7005496974en_HK
dc.identifier.scopusauthoridZhou, ZQ=15924687500en_HK
dc.identifier.issnl0098-5589-

Export via OAI-PMH Interface in XML Formats

OR

Export to Other Non-XML Formats