Spreadsheet Verificator
Introduction
Do you want to ensure the correctness of your spreadsheets?
Do you need to review spreadsheets made by others?
If so, Spreadsheet Verificator is your best friend!
 Spreadsheet Verificator verifies all the cell values and formulas
of your spreadsheet by types.
 It either proves that the spreadsheet is exempt of a class of typing errors,
or identifies the cell formulas that contain typing mismatches,
which are clues to spreadsheet defects.
 As a result, verifying and validating spreadsheets by Spreadsheet Verificator
will improve their quality and
prevent you from making business decisions with incorrect spreadsheets.
Elements in the Task Pane
 1 button
 1 result area
 1 link to the support page
Mustdo Before Running the Tool
 unprotect manually the worksheets protected with password, if there is any
Tests
 Comparison.xlsx: an artificial simple example to show a comparison of a string and a double does not lead to an obvious error (eg, #VALUE) in Excel, though such a comparison does not make any sense in reality.
 Finalgradebook.xlsx:
Spreadsheet Verificator will detects a typing error: "AVERAGE(Double, Double, Double, Double, Empty)", from where we could observe that the last argument of the formula does not point to the correct cell.
 act3_lab23_posey.xlsx:
A "CurrencyString" typing error will be raised by the verificator;
it reveals that the value of a cell is incorrectly entered.
 Progress.xlsx:
A "Double/String" typing error raised by the verificator will
reveal the incomplete part of the spreadsheet.
Brief Description of our Verification
Why Should Spreadsheets Be Verified by Tools?
 Spreadsheets are errorprone,
because errors in spreadsheets are not blocking
 Spreadsheets are carriers of important business information, data and logic

Spreadsheets can be big and complex, or made by others;
they are hard to review thoroughly.
Verification by Types
Type checking is a classic, popular, and effective method to verify computer programs.
It is even systematically applied to programs written in certain languages
such as OCaml, C#, etc., which are thus called "strongly typed" languages.
However, almost all the spreadsheet languages are "weakly typed".
For example,
a comparison of a string and a numeric value is permitted (returns true of false),
and does not lead to any error.
Even though some meaningless operations show errors such as #VALUE,
they are not blocking and can be easily disregarded by users.
Therefore, our approach aims at applying type checking to spreadsheet programs,
to improve their quality.
Our Types
Currently, in our type system, we class cell values by the following types:
Empty 
Double 
Integer 
Boolean 
String 
Date 
Currency 
We implement a set of "dangerous" typing rules in Spreadsheet Verificator.
The tool verifies all the formulas of a spreadsheet,
raises a typing error,
if it discovers a dangerous typing rule may be matched
during the calculation of the spreadsheet.
In the following table, we list the dangerous typing rules
that are easy to formalize.
For instance, "Boolean +   Currency  Date" means
it is dangerous to add or minus a Boolean value to a Currency or a Date.
SIN  COS  ATAN  ASIN (Boolean  Date  String) 
LN  LOG1  LOG10  SQRT  EXP (Boolean  Date) 
(Boolean  Date) 
+Boolean 
POWER  LOG2 (ANY, Boolean  Date) 
POWER  LOG2 (Boolean  Date, ANY) 
Currency +    *  / Date 
Date +    *  / Currency 
Currency  Date +   Boolean 
Boolean +   Currency  Date 
Boolean  String +    *  / ANY 
ANY +    *  / Boolean  String 
Date *  / ANY 
ANY *  / Date 
Date <  >  <=  >=  ==  <> String  Integer  Double  Boolean  Currency 
Currency <  >  <=  >=  ==  <> String  Boolean  Date 
String <  >  <=  >=  ==  <> Boolean  Integer  Double  Date  Currency 
Boolean <  >  <=  >=  ==  <> String  Integer  Double  Date  Currency 
Integer  Double <  >  <=  >=  ==  <> String  Boolean  Date 
MIN  MAX (Boolean  String) 
MIN  MAX has one argument, which is array; the array contains Boolean  String 
MIN  MAX has one argument, which is array; the array does not contain Boolean  String; it contains Currency  Double  Integer and Date 
MIN  MAX has more than one argument, and there exists one Boolean  String argument 
MIN  MAX has more than one argument; there is no Boolean  String argument; there exists one Currency  Double  Integer argument and one Date argument 
SUM (Boolean  Date  String) 
SUM has one argument, which is array; the array contains Boolean  Date elements 
SUM has more than one argument, and there exists one Boolean  Date  String argument 
AVERAGE  MEDIAN (Boolean  Date  String) 
AVERAGE  MEDIAN has one argument, which is array; the array contains Boolean  Date elements 
AVERAGE  MEDIAN has more than one argument, and there exists one Boolean  Date  String argument 
... 
Note that some typing rules may be considered dangerous by some users, but safe by others. It is not possible to make a universally absolute and exhaustive set of dangerous typing rules. If you think certain typing rules are missing in the tool, please write to us.
Advantages

Spreadsheet Verificator is fully automatic;
it does not require users to provide supplementary information to be launched.

Another important advantage of our approach is its "soundness".
That means we guarantee that
none of the dangerous typing rules could ever be matched in any calculation of the spreadsheet.
In other words,
if the spreadsheet is validated by the tool,
the validation applies to all the possible input cell values,
as long as their type does not change.
This is particularly better and more exhaustive than a manually testing approach,
which cannot cover all the possible input instances.
False Alarms
As the cell property (ie, types) we reason on is more abstract and less precise than concrete cell values, verification tools like ours involves a notion of precision.
In case of being not precise enough, there may be false alarms,
which means what the tool raises is not a real error.
For instance, the formula =IF(ABS(A1)>=0, 3, false)+5
always evaluates to 8. Whereas, an analysis solely based on types
translates the formula to "=IF(ABS(A1)>=Integer, Integer, Boolean)+Integer".
As it cannot evaluate the value of "ABS(A1)>=Integer", it considers
the typing error "Boolean+Integer" is possible.
Therefore, one target of verification tools is to improve their precision
and have less false alarms.
Upcoming Features
 be able to verify array formulas
 verify formulas containing names
 verify VBA macros in a spreadsheet
Contact Us