|♦ CSCI P415/515||Tue Sep 27 11:43:56 EDT 2011 [SDJ]|
|Index news info homework notes description topics background text goals grading|
|What's New -- Look here regularly for postings|
|may 7, 2012|| |
P415 Introduction to Verification (3 cr.)
P: C311 or C521.
Tools and techniques for rigorous reasoning about programs and systems.
Safety, reliability, security, and other design-critical applications.
Decision algorithms. Projects involving the use of automated reasoning tools,
such as model checkers, theorem provers, and program transformers.
P515 Specification and Verification (3 cr.) P: C311 or C521. Tools and techniques for rigorous reasoning about programs and systems. Safety, reliability, security, and other design-critical applications. Decision algorithms. Projects involving the use of automated reasoning tools, such as model checkers, theorem provers, and program transformers.
Credit not given for both P415 and P515.
If you have not taken the prerequisite course, you may still be allowed to enroll. Contact the instructor. See also the Background section below.
Tue/Thu 1:00 PM – 2:15 PM, Ballentine Hall (BH) 005
office hours: Tue/Thu 2:30 PM – 3:30 PM, Lindley Hall 330F
Students are welcome in my office any time my door is open
|Homework – 10 to 12 weekly assignments & readings. (Due dates are advisory. At certain points in the course, the Instructor will
"sweep" your work space to review where you are with the homework. These sweeps are
usually announced 4–7 days in advance.
Feel free to work ahead, but be advised that some assignments
may be changed or extended as the semester progresses.)
|Notes – There is no required textbook; lecture notes, references, suggersted readings, etc. are posted here|
– Up to half of your course grade is based on a project,
assigned around the eighth week.
Team projects are strongly encouraged.
This course introduces methods for performing logical analysis of programs and systems to verify their correctness. It lays a foundation for software engineering in critical applications where a high degree of certainty is needed that the programs realize a specified function or behavior. The broader aim is to show that programming can be done rigorously, when necessary, and is not merely a "craft" based on years of experience. More generally, this course allows students to take a retrospective look at what they have learned in prior classes and tie together concepts that may seem disconnected the first time they are seen.
The course centers on automated tools used in practice to prove properties correctness properties about programs and systems. The emphasis is on gaining exposure and skills in the use of automated reasoning tools in the design process. Participants learn to use two such tools, a theorem proving environment and a model checker, and undertake a project involving the use (or implementation) of these tools. Time permitting we also investigate how these tools work, looking at their underlying algorithms and data structures, as well as the relevant theory. However, the emphasis is on doing, in order to gain insight and motivate theoretical aspects.
An important byproduct of this experience is a fundamental understanding of predicate logic. This knowledge comes "for free" in the sense that it is the medium in which the reasoning tools operate. Thus, comprehension of inference rules and formal proofs is assimilated through their active, computer-validated use.
Throughout the course, participants read and discuss writings related to verification including position papers, accident reports, and general articles about formal methods. The purpose is to develop a perspective on design, the role of verification in practice, the kinds of problems this technology addresses, and the kinds it does not.
Participants learn how to use reasoning tools for specification analysis and implementation verification, examine the underlying algorithms and data structures for high performance decision procedures, and survey selected reports, case studies, and essays relating to catestrophic design errors.
Verification is the task of determining whether an implementation satisfies its specification. This has traditionally been done by submitting the design (a program or hardware simulation) to a battery of test inputs and comparing generated with expected outputs. As systems get larger, the number of possible tests is astronmically high, so this experimental style of verification can cover only a tiny fraction of the possibilites. Formal verification is the use of decision procedures to completely characterize a design; it is equivalent to exhaustive testing for a particular property.
In design critical applications, the considerable effort of formal verification is worthwhile; and, as the needed tools and expertise develop, broader classes of design are subject to this methodology. The focus of this course is on the technology of verification, how it is built and used today, and what it will look like in the future.
Thus, if you have completed the core courses of a computer science/engineering major and have an interest in systems, theory, hardware/architecture, software engineering, logic, programming languages, or have an interest in critical design applications you should consider yourself qualified. Experience indicates that successful people in this field have good mathematical skills and a keen interest in applications.
"Do I need C311?" Because of scheduling issues, a significant number of undergraduate Seniors ask permission to take this course concurrently with C311 (normally a prerequisite). Having tracked these students over the years, I have found that strong students have sufficient aptitudes and experience to succeed (not necessarily with an A) in this course while taking C311 at the same time. The topical content C311 is less significant than the methodogical content. However, I do assume in my lectures that students have a basic understanding of symbolic programing languages (e.g. Scheme) and recursive programming.
Formal analysis does not see widespread use in practice, but areas of application are expanding. It is not my goal to prepare you for a career in verification, or even to convince you that formal verification is "the one true way." Rather, I want you to see that programming can be done rigorously, when it is necessary to do so. For most students, I believe this is an opportunity to consider what they have learned in retrospect, and to begin making sense of programming.
There are no required textbooks. The following references may be useful for students seeking background information or interested in advanced topics.
Individual and group projects are encouraged, and may continue for additional credit subsequent to this course. Such projects may include (but are not limited to) advanced case studies in verification, reeimplementation of tools for either expository or research purposes, integration of software packages in Scheme, and so on. Projects must be approved by the instructor, based on a written proposal as outlined in class.
Participants should expect to work independently to gain expertise with software tools, and creatively to explore applications within their domain of interest. They should expect to share their insights with others and collaborate on more ambitious projects. Although, it is unlikely that one can reach a high level of expertise in a single semester, motivated students will lay the groundwork for experimental research or toward technical skills that currently are in high demand.
Your grade will be determined by:
Students enrolled in the graduate section (P515) are required to do additional work, which may include:
Students are strongly encouraged to fill out course evaluations at the end of the semester, and will be given credit equivalent to approximately one homework assignment.