The problem here is if hardware and algorithms for static analysis are improving at linear pace, applications are growing at least exponentially (if we add-in 3rd party libraries).
see Model Verification: http://en.wikipedia.org/wiki/Kripke_structure_(model_checkin... and SMT solving: http://en.wikipedia.org/wiki/SMT_solver