Software Engineering with
   predicate-based, test-driven development and
   mechanized logic

Engineering Correct Software. Engineering, according to dictionaries, is the applying principles of science and mathematics to the design of useful things. Software engineering isn't. A primary goal of this project is to develop educational materials that present software engineering within an engineering framework.

Projects for learning to engineer software may be found here:
   http://www.cs.ou.edu/~rlpage/SEcollab/20projects.htm

A one-page description of three courses that have emerged from this process so far may be viewed here:
   http://www.cs.ou.edu/~rlpage/SEcollab/EngineeringSoftwareCourses.pdf
A short paper on the courses may be viewed here:
   http://www.cs.ou.edu/~rlpage/SEcollab/rlpACL209.pdf
   slides from presentation
Links to specific materials on the subject appear below.

Teaching Software Correctness Workshop, May 13-15, 2008

Publications on the use of mechanized logic and predicate-based testing in software engineering:

• Engineering software correctness, Journal of Functional Programming 17, 6 (Nov 2007) 675-686
  FDPE 2005 Conference presentation: PDF slides, PPT slides
• Functional Programming and Theorem Proving for Undergraduates: A Progress Report, FDPE 2008, Victoria, B.C., Canada (Sep 21, 2008) (with Carl Eastlund and Matthias Felleisen) 21-29
• ACL2 in DrScheme, Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, Seattle Washington (Aug 15-16, 2006) (with Dale Vaillancourt and Matthias Felleisen) 107-116

Lecture Notes - Mechanized logic
    zipped PDF
    zipped PPT

Lecture Notes - Processes
    zipped PDF
    zipped PPT

Projects
    Project write-ups (zipped HTML, two project sequences for SE-I: 1A, 1B)
    Software supplied with projects (zipped Lisp)

Syllabus, texbooks, lesson plan, ... (SE-I)
    PDF