English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We report on our experience using ACL2 in the classroom to teach studentsabout software testing. The course COSC2300 at the University of Wyoming is amostly traditional Discrete Mathematics course, but with a clear focus oncomputer science applications. For instance, the section on logic and proofs ismotivated by the desire to write proofs about computer software. We emphasizethat the importance of software correctness falls along a spectrum with casualprograms on one end and mission-critical ones on the other. Corresponding tothis spectrum is a variety of tools, ranging from unit tests, randomizedtesting of properties, and even formal proofs. In this paper, we describe oneof the major activities, in which students use the ACL2 Sedan's counter-examplegeneration facility to investigate properties of various existing checksumalgorithms used in error detection. Students are challenged to state therelevant properties correctly, so that the counter-example generation tool isused effectively in all cases, and ACL2 can find formal proofs automatically insome of those.

Using ACL2 To Teach Students About Software Testing