Teaching Software Correctness Workshop, May 13-15, 2008, Univ of Oklahoma & NSF

Instructor

 Rex Page

Assistants

 Carl Eastlund (lead), Ryan Ralston, Zac White
Tuesday

Directions to Lodging & Lab

Participants
9:00-10:15 01 Lecture: ACL2 programs Goals, function definitions, tests, theorems
10:15-10:30

coffee break

     (defun, DoubleCheck, defth
10:30-12:00 02 Lab session Participants select from several small exercises
12:00-1:30

lunch break
1:30-2:30 03 Lecture: Guiding ACL2 Using lemmas and hints to facilitate proofs
2:30-2:45

coffee break

      (use-instance, hands-off, disable, ...)
2:45-5:45 04 Lab session Add theorems to code and certify
5:45-6:00 05 Evaluation Online assessment questionnaire
Wednesday
9:00-10:15 06 Lecture: File i/o and GUIs ACL2 file i/o and DrACuLa GUIs
10:15-10:30

coffee break

  
10:30-12:00 07 Lab session A projects with file i/o and another with a GUI
12:00-1:30

lunch break
1:30-2:00 08 Lecture: Exports and Imports Organizing and certifying "books" for import
2:00-3:15 09 Lab session Crypto project - encryption of text
3:15-3:30

coffee break

 Coffee and entertainment: Fibonacci-fast vs slow
3:30-5:45 10 Lab session Continue crypto project
5:45-6:00 11 Evaluation Online assessment questionnaire
Thursday
9:00-9:45 12 Lecture: Top down design ACL2 encapsulate, local; true-list predicates
9:45-10:00

coffee break
10:00-11:30 13 Lab session Steganography project (binary file i/o, encryption)
11:30-1:00

lunch break
1:00-1:30 14 Lecture: DrACula modules Demo DrACula modules prototype
1:30-2:15 15 Discussion: TSC in practice Possible uses of predicate-based testing, mechanical logic in undergrad coursework or projects
2:15-3:45 16 Lab session True-list predicates; Steganography project 
3:45-4:00 17 Evaluation Online assessment questionnaire