Modular Heap Shape Analysis for Java Programs

Modular Heap Shape Analysis for Java Programs

Florian Frohn1

1 RWTH

Ju?rgen Giesl1

Aachen University, Germany

September 19, 2017

1/9

AProVE and Java

AProVE: termination and complexity analysis tool for Java

2/9

AProVE and Java

AProVE: termination and complexity analysis tool for Java

public void add ( Object x ) {

List l = this ;

while ( l . n != null ) {

l = l.n;

}

List ll = new List ();

l . n = ll ;

ll . v = x ;

}

2/9

AProVE and Java

AProVE: termination and complexity analysis tool for Java

public void add ( Object x ) {

List l = this ;

while ( l . n != null ) {

l = l.n;

}

List ll = new List ();

l . n = ll ;

ll . v = x ;

}

sophisticated heap shape analysis

2/9

AProVE and Java

AProVE: termination and complexity analysis tool for Java

public void add ( Object x ) {

List l = this ;

while ( l . n != null ) {

l = l.n;

}

List ll = new List ();

l . n = ll ;

ll . v = x ;

}

sophisticated heap shape analysis

lacks modularity

2/9

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download