| |
Covering the development of software – with emphasis on rigour and formality. Concepts covered include the foundations for reasoning about software correctness with emphasis on the underlying logics used, state of the art tools, research developments and usage in industry. Topics include Design by Contract; Logics such as Hoare Logic, Temporal Logic and Separation Logic; Specification Languages such as OCL, JML, Eiffel, Dafny or Event-B; as well as verification techniques and tools used for reasoning about program correctness including deductive verification, model checking, refinement and use of SMT solvers.
|
RIGOROUS SOFTWARE PROCESS
