Show simple item record

dc.contributor.author
Brucker, Achim D.
dc.contributor.author
Wolff, Burkhart
dc.date.accessioned
2017-08-10T09:51:40Z
dc.date.available
2017-06-10T19:31:04Z
dc.date.available
2017-08-10T09:51:40Z
dc.date.issued
2004-06
dc.identifier.uri
http://hdl.handle.net/20.500.11850/69776
dc.identifier.doi
10.3929/ethz-a-006744541
dc.description.abstract
We present a method for the automatic generation of test cases for HOL formulae containing primitive recursive predicates. These test cases may be used for the animation of specifications as well as for black-box-testing of external programs. Our method is two-staged: first, the original formula is partitioned into test cases by transformation into a Horn-clause normal form (CNF). Second, the test cases are analyzed for ground instances satisfying the premises of the clauses. Particular emphasis is put on the control of test hypothesis’ and test hierarchies to avoid intractability. We applied our method to several examples, including AVL-trees and the red-black implementation in the standard library from SML/NJ.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
Symbolic test case generations
en_US
dc.subject
Isabelle/HOL
en_US
dc.subject
Theorem proving
en_US
dc.subject
Black box testing
en_US
dc.title
Symbolic Test Case Generation for Primitive Recursive Functions
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
ethz.journal.title
ETH technical report
ethz.journal.volume
449
en_US
ethz.size
20 p.
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.notes
Technical Reports D-INFK.
en_US
ethz.identifier.nebis
006744541
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.date.deposited
2017-06-10T19:34:36Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp593650d35cc8425393
ethz.identifier.importid
imp59366b14adfcd78278
ethz.ecolpid
eth:4774
ethz.ecitpid
pub:110483
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-16T03:17:00Z
ethz.rosetta.lastUpdated
2017-08-10T09:51:41Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Symbolic%20Test%20Case%20Generation%20for%20Primitive%20Recursive%20Functions&rft.jtitle=ETH%20technical%20report&rft.date=2004-06&rft.volume=449&rft.au=Brucker,%20Achim%20D.&Wolff,%20Burkhart&rft.genre=report&
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record