[Soot-list] 答复: Is it possible to perform verification over path?

[#DING SUN#]

Ya, thanks ! I will have a try first.

-----邮件原件-----
发件人: eric.bodden at googlemail.com [mailto:eric.bodden at googlemail.com] 代表 Eric Bodden
发送时间: 2011年7月19日 22:45
收件人: #DING SUN#
抄送: Soot list
主题: Re: [Soot-list] Is it possible to perform verification over path?

Sure, that should be possible.

Clara also takes as input "heuristics" as you call them. They are just written in a special data format - AspectJ aspects with some additional annotation.

This may not be the representation you envision but it should certainly be able to implement something along those lines for the properties you are interested in.

Eric

On 19 July 2011 09:08, #DING SUN# <DING0037 at e.ntu.edu.sg> wrote:
> Hi，Eric，
>     Yes, it's actually is what you mentioned in soot: to verify the property of some object. But I may need more , like heuristics or build-in theories telling which kind of objects or properties need to checked.
>     For example,  the software :Esc/java or Findbugs.  They are designed to automatically verify bugs in a java program. The bug list is predefined by heuristics, like null reference, out boundary exception, divide zero, etc.
>     I'm wondering whether it is possible to do the similar things over paths.
>
> Best Regards,
> Ding Sun
>
> On Jul 19, 2011, at 6:33 PM, "Eric Bodden" <bodden at st.informatik.tu-darmstadt.de> wrote:
>
>> Hi Ding Sun.
>>
>> It's certainly possible, butI guess your question is really if anyone 
>> has done this before, right?
>>
>> Regarding verification, I am not exactly sure what you mean. In my 
>> PhD Thesis I have used Soot to verify finite-state properties of 
>> objects, such as "don't write to a file after closing it". This is 
>> flow-sensitive and path-sensitive. It's implemented as an extension 
>> to Soot, called Clara: http://bodden.de/clara/
>>
>> I am not aware of Soot being used for test generation but there may 
>> be people who have done this. Maybe somebody else on this list can 
>> comment on this.
>>
>> Eric
>>
>> On 18 July 2011 21:54, #DING SUN# <DING0037 at e.ntu.edu.sg> wrote:
>>> Dear All,
>>>       I'm wondering whether it is possible to connect soot with other static analysis tools to perform verification over program path? Or generate test case over a path?
>>>
>>> Best Regards,
>>> Ding Sun
>>> _______________________________________________
>>> Soot-list mailing list
>>> Soot-list at sable.mcgill.ca
>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>>
>>
>>
>>
>> --
>> Dr. Eric Bodden, http://bodden.de/
>> Principal Investigator in Secure Services at CASED Coordinator of the 
>> CASED Advisory Board of Study Affairs PostDoc at Software Technology 
>> Group, Technische Universität Darmstadt
>> Tel: +49 6151 16-5478    Fax: +49 6151 16-5410 Mailing Address: S2|02 
>> A209, Hochschulstraße 10, 64289 Darmstadt
>



--
Dr. Eric Bodden, http://bodden.de/
Principal Investigator in Secure Services at CASED Coordinator of the CASED Advisory Board of Study Affairs PostDoc at Software Technology Group, Technische Universität Darmstadt
Tel: +49 6151 16-5478    Fax: +49 6151 16-5410 Mailing Address: S2|02 A209, Hochschulstraße 10, 64289 Darmstadt