|
Coverings the development of software – with emphasis on rigour and formality. Concepts covered include the foundations for deductive verification and model checking techniques with emphasis on the underlying logics used, state of the art tools, research developments and usage in industry. Topics include Design by Contract; Hoare Logic, Temporal Logic, Separation Logic; Intermediate Verification Languages such as Boogie or Why3, Specification Languages such as OCL, JML, Eiffel, Spec# or Event-B; Refinement, SMT Solvers, Verification of concurrent software and model checking.
|