3
$\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.

$\endgroup$
  • $\begingroup$ This other question might prove useful for you :), specially the mentions to the Software Foundations series. $\endgroup$ – Aristu Dec 9 '18 at 22:55
  • $\begingroup$ Also, it might be interesting to take a look on Type Driven Development. $\endgroup$ – Aristu Dec 9 '18 at 23:14
  • $\begingroup$ @Aristu: Thanks a lot for these very helpful links! $\endgroup$ – eins6180 Dec 10 '18 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 '18 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$ – Dmitri Chubarov Dec 11 '18 at 14:11
2
$\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.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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