P515 Specification and Verification (3 cr.) Tools and techniques for
rigorous reasoning about software and digital hardware.  Safety,
reliability, security, and other design-critical applications.
Decision algorithms. Projects involving the use of automated
reasoning, such as model checkers, theorem provers, and program
transformation. Credit not given for both P415 and P515.