Faster checking of software specifications by eliminating isomorphs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Faster checking of software specifications by eliminating isomorphs

Full text

Pdf (1.11 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

St. Petersburg Beach, Florida, United States

Pages: 79 - 90

Year of Publication: 1996

ISBN:0-89791-769-3

Authors

Daniel Jackson	School of Computer Science, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA
Somesh Jha	School of Computer Science, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA
Craig A. Damon	School of Computer Science, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 20, Citation Count: 8

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/237721.237733 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	B+94	Juan C. Bicarregui , John S. Fitzgerald , Peter A. Lindsay , Richard Moore , Brian Ritchie, Proof in VDM: a practitioner's guide, Springer-Verlag New York, Inc., New York, NY, 1994
	BC+92	J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
	BG94	J. Bowen and M,J.C. Gordon. Z and HOL. Z User Workshop, Cambridge, England, 1994, Springer- Verlag Workshops in Computing, pp. 141-167.
	BH94	Rudolf Berghammer and Claudia Hattensperger. Computer-Aided Manipulation of Relational Expressions and Formulae Using RALF. Technical Report, Institut fur Informatik und Praknsche Mathematik, Chrisnan-Albrechts Universitat Zu Kiel, Kiel, Germany, 1994.
	BS92	Belaid Benhamou , Lakhdar Sais, Theoretical Study of Symmetries in Propositional Calculus and Applications, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.281-294, June 15-18, 1992
	CFJ93	Edmund M. Clarke , Thomas Filkorn , Somesh Jha, Exploiting Symmetry In Temporal Logic Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.450-462, June 28-July 01, 1993
	DK94	Jeffrey Douglas , Richard A. Kemmerer, Aslantest: a symbolic execution tool for testing Aslan formal specifications, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.15-27, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.186487]
	ELL94	René Elmstrøm , Peter Gorm Larsen , Poul Bøgh Lassen, The IFAD VDM-SL toolbox: a practical approach to formal specifications, ACM SIGPLAN Notices, v.29 n.9, p.77-80, Sept. 1994 [doi>10.1145/185009.185028]
	ES93	E. Allen Emerson , A. Prasad Sistla, Symmetry and Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.463-478, June 28-July 01, 1993
	ES94	Marcm EngeI and Jens Ulrlk Skakkebaek. Applying PVS to Z. Techmcal Report ID/DTU ME 3/1, ProCos Project, Department of Computer Science, Technical University of Denmark, Lyngby, Denmark.
	GGH90	S. J. Garland , J. V. Guttag , J. J. Horning, Debugging Larch Shared Language Specifications, IEEE Transactions on Software Engineering, v.16 n.9, p.1044-1057, September 1990 [doi>10.1109/32.58789]
	Hay93	Ian Hayes, Specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1987
	Hol91	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	ID93	C. Norris Ip , David L. Dill, Better Verification Through Symmetry, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.97-111, April 26-28, 1993
	Jac94	Daniel Jackson, Abstract Model Checking of Infinite Specifications, Proceedings of the Second International Symposium of Formal Methods Europe on Industrial Benefit of Formal Methods, p.519-531, October 24-18, 1994
	Jac96	Daniel Jackson. Nitplck: A Checkable Specification Language. Proc.Workshop on Formal Methods m Software Practice, San Diego, CA, January 1996.
	JD96	Daniel Jackson , Craig A. Damon, Elements of style: analyzing a software design feature with a counterexample detector, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.239-249, January 08-10, 1996, San Diego, California, United States
	Jon92	R.B. Jones. ICL ProofPower. British Computer Society Formal Aspects of Computer Sctence, Series 3, 1(1), 1992, pp. 10-13.
	Kur86	R.E Kurshan. Testing Containment of Omega- Regular Languages. AT&T Bell Laboratories, Techmcal Report 1121-861010-33 (1986).
	Kur94	Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
	LL91	Peter Gorm Larsen , Poul Bøgh Lassen, An Executable Subset of Meta-IV with Loose Specification, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.604-618, October 21-25, 1991
	McK81	Brendan D. McKay. Practical graph isomorphism. Congressus Numerantium 21 (1981), pp. 499-517.
	McK94a	Brendan D. McKay. Nauty User's Guide, version 1.5. Computer Science Department, Austrahan National University, GPO Box 4, ACT 2601, Austraha.
	McK94b	Brendan D. McKay. Isomorph-free exhaustive generatzon. Unpubhshed manuscript. Computer Science Department, Austrahan National Unlversity, GPO Box 4, ACT 2601, Australia.
	Sla94	John K. Slaney, FINDER: Finite Domain Enumerator - System Description, Proceedings of the 12th International Conference on Automated Deduction, p.798-801, June 26-July 01, 1994
	Spi92	J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
	SS93	Gunther Schmldt and Thomas Strohlein. Relations and Graphs. EATCS Monographs in TheorencaI Computer Science, Springer-Verlag, t993.
	Sta91	P. H. Starke, Reachability analysis of Petri nets using symmetries, Systems Analysis Modelling Simulation, v.8 n.4-5, p.293-303, 1991
	Val91	Samuel H. Valentine, Z--, an Executable Subset of Z, Proceedings of the Z User Workshop, p.157-187, December 16-17, 1991
	WO80	E.J. Weyuker and T.J. Ostrand. Theories of program testing and the apphcanon of reveahng subdomains. IEEE Trans. on Software Engineering, vol. SE-6, pp. 236-24S, May 1980.

CITED BY 8

	Daniel Jackson , Craig A. Damon, Elements of style: analyzing a software design feature with a counterexample detector, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.239-249, May 1996
	Craig A. Damon, Nitpick: a tool for interactive design analysis, Proceedings of the 19th international conference on Software engineering, p.596-597, May 17-23, 1997, Boston, Massachusetts, United States
	Daniel Jackson , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998
	Craig A. Damon , Daniel Jackson , Somesh Jha, Checking relational specifications with binary decision diagrams, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.70-80, Nov. 1996
	Daniel Jackson, An intermediate design language and its analysis, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.121-130, Nov. 1998
	Daniel Jackson , Craig A. Damon, Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector, IEEE Transactions on Software Engineering, v.22 n.7, p.484-495, July 1996
	Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998
	Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999