
Overview This program is able to infer fixpoints for given disjunctive formulae (postconditions). It makes use of a novel concept called planar affinity, a technique for measuring how related (or similar) are two given formulae. Affinity is used in both hulling and widening operations throughout the fixed point algorithm. The fixed point algorithm follows from the seminal work of Cousot and Halbwachs for the (conjunctive) polyhedron abstract domain [Cousot:POPL78]. More recent work on disjunctive abstract domains include [Bagnara:VMCAI04, Sankaranarayana:SAS06]. The algorithm implemented in the Fixpoint Calculator is described in more details in the paper ASIAN06. Terms Fixpoint analysis  Often in program analysis writing formulae that can express relations between inputs and outputs (of a given block or method) necessitates this type of analysis. The blocks requiring fixpoint analysis are the ones containing a recursive construct of some kind. Through successive iterations, the starting formula is modified until its form remains the same for two consecutive computations. Hulling and widening are applied in computing next iterations, at times. Disjunctive normal form  a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses. Hulling  an aproximation technique that combines related disjunctive formulae into a conjunct. For the Fixpoint Calculator a new selective hull operation is introduced, parameterized with m, maximum number of disjuncts that the resulting formula should have. Widening  another aproximation operation that drops some conjunctive subformulae. The conjunct that is removed is usually one that changes between fixpoint analysis iterations. A pairwise widening technique is used for the Calculator, where only the most related pairs will distribute the widening operator (when applied for two disjunctive formulae). Software Omega Calculator  The Fixpoint Calculator is incorporationg this software. It needs to have been installed for running Fixpoint Calculator. Fixpoint Calculator  Binary compiled under Fedora Core release 4. Tutorial Syntax and semantics of input files for our calculator are close to that of Omega Calculator, for ease of understanding. An example input file (runs with  sumvec:={[s,i,j] > [] > [i,j]: exists (PRMi,PRMj: exists (i_1: (i>j  (i<=j && 0<=i<s && i_1=i+1 && sumvec(s,i_1,j)))))}; sumvec; sumvec0:={[]: 0=1}; sumvec1:=sumvec(sumvec0); sumvec2:=sumvec(sumvec1); sumvec3:=sumvec(sumvec2); sumvec3h:=selhull(sumvec3,3,SimHeur); sumvec4:=sumvec(sumvec3h); sumvec4h:=selhull(sumvec4,3,SimHeur); sumvec3w:=widen(sumvec3h,sumvec4h,SimHeur); #sumvec4:=sumvec(sumvec3); Fix:=bottomup(sumvec,3,SimHeur); sumvec0;sumvec1;sumvec2;sumvec3;sumvec4;Fix;sumvec3w; 
 We're calculating a postcondition for the following function:
 The first line defines the recursive formula for the function's constraint abstraction.
These have to be provided by the user.
The variables
 The
 We start with Papers
disjunctive.asian06.pdf
array.pepm08.pdf
dual.pdf
thesis.pdf People Contributors to this Calculator and its techniques are: 