Deductive Software Verification II

29 Setembro 2021, 16:30 • Antónia Lopes

Deductive Software Verification II

• Hoare logic (cont'd):
• Right weakening, skip, sequential composition, conditionals, loops
• Proving termination
• Soundness and completeness
• Pros & Cons

Exercises on Hoare Calculus II

29 Setembro 2021, 15:00 • Antónia Lopes

Exercises1 (Hoare Calculus) : 2&3(t), {n≥0}Fact{f=n!} 

Execises on Hoare Calculus

22 Setembro 2021, 18:30 • Antónia Lopes

Exercises1 (Hoare Calculus) : 1, 2 (a)-(j)

Deductive Software Verification I

22 Setembro 2021, 16:30 • Antónia Lopes

Deductive Software Verification I

• Logic and Proof systems
  • Validity, Satisfiability
  • Proof System and Formal theory, Soundness, Completeness
• Hoare logic:
  • Program analysis as a validity checking problem
  • Partial vs total correctness
  • Assignment, left strengthening

Execises on Hoare Calculus

22 Setembro 2021, 15:00 • Antónia Lopes

Exercises1 (Hoare Calculus) : 1, 2 (a)-(j)