Instructor: Chandrasekhar Boyapati
The motivation behind this course is the need for reliable and secure software. Software has become pervasive in our civilian infrastructure. All activities including transportation, telecommunications, energy, medicine, and banking rely on the correct working of software systems. Consequently, the problem of making software reliable and secure has become one of today's most important challenges. Multi-hundred-million-dollar space projects are interrupted by software glitches, power-grid failures are caused by bugs in software, and new security exploits are announced daily. Software reliability is crucial in critical systems, where failures can lead to loss of life---with risks ranging from a few individuals (anti-lock braking systems and airbag-deployment systems) to a few hundred (aircraft collision-avoidance systems) to tens of thousands (nuclear reactors and weapons systems). Software reliability also impacts security because buggy code underlies most security violations and progress in making systems more reliable will make them more resistant to deliberate attack as well. Moreover, software reliability has a significant impact on economy. Studies estimate that bugs in software cost businesses worldwide about $175 billion annually.
This course covers basic and advanced topics in programming languages, and shows how good programming languages and tools can significantly improve the reliability and security of software systems. This course has three objectives: 1) To understand fundamental concepts in programming languages, 2) To study some recent topics and trends in PL research, and 3) To gain experience planning and carrying out a modest PL research project.
Please see the course web page for more information.
All books are recommended:
1) Pierce, Benjamin C. Types and Programming Languages. Cambridge, MA: MIT Press, 2002.
2) Nielson, Flemming, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Berlin: Springer, 2005.
3) Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. Cambridge, MA. MIT Press, 2001.
- Mathematical Foundations: Sets, Relations, Functions, Inductive Proof Techniques
- Defining a Programming Language: Syntax and Semantics
- Making a Programming Language and Programs Safe
- Type Systems: Type Safety, Type System for Java, Recent Advances in Type Systems for Preventing Data Races, Deadlocks, Memory Errors, Information Leaks, Protocol Errors, etc.
- Program Analysis: Dataflow Analysis, Abstract Interpretation, Pointer Analysis, Shape Analysis, Recent Advances
- Software Model Checking: Bounded Exhaustive Testing, Partial Order Reduction, Abstraction and Counter Example Guided Refinement, Recent Advances
- Theorem Proving: Hoare Logic, Specification Languages, Interactive & Automated Theorem Proving, Recent Advances