Syllabus
Office:
Office hours:
Email:
Phone:
|
WVH 346
by appointment
pete@ccs
617-373-3694
|
Course number:
Web page:
Locations:
|
CS G369
http://www.ccs.neu.edu/home/pete/courses/Topics-in-Formal-Methods/2008-Fall/
Tu/Fri 11:45-1:25, 166 West Village Bldg H
|
Course Description
This is a course on the current state-of-the-art in a few
selected topics in formal methods. The topics are: termination,
satisfiability modulo theories, theorem proving, and refinement
(see below for more information). The course is an advanced
PhD-level course. It is appropriate for PhD students, and,
perhaps, for gifted and motivated undergraduate and masters
students. Please contact me if you are not a PhD student and want
to take the class; you will need my permission. The major goal is
the completion of a project that extends the state-of-the-art and
leads to publishable results.
Teaching Philosophy
My goal is to help you develop into critical,
independent-thinking, and creative scientists. In this course, I
will try to do this by giving you opportunities to grapple with
and gain technical mastery of selected research topics in formal
methods. We will delve deeply into a few selected topics, and
the main goal will for you to complete a project that leads to
new, publishable results.
During lectures I try to explain, clarify, emphasize,
summarize, encourage, and motivate. I can also answer questions,
lead discussions, and ask questions. In class you have an
opportunity to test your understanding, so things work best if
you come to class prepared. We can then focus on the interesting
issues, rather than on covering material that you could just as
easily find in the readings.
Textbooks
We are mostly going to be reading research papers, but it may be
useful for those of you who aren't familiar with ACL2 to get the
following book.
-
Computer-Aided
Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother
Moore. Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7744-3)
Note: A paperback version is available on
the
Web. This is much cheaper than the hardcover
version.
Tools
Install the ACL2 Sedan.
Grading
Your grade will be based on the following.
Class Participation:
Presentations & Homework:
Project:
|
20%
30%
50%
|
Tentative Syllabus
Here is an overview of the material that I would like to cover.
I reserve the right to make modifications based on the interests
of the class and/or time constraints.
- Termination Analysis
- Basic Set Theory: ordinals, well-founded and well-ordered relations
- Measure functions and their use in ACL2
- Size-change principle
- Calling-context graphs
- Methods from term-rewriting
- Decision procedures
- Using SAT solvers for termination analysis
- Satisfiability modulo theories
- Basic Framework
- Congruence Closure
- Linear arithmetic
- Arrays
- Scheduling
- Pseudo-boolean solving
- Theorem Proving
- Review of First Order Logic
- The ACL2 Theorem Prover
- Term rewriting
- Priority-based rewriting
- Combining SMT & theorem proving
- Refinement & Abstraction
- Simulation & bisimulation
- Stuttering
- Refinement
- Conservative abstractions
- Reactive systems
- Temporal calculi, mu-calculus, fixpoints
- Refinement and its relation to temporal logic
Last modified: Fri Sep 12 09:20:55 EDT 2008