skip to main content
10.1145/1101908.1101956acmconferencesArticle/Chapter ViewAbstractPublication PagesaseConference Proceedingsconference-collections
Article

A strategy for efficient verification of relational specifications, based on monotonicity analysis

Published: 07 November 2005 Publication History

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.

References

[1]
Frias M. F., Lopez Pombo C. G., Baum G. A., Aguirre N. and Maibaum T. S. E., Reasoning About Static and Dynamic Properties in Alloy: A Purely Relational Approach, to appear in ACM TOSEM, in press.
[2]
D. Nitpick: A checkable specification language. In Proceedings of the Workshop on Formal Methods in Software Practice (San Diego, Calif., Jan. 1996).
[3]
Jackson D., Schechter I. and Shlyakhter I., Alcoa: the Alloy Constraint Analyzer, Proceedings of the International Conference on Software Engineering, Limerick, Ireland, June 2000.
[4]
Jackson D., Alloy: A Lightweight Object Modelling Notation, ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256--290.
[5]
Tarski, A. and Givant, S., A Formalization of Set Theory without Variables, A.M.S. Coll. Pub., vol. 41, 1987.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering
November 2005
482 pages
ISBN:1581139934
DOI:10.1145/1101908
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. alloy
  2. relational methods
  3. software specification
  4. software validation

Qualifiers

  • Article

Conference

ASE05

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 134
    Total Downloads
  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media