Syllabus:
• Introduction to specification and programming languages for building secure and reliable software
• Logics for formal specification: Propositional logic, first-order logic and temporal logic
• Automatic proof techniques: SAT solving for propositional logic, SMT solving for first-order logic and theories, Bounded model-checking via SAT for temporal logic
• Program specification: Domain languages for behavioral specification, execution safety properties and functional properties, contract-based specification
• Static program verification: verification conditions for programs with contracts
• Dynamic program verification: runtime monitoring with contracts
• Introduction to formal methods for cyber-physical systems