P: C241. P or C: C212. Fundamentals of formal language theory, computation models and computability, the limits of computability and feasibility, and program verification. Credit not given for both A595 and B401. Undergraduate CS majors should take B401. May be credited towards the PhD Minor, graduate credit available for CS M.S. candidates with special permission.