Instructor: Dr. Ali Ebnenasir
Office: 206 Rekhi Hall
Phone: 487-4372


Textbook: "Software Abstractions: Logic, Language, and Analysis", by Daniel Jackson, The MIT Press, revised edition, February 2012. (ISBN: 0262017156)

Meeting time: Tuesday/Thursday 14:05-15:20

Meeting room: 126 Fisher Hall

Office Hours: Wed.  3:00 - 4:00pm, and by appointment†††††††

Prerequisites: Team Software Project (CS3141) and Formal Models of Computation (CS3311). This course requires a sound background in discrete math and finite state machines along with general knowledge of object-oriented programming.

Web page:

Description: The focus of this course is on formal modeling of software systems, automated analysis, verification, and design. After taking this course, the students will have the skills to (1) use one or more formal specifications languages, (2) use tools for automated analysis and verification of models, and  (3) apply one or two well-known design methodologies.     

Grading Policy:

         Individual assignments ††††††††††††† 30%

         Group assignments ††††††††††††††††††† 40%

         Reading assignments†††††††††††††††††††20%

         Team work††††††††††††††††††††††††† 10%

         Presentations†††††††††††††††††††††††††††††† 5%†† (extra credit)


Late Assignment Policy:†††††††††† †††††††††††

         Grace period: Throughout the semester, only one assignment can be late for at most 3 days!

         If you are late on an assignment after you have used your grace period, you will lose 20% of the total score of that assignment for each day you are late.


Academic Integrity Policy:  Please read MTUís general policy on Academic Integrity and sanctions considered for Academic Dishonesty. Here is the URL: