F20CV - Computer-aided Verification

Course leader(s):

• Kathrin Stark (Edinburgh, September)
• To be announced (Edinburgh, September)

Syllabus

1. Overview of the history of mathematical logic (1.1 Overview of the history of mathematical logic representations, propositional and predicate logic, semantics, formal reasoning interactive and automated reasoning, theorem provers, combinatorial explosion, different reasoning techniques, adequacy of formalisations)

2. Concepts of formal logic (2.1 Concepts of formal logic, i.e. inference rules, proof techniques, inductive reasoning, inductive predicates, deductive reasoning, formal semantics)

3. Proofs and correctness (3.1 Proof and correctness: formalisation of proof, inference rules and resolution, unification, equational reasoning, combinatorial explosion, search algorithms.)

4. Proof techniques (4.1 Proof techniques: rewrite rules, human proofs, decision procedures, meta-level inference.)

5. Student Project (5.1 Student Project with different starting points, starting with fixed theorems to prove and then allowing the students to explore more freely.)

Learning outcomes

By the end of the course, students should be able to do the following:

• Analyse critically the work of peers, providing constructive feedback.
• discuss critically fundamental concepts in formal logic, such as proof theory or axiomatic systems.
• employ an interactive theorem prover (e.g., Lean, Coq, Agda, or Isabelle) proficiently to represent mathematical statements, verify program specifications, and construct rigorous proofs.
• apply advanced features in functional programming, such as dependent types, to solve complex problems and construct robust proofs.
• inspect research papers from the field of theorem proving, demonstrating the ability to present key findings coherently.
• assess the correctness of programs and mathematical models, ensuring their adherence to specifications.
• contrast mathematical ideas and proof methodologies effectively in both written and oral forms.
• plan a multi-week project on a topic in theorem proving, showcasing autonomy and effective time management.

Further details

Curriculum explorer: Click here

SCQF Level: 10

Credits: 15