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.