Monotonicity Analysis Can Speed Up Verification

FRIAS, MARCELO FABIAN; GAMARRA, RODOLFO; STEREN, GABRIELA; BOURG, LORENA

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2006 vol. 4136 p. 177 - 191

0302-9743

We introduce a strategy for the verification of relational specifications based on the analysis of monotonicity of variables within formulas. By comparing with the Alloy Analyzer, we show that for a relevant class of problems this technique outperforms analysis of the same problems using SAT-solvers, while consuming a fraction of the memory SAT-solvers require.