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.
-
1$\begingroup$ This other question might prove useful for you :), specially the mentions to the Software Foundations series. $\endgroup$Schonfinkel– Schonfinkel2018年12月09日 22:55:51 +00:00Commented Dec 9, 2018 at 22:55
-
1$\begingroup$ Also, it might be interesting to take a look on Type Driven Development. $\endgroup$Schonfinkel– Schonfinkel2018年12月09日 23:14:06 +00:00Commented Dec 9, 2018 at 23:14
-
$\begingroup$ @Aristu: Thanks a lot for these very helpful links! $\endgroup$eins6180– eins61802018年12月10日 21:49:54 +00:00Commented 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$Schonfinkel– Schonfinkel2018年12月10日 22:48:38 +00:00Commented 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– Dima Chubarov2018年12月11日 14:11:00 +00:00Commented Dec 11, 2018 at 14:11
1 Answer 1
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:
- Error Prone of Google
- Nullaway of Uber
- Facebook Infer
- Ikos of NASA
- Java PathFinder developed by NASA, now maintained by community.
- Clang Static Analyzer of Apple
- ...
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.
Explore related questions
See similar questions with these tags.