Types as models: model checking message-passing programs. (English) Zbl 1323.68365
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’02, Portland, OR, USA, January 16–18, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-450-9). 45-57 (2002).
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N18 | Functional programming and lambda calculus |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73-132, 1993.]] 10.1145/151646.151649 |
| [2] | M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507-534, 1995.]] 10.1145/203095.201069 |
| [3] | R. Alur and T. A. Henzinger. Reactive modules, hi LICS 96: Logic in Computer Science, pages 207-218. IEEE Computer Society Press, 1996.]] |
| [4] | R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, and S. Tasiran. MOCHA : Modularity in model checking. In CAV 98: Computer Aided Verification, LNCS, pages 521-525. Springer-Verlag, 1998.]] |
| [5] | T. Anitoft, F.Nielson, and H.R. Nielson. Type and Effect Systems. Behaviours for Concurrency. Imperial College Press, 1999.]] |
| [6] | S. Chaki, S.K. Rajaniani, and J. Rehof. Types as models: Model checking niessage-passing programs. Technical report, Microsoft Research, 2001. Available at research.microsoft, com/behave.]] |
| [7] | S. Christensen, Y. Hirshfeld, and F. Moiler. Decidable subsets of CCS. The Computer Journal, 37(4):233-242, 1994.]] |
| [8] | E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.]] |
| [9] | Customer Support Consortium (CSC) and Desktop Management Task Force (DMTF). Service incident standard (sis) specification, version 1.1. Technical report, DMTF. Available at WWW. dmtf. org.]] |
| [10] | A.T. Eiriksson. The formal design of 1M-gate ASICs. hi FMCAD 98: Formal Methods in Computer-Aided Design, LNCS 1522, pages 49-63. Springer-Verlag, 1998.]] |
| [11] | C. Flanagan and M. Abadi. Types for safe locking, hi ESOP 99: European Symposium on Programming, LNCS 1576, pages 91-108. Springer-Verlag, 1999.]] |
| [12] | C. Flanagan and S. N. Freund. Type-based race detection for Java. hi PLDI 00: Programming Language Design and Implementation, pages 219-232. ACM, 2OOO.]] 10.1145/349299.349328 |
| [13] | A. Gordon and A. Jeffrey. Typing corresondence assertions for communication protocols. In MFPS: Mathematical Foundations of Programming Semantics, pages 99 120. BRICS Notes Series NS-01-2, 2001. T. A. Henzinger, X. Liu, S. Qadeer, and S. K.]] |
| [14] | Rajamani. Formal specification and verification of a dataflow processor array. In ICCAD 99:Computer-Aided Design, pages 494-499. IEEE Computer Society Press, 1999.]] |
| [15] | T.A. Henzinger, S. Qadeer, S.K. Rajaniani, and S. Tasiran. An assume-guarantee rule for checking simulation. In FMCAD 98: Formal Methods in Computer-aided Design, LNCS 1522, pages 421 432. Springer-Verlag, 1998.]] |
| [16] | G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.]] |
| [17] | G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279 295, May 1997.]] 10.1109/32.588521 |
| [18] | Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP 98. Springer, 1998.]] |
| [19] | A. Igarashi and N. Kobayashi. A generic type system for the Pi-calculus. In POPL 01: Principles of Programming Languages, pages 128 141. ACM, 2001.]] 10.1145/360204.360215 · Zbl 1323.68410 |
| [20] | Kim G. Larsen and Robin Mihier. A compositional protocol verification using relativized bisimulation. Information and Computation, 99:80 108, 1992.]] 10.1016/0890-5401(92)90025-B · Zbl 0753.68067 |
| [21] | J. R. Larus and M. Parkes. Using cohort scheduling to enhance server performance. Technical Report MSR-TR-2001-39, Microsoft Research, 2001.]] |
| [22] | K. L. McMillan. A compositional rule for hardware design refinenient, hi CA V 97: Computer-Aided Verification, LNCS 1254, pages 24-35. Springer-Verlag, 1997.]] |
| [23] | R. Misra. Communicating and Mobile Systems: the 7c-Calculus. Cambridge University Press, 1999.]] · Zbl 0942.68002 |
| [24] | J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417-426, 1981.]] · Zbl 0468.68030 |
| [25] | H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In POPL 94: Principles of Programming Languages, pages 84-97. ACM, 1994.]] 10.1145/174675.174538 |
| [26] | F. Puntigam and C. Peter. Changeable interfaces and promised messages for concurrent components. In SAC 99: Symposium on Applied Computing, pages 141-145. ACM, 1999.]] 10.1145/298151.298223 |
| [27] | S.K. Rajamani and J. Rehof. A behavioral module system for the pi-calculus. In SAS 01: Static Analysis, LNCS 2126, pages 375-394. Springer-Verlag, 2001.]] · Zbl 0997.68514 |
| [28] | A. Ravara and V. Vasconcelos. Typing non-uniforni concurrent objects. In CONCUR 00: Concurrency Theory, LNCS 1877, pages 474-488. Springer-Verlag, 2000.]] · Zbl 0999.68151 |
| [29] | D. Sangiorgi. -calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(2), 1996.]] 10.1016/0304-3975(96)00075-8 · Zbl 0874.68103 |
| [30] | D. Sangiorgi. A theory of bisimulation for the 7c-calculus. Acta Informatica, 33, 1996.]] 10.1007/s002360050036 · Zbl 0835.68072 |
| [31] | N. Yoshida. Graph types for monadic mobile processes, hi FSTTCS: Software Technology and Theoretical Computer Science, LNCS 1180, pages 371-387. Springer-Verlag, 1996.]] |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
