On Sat, Oct 25, 2008 at 3:17 AM, Russell Wallace <[EMAIL PROTECTED]> wrote: > On Fri, Oct 24, 2008 at 7:42 PM, Vladimir Nesov <[EMAIL PROTECTED]> wrote: >> This general sentiment doesn't help if I don't know what to do specifically. > > Well, given a C/C++ program that does have buffer overrun or stray > pointer bugs, there will typically be a logical proof of this fact; > current theorem provers are typically not able to discover this proof, > but that doesn't rule out the possibility of writing a program that > can. (If this doesn't clarify, then I'm probably misunderstanding your > question, in which case can you rephrase?) >
There are systems that do just that, constructing models of a program and representing conditions of absence of a bug as huge formulas. They work with various limitations, theorem-prover based systems using counterexample-driven abstraction refinement (the most semantically accurate brute force models) able to work with programs of up to about tens of thousands lines of code. They don't scale. And they don't even handle loops well. Then there are ways to make anaylsis more scaleable or precise, usually in a tradeoff. The most of what used to be AI that enters this scene are theorem provers (that don't promise to solve all the problems), and cosmetic statistical analyses here and there. What I see as potential way of AI in program analysis is cracking abstract interpretation, automatically inventing invariants and proving that they hold, using these invariants to interface between results of analysis in different parts of the program and to answer the questions posed before analysis. This task has interesting similarities with summarizing world-model, where you need to perform inference on a huge network of elements of physical reality (start with physical laws, if they were simple, or chess rules in a chess game), basically by dynamically applying summarizing events, matching simplified models. But it all looks almost AI-complete. -- Vladimir Nesov [EMAIL PROTECTED] http://causalityrelay.wordpress.com/ ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
