New preprint: Loop unrolling — formal definition and application to testing
New preprint: Li Huang, Bertrand Meyer and Reto Weber, New preprint: Loop unrolling: formal definition and application to testing, February 2025, submitted to publication. Available here on arXiv and also here.
Abstract
Testing coverage criteria usually make a gross simplification: they assume that loops will have their bodies executed 0 or 1 time. How much (specificall,y how many bugs) are we missing as a result?
This article defines loop unrolling formally (removing common misconceptions of the topic), shows how loop unrolling was applied to a testing framework (using program-proving techniques as well), in line with our test-and-proofs work of the past several years), and presents detailed empirical evidence about the effect on finding bugs.
(Some of the initial ideas were recorded earlier in an unpublished technical note.)
Reminder: my full annotated publication list is here.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy