7
$\begingroup$

I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also recommendations which books and articles to read next.

My goal is to be able to judge what parts of formal verification I could apply to my job as a software/network engineer. So if the overview had a practical slant it would be a plus. But I also don't mind theory at all since I have a rather solid background in pure maths.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ This other question might prove useful for you :), specially the mentions to the Software Foundations series. $\endgroup$
    – Aristu
    Dec 9, 2018 at 22:55
  • 1
    $\begingroup$ Also, it might be interesting to take a look on Type Driven Development. $\endgroup$
    – Aristu
    Dec 9, 2018 at 23:14
  • $\begingroup$ @Aristu: Thanks a lot for these very helpful links! $\endgroup$
    – eins6180
    Dec 10, 2018 at 21:49
  • $\begingroup$ Lastly, Model Checking seems like an interesting subject itself, but I know nothing about it. There seems to be some really recent lectures from Aachen though. $\endgroup$
    – Aristu
    Dec 10, 2018 at 22:48
  • 2
    $\begingroup$ This is a very good question. As I understand this is a question of why there is so little use of formal methods in the practice software development, ... or is there? The Wikipedia article is certainly not very well written and the Industry Use section is patchy at best. I'd love to read answers here and perhaps contribute some links or anecdotes. $\endgroup$
    – Dima Chubarov
    Dec 11, 2018 at 14:11

1 Answer 1

Reset to default
4
$\begingroup$

My goal is to be able to judge what parts of formal verification I could apply to my job as a software/network engineer.

If you plan to use formal verification as black boxes, then I would suggest using some tools to have an idea how they work. Here are some open source tools:

If you want to understand their basics, you can start with the book "Principal of Program Analysis". It covers many basic topics from Type Theory to Abstract Interpretation etc.

The book doesn't discuss anything deeply. For example, it doesn't discuss any abstract domains, the key part in abstract interpretation. Recent topics such as separation logic, which Facebook Infer is based on, are not covered either.

If you want to learn advanced topics, the only way is to read the proceedings of top conferences, e.g. POPL, PLDI, CAV, VMCAI, SAS, ICSE, FSE, ASE, ISSTA, etc etc.

A comment by @DmitriChubarov

As I understand this is a question of why there is so little use of formal methods in the practice software development, ... or is there?

There are companies that are earning hundreds of millions a quarter by selling static analysis tools (I work for one of them), so I believe the number of companies that use formal verification is not little at all.

Improve this answer
$\endgroup$

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.