Heuristically creating test cases for program verification systems

dc.contributor.authorBeckert, B.en
dc.contributor.authorBormer, M.en
dc.contributor.authorWagner, M.en
dc.contributor.conferenceMetaheuristics International Conference (10th : 2013 : Singapore)en
dc.date.issued2013en
dc.description.abstractThe correctness of program verification systems is of great importance, as they are used to formally prove that safety- and security-critical programs follow their specification. This correctness needs to be checked and demonstrated to users and certification agencies. One of the contributing factors to the correctness of the whole verification system is the correctness of the background axiomatization, which captures the semantics of the target program language. We present an optimisation framework for the maximization of the proportion of the axiomatization that is used (“covered”) during testing of the verification tool. We show how test cases for regression tests can be created based on existing ones, as the initial creation of test cases is a very time consuming process. Our study shows that the combination of different heuristics leads to a diverse set of test cases, which in turn increases the axiomatization coverage. This translates into a significant increase in trust in the program verification system.en
dc.description.statementofresponsibilityBernhard Beckert, Thorsten Bormer, Markus Wagneren
dc.identifier.citationProceedings of the 10th Metaheuristics International Conference, MIC2013: pp.37-46en
dc.identifier.orcidWagner, M. [0000-0002-3124-0061]en
dc.identifier.urihttp://hdl.handle.net/2440/83951
dc.language.isoenen
dc.publisherSingapore Management Universityen
dc.publisher.placeonlineen
dc.rightsCopyright status unknownen
dc.titleHeuristically creating test cases for program verification systemsen
dc.typeConference paperen
pubs.publication-statusPublisheden

Files