Mathematical techniques for describing software systems, proving properties of
a the system's behavior prior to its implementation, and determining if the
system has been correctly implemented. Description mechanisms for requirements
and designs (state machines, Z), proof systems (natural deduction, term
rewriting, model checking), static analysis (abstract interpretation,
inspections, fault-tree analysis), dynamic analysis (test oracles, executable
assertions, coverage metrics).
Prerequisites
CMSC 430.
Topics
Software requirements: formal descriptions based on state machines,
checking of global and user-specified properties, model checking.
Program verification and automated theorem proving.
Abstract data types: algebraic specification and
term rewriting.
