VMCAI'10:An Analysis of Permutations in Arrays

This paper try to reason the content of data structure independent of its particular structure, for example, the sorted array has the same set of data as that of before sorting.

I also consider such problem before, but not work into it.

Basically, there are 3 types of problem
1 traditional shape analysis, such as the size and shape of data structure
2 extend above approach to deal with the relation between content and position, such as comparing two array or sortness.
3 this paper approach.

following paper even prove that such problem can't be expressed by first order logic.
Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. J. ACM 27(1) (January 1980)

VIMCAI'10:RGSep Action Inference

This paper integrate the rely-guarantee with separation logic to deal with memory problem and concurency

actually, rely is a over-approximation, while guarantee is under-approximation.

VMCAI'10: Collections, Cardinalities, and Relations

This paper propose the QFBAPA-REL logic to describe the Cardinalities relation between collection like data structrue, such as list , set multi set and so on.

It can deal with problem such as "inserting an element into tree and prove that the size is increase by 1"

verification condition

I finally find out what is verification condition.

For a program properly annotated with loop invariant and initial condition assertion. A logic formula is generated to express the relation between these assertion and invariants.


This logic formula is verification condition.

my ICCAD'09 paper

I forget to update that, my paper had been accepted by ICCAD'09,
Synthesizing Complementary Circuits Automatically

please refer to my home page for more detail of my researching work progress.

VIMCAI'10 : Considerate Reasoning and the Composite Design Pattern

the major problem of verification of imperative oo program is the complex heap structure.
One approach is the seperation logic alike approachs, including dynamic frame.

Other approaches build on the concept of object invariant, and usually sup-
port some variation of visible states semantics (with the notable exception of the
Boogie methodology [3]). In visible states semantics, object invariants should
hold at the pre- and post-states of method calls, but may be temporarily bro-
ken during method execution. Various refinements have been proposed, usually
based on some notion of ownership - a way of imposing structure on the heap by
requiring that one object is encapsulated within another.

But many programming style are not in ownership style. so Considerate Reasoning is proposed.

It is based on visible states semantics; in order to support methods meant
to fix invariants, it introduces the specification construct broken. Invariants de-
clared “broken”in a method specification are not expected to hold before calls to
the corresponding methods, but are expected to be re-established by these meth-
ods. All invariants are expected to hold at the end of a method execution.


I think such appraoch are meant to trying to find another type of ownership alike encapsule.

Some referred works

POPL'05 Separation Logic and Abstraction

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.5332&rep=rep1&type=pdf

this paper combine seperation logic with module abstaction in its reasoning rules for the first time.

FM'06 : Dynamic Frames: Support for Framing,Dependencies and Sharing Without Restrictions

This paper first state the frame approach that explictly specify the set of variables that modified by a statements.

andthen they want to invoke private viariable that is widely used in current object oriented program language, which is invisible to specification writter. so they chose to invoke specification variable for implementor, such that he can write the relation between spec var and private var.

but such approach suffer from alias pointer that can' be modeled.

so he propose an explictly approach to state the modification and preservation of sertain object.

such approach is called dynamic frame

But I think all these approaches are similar to separation logic that try to avoid specification of unmodified objects.

ICCAD'09:Interpolating Functions from Large Boolean Relations

This paper use interpolation to characterize function from huge relation
http://alcom.ee.ntu.edu.tw/publications/iccad09-r2f.pdf

This solve the problem of my ICCAD'09 paper, that can't characterizeboolean function of complementary circuit efficiently.

I need to integrate this approach into my framework.