1
$\begingroup$

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are:

  1. Hoare Logic (for proving correctness of imperative programs)
  2. Linear Temporal Logic (to model-check programs)

What can be others?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

It is helpful to know basic mathematics and logic. But I would suggest that you go ahead and study software verification now, and learn additional logical background as needed. There is an unending literature on logic that one could potentially learn, but I think better to learn it on demand.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ On top of this, I would recommend getting a good modern proof assistant, like Lean or Coq, and just start playing with it. Prove some simple theorems that you already know. There is nothing quite like hands-on learning. $\endgroup$
    – Pseudonym ♦
    Dec 27, 2021 at 1:01
  • $\begingroup$ Thanks @Pseudonym. I know beginner level Haskell. Which proof assistant would suit me the most? I tried to explore Coq but the learning curve seemed very steep. $\endgroup$
    – a_fan
    Jan 22, 2022 at 12:23
  • $\begingroup$ I mean an interactive proof assistant! $\endgroup$
    – a_fan
    Jan 22, 2022 at 12:59
  • 2
    $\begingroup$ @a_fan I don't know, but consider signing up for this new beta SE: area51.stackexchange.com/proposals/126242/proof-assistants $\endgroup$
    – Pseudonym ♦
    Jan 23, 2022 at 4:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.