CISC/CMPE422, CISC835: Formal Methods in Software Engineering (Fall 2019)
Detailed course content
[
Home
] [
Content
] [
Schedule
] [
Readings
] [
Assignments
]
Introduction, motivation and overview
Background
Languages: Propositional and first-order logic
Analysis techniques: theorem proving
Tools:
Jape
Formal specifications and their analysis
Introduction to object modeling
Languages: Class diagrams, first-order logic with relational calculus
Analysis techniques: constraint solving
Tools:
Alloy Constraint Checker
Finite state machines and their analysis
Languages: Finite state machines, temporal logic (Computation Tree Logic)
Analysis techniques: state space exploration (i.e., CTL model checking)
Tools:
nuSMV