Semantic analysis of shared-memory concurrent languages using abstract model-checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Semantic analysis of shared-memory concurrent languages using abstract model-checking

Full text

Pdf (1.30 MB)

Source

ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation archive
Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation table of contents

La Jolla, California, United States

Pages: 214 - 225

Year of Publication: 1995

ISBN:0-89791-720-0

Author

Régis Cridlig

Laboratoire d'Informatique de l'Ecole Normale Supérieure, 45 rue d'Ulm, 75230 Paris, Cedex 05, France

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 7, Citation Count: 10

Additional Information:

references cited by index terms collaborative colleagues peer to peer

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/215465.215593 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.

	BDER79	G. Bristow , C. Drey , B. Edwards , W. Riddle, Anomaly detection in concurrent programs, Proceedings of the 4th international conference on Software engineering, p.265-273, September 17-19, 1979, Munich, Germany
	Bou92	F. Bourdoncle. Sdmantique des Iangages impdratifs d'ordre ,supdrieur et interprdtation abstraite. PhD thesis, Ecole polytechnique, 1992.
	Bou93	François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
	CC77	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	CC79	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
	CC92	P. Cousot and t~. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4), 1992.
	CG93	Régis Cridlig , Eric Goubault, Semantics and Analysis of Linda-Based Languages, Proceedings of the Third International Workshop on Static Analysis, p.72-86, September 22-24, 1993
	CGL94	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
	CH92	J.-H. Chow and W. L. Harrison III. Compile-time Analysis of Parallel Programs that Share Memory. In LISP and Functional Programming, June 1992.
	CH94	J.-H. Chow and W. L. Harrison III. State Space Reduction in Abstract }nterpretation of Parallel Programs. In Proceedings of the 1994 International Conrerence on Computer Languages. IEEE, 1994.
	CPY94	Rance Cleaveland , S. P Iyer , Daniel Yankelevich, Abstractions for Preserving All CTL* Formulae, North Carolina State University at Raleigh, Raleigh, NC, 1994
	DGG94	D. Dams, O. Grumberg. and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving VCTL, 3CTL and CTL*. In E.-R. Olderog, editor, Proceedings of the IFIP WG2.I/WG2.2/WG2.3 Working Conference on, Programming Concepts, Methods and Calcuh (PROCOMET), IFIP Transactions, Amsterdam, June 1994. North-Holland/Elsevier.
	DP94	P. Degano and C. Priami. A Compact Representation of Finite State Processes. Technical report, Dipartimento di Informatica, Universit~ di Pisa, 1994.
	EL86	E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus (Extended abstract). In Proc. IEEE Symposium, on Logic ~n Computer Science, pages 267-278, Cambridge, MA, June 1986.
	GJ92	Eric Goubault , Thomas P. Jensen, Homology of Higher Dimensional Automata, Proceedings of the Third International Conference on Concurrency Theory, p.254-268, August 24-27, 1992
	Gla91	R. van Glabbeek. Bisimulation Semantics for Higher Dimensional Automata. Technical report, Stanford University, 1991.
	Gra91	Philippe Granger, Static analysis of linear congruence equalities among variables of a program, Proceedings of the international joint conference on theory and practice of software development on Colloquium on trees in algebra and programming (CAAP '91): vol 1, p.169-192, April 1991, Brighton, United Kingdom
	Hoa78	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	Kel94	P. Kelb. Model Checking and Abstraction: A Framework Approximating both Truth and Failure Information. Technical report, University of Oldenburg, 1994.
	Mil89	R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	Plo81	G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus, Denmark, September 1981.
	Pra91	Vaughn Pratt, Modeling concurrency with geometry, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.311-322, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99625]
	Tay93	Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
	Val89	Antti Valmari, Eliminating Redundant Interleavings During Concurrent Program Verification, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.89-103, June 12-16, 1989
	WJ78	K Jensen , N Wirth , A B Mickel , J F Miner, Pascal user manual and report; 3rd ed., Springer-Verlag New York, Inc., New York, NY, 1985
	Zuc93	Jeffery I. Zucker, The Propositional mu-Calculus and Its Use in Model Checking, Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada, p.117-128, January 1993

CITED BY 10

	Patrick Cousot, Program analysis: the abstract interpretation perspective, ACM Computing Surveys (CSUR), v.28 n.4es, Dec. 1996
	Susanne Graf, Characterization of a sequentially consistent memory and verification of a cache memory by abstraction, Distributed Computing, v.12 n.2/3, p.75-90, June 1999
	Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
	Satish Chandra , Patrice Godefroid , Christopher Palm, Software model checking in practice: an industrial case study, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Lisbeth Fajstrup , Martin Raußen , Eric Goubault, Algebraic topology and concurrency, Theoretical Computer Science, v.357 n.1, p.241-278, 25 July 2006
	Eric Goubault, Geometry and concurrency: a user's guide, Mathematical Structures in Computer Science, v.10 n.4, p.411-425, August 2000
	Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
	Patrick Cousot , Radhia Cousot, Refining Model Checking by Abstract Interpretation, Automated Software Engineering, v.6 n.1, p.69-95, January 1999
	R. J. van Glabbeek, On the expressiveness of higher dimensional automata, Theoretical Computer Science, v.356 n.3, p.265-290, 30 May 2006
	R. J. van Glabbeek, Erratum: Erratum to “On the expressiveness of higher dimensional automata”, Theoretical Computer Science, v.368 n.1-2, p.168-194, December, 2006