Experiments with Succinct Solvers

Mikael Buchholtz; Hanne Riis Nielson; Flemming Nielson

Experiments with Succinct Solvers

Mikael Buchholtz, Hanne Riis Nielson, Flemming Nielson

Research output: Book/Report › Report › Research › peer-review

61 Downloads (Pure)

Abstract

The Succinct Solver of Nielson and Seidl is based on the Alternation-free Least Fixed Point Logic and it is implemented in SML using a combination of recursion, continuations, prefix trees and memoisation. It is known that the actual formulation of the analysis has a great impact on the execution time of the solver and the aim of this note is to provide some insight into which formulations are better than others. The experiments addresses three general issues: (i) the order of the parameters of relations, (ii) the order of conjuncts in preconditions and (iii) the use of memoisation. The experiments are performed for Control Flow Analyses for Discretionary Ambients.

Original language	English

Publication status	Published - 2002

Access to Document

Imm919

http://www.imm.dtu.dk/pubdb/p.php?919

OpenUrl availability

Full text

Cite this

@book{92f7a095fa474b75aecb25d7aab510d0,

title = "Experiments with Succinct Solvers",

abstract = "The Succinct Solver of Nielson and Seidl is based on the Alternation-free Least Fixed Point Logic and it is implemented in SML using a combination of recursion, continuations, prefix trees and memoisation. It is known that the actual formulation of the analysis has a great impact on the execution time of the solver and the aim of this note is to provide some insight into which formulations are better than others. The experiments addresses three general issues: (i) the order of the parameters of relations, (ii) the order of conjuncts in preconditions and (iii) the use of memoisation. The experiments are performed for Control Flow Analyses for Discretionary Ambients.",

keywords = "Succinct Solver, Control Flow Analysis, Program Analysis, Constraint solving, Discretionary Ambients",

author = "Mikael Buchholtz and Nielson, {Hanne Riis} and Flemming Nielson",

year = "2002",

language = "English",

}

TY - RPRT

T1 - Experiments with Succinct Solvers

AU - Buchholtz, Mikael

AU - Nielson, Hanne Riis

AU - Nielson, Flemming

PY - 2002

Y1 - 2002

N2 - The Succinct Solver of Nielson and Seidl is based on the Alternation-free Least Fixed Point Logic and it is implemented in SML using a combination of recursion, continuations, prefix trees and memoisation. It is known that the actual formulation of the analysis has a great impact on the execution time of the solver and the aim of this note is to provide some insight into which formulations are better than others. The experiments addresses three general issues: (i) the order of the parameters of relations, (ii) the order of conjuncts in preconditions and (iii) the use of memoisation. The experiments are performed for Control Flow Analyses for Discretionary Ambients.

AB - The Succinct Solver of Nielson and Seidl is based on the Alternation-free Least Fixed Point Logic and it is implemented in SML using a combination of recursion, continuations, prefix trees and memoisation. It is known that the actual formulation of the analysis has a great impact on the execution time of the solver and the aim of this note is to provide some insight into which formulations are better than others. The experiments addresses three general issues: (i) the order of the parameters of relations, (ii) the order of conjuncts in preconditions and (iii) the use of memoisation. The experiments are performed for Control Flow Analyses for Discretionary Ambients.

KW - Succinct Solver

KW - Control Flow Analysis

KW - Program Analysis

KW - Constraint solving

KW - Discretionary Ambients

M3 - Report

BT - Experiments with Succinct Solvers

ER -