On Sat, Oct 25, 2008 at 9:29 AM, Vladimir Nesov <[EMAIL PROTECTED]> wrote: > 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.
Thanks, that was about where I understood the state-of-the-art to be. > 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. Yes, that's the sort of thing I have in mind. > But it all looks almost AI-complete. It's a very hard problem, but it's a long way short of AI complete. I think it's worth aiming for as an intermediate stage between the current state of the art and "good morning Dr. Chandra". ------------------------------------------- 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
