Software Formal Verification, SNU M1522.007300, 2025 Fall

• Instructor: Prof. Chung-Kil Hur
  • Email address: gil.hur@sf.snu.ac.kr
  • Office: 302-426
• TA: Taeyoung Yoon
  • Email address: sf@sf.snu.ac.kr
    • When sending TA an email,
      • The subject (제목) must start with [SF]
      • Your name and student ID must be included in the body (본문)
  • Office: 302-317
• Class material: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
• Please use email to ask questions (Do not use GitHub Issues)

Grading(tentative)

• Attendance: 5%
• Mid-term: 45%
• Final: 50%

Announcements

• Oct. 21: Assignment 1 is uploaded.
• Oct. 27: Midterm exam will be held in Nov. 1. Please check instructions through this page.
• Oct. 31: Assignment 2 and 3 are uploaded.
• Oct. 31: Sample of the midterm exam is uploaded - the format will be similar in our upcoming midterm. Check the exam directory.
• Nov. 24: Midterm scores are out in etl. Please claim until Nov. 28.
• Dec. 07: Assignment 4 is uploaded. As usual, these files are not to be graded but provided as a supplementary material for self-study. Sidenote: SFRev.v is a file for reversing an array with solution provided.
• Dec. 10: Sample of the final exam and the solution is uploaded. Check the final directory.
• Dec. 17: Midterm scores are out in etl. Please claim until Nov. 18.

Assignments

• Download skeleton code and replace FILL_IN_HERE with your code in P**.v.
• Each assignment have forbidden keyword in forbidden.txt. Try not to use those keywords.
• We will not be grading assignments - feel free to complete them and test your understanding about the materials dealt in the classes.
• Consult to the TA if you have any questions.

Coq

• Install Rocq 9.0.0.

  • Using an installer (Windows, MacOS)

    • Download Binaries and install it.
    • Using Coq in Windows could have unexpected, unsupported problem. TA cannot help you in this case.

  • Using OPAM (Linux / MacOS) (recommended)

    • OPAM is OCaml package manager, and you can use it to install Coq in Linux.
    • See https://coq.inria.fr/opam-using.html.

  • Using brew (MacOS)

    • Run brew install coq.
    • Note this wouldn't install CoqIDE.

• Install IDE for Coq.

  • CoqIDE: installed by default.
  • VS Code: VSCoq. Follow the setup instructions.
    • VsCoq v2.x is new and shows unstableness. If you have trouble using VsCoq v2, downgrade to VsCoq Legacy (v0.3.9).
    • Basic command (based on vscoq github page)
      • alt + down : interpret next step
      • alt + up : return to previous step
      • alt + right : interpret to right before cursor
      • alt + end : interpret until end of file
      • alt + home : reset
      • more commands : F1 & type Coq:
        • example : Coq: Prompt Check
  • Emacs: Company-Coq. Follow the setup instructions.
    • If it shows Searching for program No such file or directory coqtop error, please add (custom-set-variables '(coq-prog-name "PATH/TO/coqtop")) to .emacs file.
    • In case of MacOS, coqtop is at /Applications/CoqIDE_8.9.1.app/Contents/Resources/bin/.

• Tips for those using Windows

  • Using WSL allows you work on linux.
  • In WSL, WSL extension of VS Code is recommended.

• It is likely that you will use your own laptop in mid-term and final exam. If you do not have a laptop or cannot install Coq on it, please let the TA know.

Tactics

• You can look up manuals about Basic tactics, Automatic solver, and Ltac for more information about proof techniques.