Automatic verification of parameterized linear networks of processes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Automatic verification of parameterized linear networks of processes

Full text

Pdf (812 KB)

Source

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

Paris, France

Pages: 346 - 357

Year of Publication: 1997

ISBN:0-89791-853-3

Authors

David Lesens	Verimag is a joint laboratory of CNRS, Institut National Polytecnique de Grenoble, Universite J. Fourier and Verilog SA assoclated with IMAG, Miniparc-ZIRST, F-38330 Montbonnot, France
Nicolas Halbwachs	Verimag is a joint laboratory of CNRS, Institut National Polytecnique de Grenoble, Universite J. Fourier and Verilog SA assoclated with IMAG, Miniparc-ZIRST, F-38330 Montbonnot, France
Pascal Raymond	Verimag is a joint laboratory of CNRS, Institut National Polytecnique de Grenoble, Universite J. Fourier and Verilog SA assoclated with IMAG, Miniparc-ZIRST, F-38330 Montbonnot, France

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 14, Citation Count: 3

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

	AK86	K R Apt , D C Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, v.22 n.6, p.307-309, May 30,1986 [doi>10.1016/0020-0190(86)90071-2]
	BG92	Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
	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]
	CC92	Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
	CES86	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	CGJ95	Edmund M. Clarke , Orna Grumberg , Somesh Jha, Veryfying Parameterized Networks using Abstraction and Regular Languages, Proceedings of the 6th International Conference on Concurrency Theory, p.395-407, August 21-24, 1995
	Eil74	Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
	EN95	E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199468]
	EN96	E. Allen Emerson , Kedar S. Namjoshi, Automatic Verification of Parameterized Synchronous Systems (Extended Abstract), Proceedings of the 8th International Conference on Computer Aided Verification, p.87-98, August 03, 1996
	Hal93	Nicolas Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, Norwell, MA, 1992
	Har87	David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
	HCRP91	N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305-1320, September 1991.
	HLR92	Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, An experience in proving regular networks of processes by modular model checking, Acta Informatica, v.29 n.6-7, p.523-543, 1992 [doi>10.1007/BF01185559]
	HLR93	Nicolas Halbwachs , Fabienne Lagnier , Pascal Raymond, Synchronous Observers and the Verification of Reactive Systems, Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.83-96, June 21-25, 1993
	KM89	R. P. Kurshan , K. McMillan, A structural induction theorem for processes, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.239-247, June 1989, Edmonton, Alberta, Canada [doi>10.1145/72981.72998]
	Mar92	Florence Maraninchi, Operational and Compositional Semantics of Synchronous Automaton Compositions, Proceedings of the Third International Conference on Concurrency Theory, p.550-564, August 24-27, 1992
	QS82	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	SG89	Z. Shtadler , O. Grumberg, Network grammars, communication behaviors and automatic verification, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.151-165, February 1990, Grenoble, France
	WL89	P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France

CITED BY 3

	Giorgio Delzanno, Constraint-Based Verification of Parameterized Cache Coherence Protocols, Formal Methods in System Design, v.23 n.3, p.257-301, November 2003
	Samik Basu , C. R. Ramakrishnan, Compositional analysis for verification of parameterized systems, Theoretical Computer Science, v.354 n.2, p.211-229, 28 March 2006
	Abhik Roychoudhury , I. V. Ramakrishnan, Inductively Verifying Invariant Properties of Parameterized Systems, Automated Software Engineering, v.11 n.2, p.101-139, April 2004