A strategy for efficient verification of relational specifications, based on monotonicity analysis
Abstract
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 drastically outperforms analysis of the same problems using SAT-solvers, while consuming a fraction of the memory SAT-solvers require.
BibTeX
@inproceedings{Frias-al:ASE05,
author = {Marcelo F. Frias and
Rodolfo Gamarra and
Gabriela Steren and
Lorena Bourg},
title = {A strategy for efficient verification of relational specifications, based on monotonicity analysis},
booktitle = {ASE},
pages = {305--308},
publisher = {{ACM}},
year = {2005},
}