Formal Verification of Software

There is a plethora of Formal Verification tools for software verification in recent years. It should be pointed out that a lot of effort has been invested on formal verification of hardware, and it remains a challenging problem. Software verification is essentially more complex. In hardware we have at least a finite state space (they are all finite state machines); but in software the state space may not be bounded anymore. One couldn't help but wonder why people are rushing to solve a much harder problem while they couldn't solve the easier sibling. The truth lies in the return on investment. Although formal verification of hardware is still unsolved, a lot of easier subproblems have been worked on, and some (like equivalence checking) have been widely deployed in industry. Meanwhile, formal verification of software remains mostly untouched. So there are a lot of low hanging fruits (in the research field) if one simply work on software verification and perhaps borrow/transform some good techniques from the hardware side. At the end of the day, software verification remains a much more difficult problem. So those late to the game are going to be very disappointed after all this gold rush is over.