Engineering Software - a Collection of Practice Projects

"Engineering" is the application of principles of science and mathematics to the design of useful things. To engineer software is to apply principles of mathematics to software design and implementation. Since software consists, literally, of formulas in mathematical logic, the principles of logic provide the basis for engineering software. These projects provide a practice ground for beginning to engineer software using the tools of mathematical logic.

Learning Goals
  • Equation-based software development
    (aka, functional programming, declarative programming)
  • Properties of software components expressed in predicate logic
  • Automated, random testing
  • Mechanized verification of software properties
  • Define the functions described in the project
  • Define and test the specified properties using, for example, DoubleCheck
  • Prove that your functions satisfy each defined property using, for example, ACL2







linear encoding cryptography steganography
firstN compress pattern search Conway's Game of Life
NthCdr blocks routing competitive pachinko
split every-other significant digits image calculator
append flip-flop linear regression audio processor
concat stats matrix rotoshop
Fibonacci symbolic differentiation
  • ACL2 - a programming language and mechanized logic, with automated proof assistance
  • DrScheme - support environment for Dracula
  • DrACula - interactive development environment for ACL2 with support for testing, graphics, and reactive software
Lectures and Other Supporting Material
  • Find lectures on mechanized logic for engineering software and other supporting materials here
  • Solutions for most of the projects are available to instructors
  • Contact Rex Page, University of Oklahoma
  • Provide your contact information through a URL to an official web page of your institution
Support for this work provided by