Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Nice to see my field get some press.

I will say, though, that static analysis is still very much an immature technology. Look for it to be much, much better in a decade or so.



> Look for it to be much, much better in a decade or so.

Why is that? Are there big unsolved problems or is it more of a grinding away at little things?


Static code analysis is extremely difficult. You have to have a notion of what an "error" is, and the complexity of interaction between different pieces of a codebase grows exponentially, making feasible analysis of big projects very difficult without throwing in heuristics to simplify the analysis at a cost of loss of precision.


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).


There are some algorithms and techniques that will improve static analysis in a greater than linear fashion (however, I wouldn't guarantee exponentially).

see Model Verification: http://en.wikipedia.org/wiki/Kripke_structure_(model_checkin... and SMT solving: http://en.wikipedia.org/wiki/SMT_solver


Well, unfortunately most interesting static analysis problems are undecidable. There can be no "general" solution.

What we have in practice are approximations and heuristics; over time we will develop better approximations for the kinds of code people write in practice. Unfortunately fragility of analysis will always be a problem; if you change your code just a little bit then reasoning may fail.

As someone who has spent years doing research on shape analysis my personal belief is that the dream of a fully automated "find my bugs" static analysis is unrealistic. Some of the problems you must solve to analyze the heap, say, are very hard indeed.

We need to think more about the interactions between language design and verification, rather than hoping that people will build better tools to analyze existing code. Strong typing (e.g., the Hindley-Milner type system) is one example of a sweet spot that demonstrates how language design (type annotation, type declarations) interacts with tools (type inference, type checking). Type systems are some of the most widely used bug finding tools today. Trying to build verification tools without considering language design is always going to be difficult.




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

Search: