Select the desired Level or Schedule Type to find available classes for the course. |
CS 4830 - System Specification, Verification, and Synthesis |
Covers the fundamental topics in formal modeling and specification (transition systems, temporal logic, regular and omega-regular languages, safety and liveness properties, etc.); computer-aided verification (state-space exploration, model checking, bounded-model checking, binary-decision diagrams, symbolic model checking, etc.); compositionality and assume-guarantee reasoning; contracts; and component-based design. Also covers fundamental topics in computer-aided synthesis of correct-by-construction systems, starting from high-level formal specifications or from example scenarios. Designing large and complex systems (digital circuits, embedded control systems such as automated vehicles, computerized healthcare devices such as pacemakers, cyber-physical systems such as automated intersections, etc.) and their software cannot be done by hand. Instead, designers use computer-aided techniques that allow them to build system models and verify correctness of the design before the real system is actually built.
4.000 Credit hours 4.000 Lecture hours Levels: Undergraduate Schedule Types: Lecture Computer Science Department Course Attributes: Computer&Info Sci Restrictions: Must be enrolled in one of the following Levels: Undergraduate Prerequisites: Undergraduate level CS 3000 Minimum Grade of D- |
Return to Previous | New Search |