Hacker News new | past | comments | ask | show | jobs | submit login

It's useful to make a distinction between the "sound" static analyses Matt Might posted about and heuristic-based, or "pragmatic" analyses.

Cousot's Analysis of Signs is sound. It can fail by returning {-,0,+}. However, when it succeeds, it does make guarantees. If it returns {0} for an integer, then it has proven that that integer will always and only have the value 0. Furthermore, if that integer can be 0, it is guaranteed the analysis will return a set containing 0.

Pragmatic analyses have no such guarantees; if a pragmatic analysis of signs returns {0}, then anything could happen. They are "pragmatic" in that their value is determined by how correlated their output is with the answer on real programs; there are no theorems to prove about them.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: