This course is designed for students familiar with basic programming concepts such as loops, variables, arrays, and functions. Students will learn the techniques for ensuring the correctness of imperative programs and how to write code that is correct by design. The course is conducted using C0, a safe variant of C, and students will gain exposure to data structures and algorithms used in computer science. The ability to write correct code, assess program performance, and compare solutions to meet deployment constraints are the main skills students will acquire through this course. Students must have passed 15-112 or equivalent to enroll, and should take mathematical courses alongside it.
https://www.cs.cmu.edu/~15122/about.shtml