Eecs755
Contents
EECS 755 - System Requirements Modeling
The homepage for EECS 755 is migrating here from a traditional website. For now, please see EECS 755 for information about this course.
(Fall 2007, MW 12:30, Location 1131 Learned Hall)
Course Summary
Welcome to the EECS 755 wiki. Systems Requirements Modeling and Analysis is an advanced introduction to modern techniques for specification, verification and implementation of computer-based systems. Topics cover both software and hardware specification and verification. Students will be exposed in lecture to modeling and requirements analysis using formal specification languages that support symbolic verification and model checking.
Course Information
| Location | 1131 Learned Hall |
| Time | 12:30-1:45 MW |
| Prerequisites | Knowledge of at least one model programming language, data structures, and discrete mathematics. An undergraduate introduction to software engineering and/or computer systems design is helpful, but not required. |
| Required Texts | There are no required texts for this course. |
Instructor
| Offices | 2022 Eaton / 136 Nichols |
| palexand [at] eecs.ku.edu / alex [at] ittc.ku.edu | |
| Phone | 4-8833 / 4-7741 |
| Office Hours | TBD in 2022 Eaton, or by appointment |
| Online Schedule | 30 Boxes Online Schedule |
Syllabus
The course syllabus outlines policies such as grading breakdown, homework and project requirements, general policies and outlines course coverage. Please make sure you read through it at least once as it represents an informal contract for those taking the class.
Homework
Projects
Resources
Isabelle Home - Learn about all things Isabelle related. Isabelle is a multi-logic theorem prover that we use in class for our experimentation.
Proof General Home - Learn about all things Proof General related. Proof General is an emacs-based interface for theorem provers that we use in class as an interface to Isabelle.
PVS Home - PVS is a commercial grade theorem prover based on the sequent calculus that we have used extensively in our research. It has recently been placed in the public domain by SRI.
HOL Hme - HOL is a theorem prover based on the sequent calculus.
