Shavuot inspired post: 5 formal methods related areas

Today in the evening starts Shavuot (feast of the weeks), the Jewish holiday that occurs 7 weeks after Passover and commemorates receiving the Torah (at Mount Sinai). The typical movie image includes Moses going down the mountain with the 10 commandments written in stone, 5 commandments on each.

Inspired by this, I will post here 5 (one tablet of stone) formal methods related areas I intend to write about in this blog:

1. Pre and post conditions: hoare logic, design by contract, software implementing these ideas, extensions
2. Model checking: temporal logic, algorithms, bdds, compositional verification, abstraction-refinement
3. Static analysis: overapproximation, abstract interpretation
4. Sat-based verification: algorithms, smt, bounded model checking
5. Parallel programming formal models: consistency models, synchronization primitives, languages (csp, ccs, lotos)

I will probably continue writing about other topics as well, such as AOP in the context of Software Engineering, Modularity..
However I hope to cover most of the topics mentioned above (given enough time)

Hag Sameach!