Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
ABRAMSKY, S. 1996. Retracing some paths in process algebra. In Proceedings of CONCUR '96 - Seventh International Conference on Concurrency Theory, Lecture Notes in Computer Science, Vol. 1119, (Pisa, Italy, Aug.) U. Montanari and V. Sassone, Eds., Springer-Verlag, Berlin, New York, 1-17.
ABRAMSKY, S., GAY, S., AND NAGARAJAN, R. 1996. Specification structures and propositions-as-types for concurrency. In Logics for Concurrency: Structure vs. Automata, F. Moller and G. Birtwistle, Eds. Lecture Notes in Computer Science, Vol. 1043, (Banff, Canada, Aug) Springer-Verlag. Berlin, New York,
ACETO, L., BLOOM, B., AND VAANDRAGER, F. W. 1994. Turning SOS rules into equations. Inf. Comput. III, 1 (May), 1-52.
ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 181-185.
ALUR, R. AND DILL, D. 1994. The theory of timed automata. TCS 126, 2.
ALUR, R. AND HENZINGER, T. A. 1996a. Computer Aided Verification (CAV '96), Lecture Notes in Computer Science, Vol. 1102, (New Brunswick, NJ, July) Springer-Verlag. Berlin, New York.
ALUR, R. AND HENZINGER, T. A. 1996b. Reactive modules. In Proceedings of the Eleventh IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Washington, DC, 207-218.
ANDERSEN, H. R. 1994. Model checking and Boolean graphs. Theor. Comput, Sci. 126, 1.
BAETEN, J. C. M. AND WEIJLAND, W. P. 1990. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, New York.
BAETEN, J. C. M., BERGSTRA, J. A., AND KLOP, J, W. 1993. Decidability of bisimulation equivalence for processes generating context-free languages. J. ACM 40, 653-682.
BARR, M. 1979. *-Autonomous Categories, Lecture Notes in Mathematics, Vol. 752, Springer-Verlag. Berlin, New York.
BERNHOLTZ, O., VARDI, M. Y., AND WOLPER, P. 1994. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification (CAV '94), Lecture Notes in Computer Science, D. L. Dill, Ed., Vol. 818, (Stanford, CA, June) Springer-Verlag, Berlin, New York. 142-155.
BERRY, G. AND GONTHIER, G. 1992. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming 19, 2 (Nov.), 87-152.
BEST, E., DEVILLERS, R., AND HALL, J. G. 1992. The Petri box calculus: A new causal algebra with multilabel communication. In Advances in Petri Nets 1992, G. Rozenberg, Ed., Lecture Notes in Computer Science, Vol. 609, Berlin, New York. Springer-Verlag, 21-69.
BEZEM, M. AND GROOTE, J. F. 1993. A formal verification of the alternating bit protocol in the calculus of constructions. Logic Group Preprint Series 88, Dept. of Philosophy, Utrecht University, March.
BHAT, G., CLEAVELAND, R., AND GRUMBERG, O. 1995. Efficient on-the-fly model checking for CTL*. In Tenth Annual Symposium on Logic in Computer Science (LICS '95) (San Diego, July), Computer Science Press, New York, 388-397.
BROOKES, S. D., HOARE, C. A. R., AND ROSCOE, A. W. 1984. A theory of communicating sequential processes. J. ACM 31, 3 (July), 560-599.
BROWNE, M. C., CLARKE, E. M., AND GRUMBERG, O. 1988. Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 1,2, 115-131.
BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, L. J. 1992. Symbolic model checking 1020 states and beyond. Inf. Comput. 98, 2 (June), 142-170.
CARRIERO, N. AND GELERNTER, D. 1989. Linda in context. Commun. ACM, 32, 4 (April), 444-458.
CHANDY, K. M. AND MISRA, J. 1988. Parallel Program Design. A Foundation. Addison-Wesley, Reading, MA.
CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 1, 244-263. Lecture Notes in Computer Sci. Vol. 697.
CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 1, 244-263. Lecture Notes in Computer Sci. Vol. 697.
CLARKE, E. M., FILKORN, T., AND JHA, S. 1993. Exploiting symmetry in model checking. In Computer Aided Verification (Elounda, Greece, June), C. Courcoubetis, Ed., Springer-Verlag, Berlin, New York, 450-462.
CLARKE, E. M., GRUMBERG, O., HIRAISHI, H., JHA, S., LONG, D. E., MCMILLAN, K. L., AND NESS, L. A. 1995. Verification of the Future+ cache coherence protocol. Formal Methods Syst. Des. 6, 217-232.
CLEAVELAND, R. AND STEFFEN, B. U. 1993. A linear-time model checking algorithm for the alternation-free modal mu-calculus. Formal Methods Syst. Des. 2, 121-147.
CLEAVELAND, R., MADELAINE, E., AND SIMS, S. 1995. A front-end generator for verification tools. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), (Aarhus, Denmark, May), E. Brinksma, R. Cleaveland, K. G. Larsen, and B. Steffen, Eds., Lecture Notes in Computer Science, Vol. 1019, Springer-Verlag, Berlin, New York, 153-173.
CLEAVELAND, R., PARROW, J., AND STEFFEN, B. U. 1993. The Concurrency Workbench: A semantics based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 1, 15, 36-72.
DAWS, C. AND YOVINE, S. 1995. Two examples of verification of mutirate automata using KRO-NOS. In Sixteenth Annual IEEE Real-Time. Systems Symposium (Pisa, Italy, Dec.), Computer Society Press, 66-75.
DE BAKKER, J. W., HUIZING, C., DE ROEVER, W.-P., AND ROZENBERG, G. 1992. Proceedings of REX Workshop on Real-Time: Theory in Practice. Lecture notes in Computer Science, vol. 600, (Mook, the Netherlands, June 1991) Springer-Verlag, Berlin, New York.
DE NICOLA, R. AND HENNESSY, M. 1984. Testing equivalences for processes. Theor. Comput. Sci. 34, 83-133.
DIJKSTRA, E. W. 1968. Cooperating sequential processes. In Programming Languages, Academic Press, London, 43-112. Originally appeared as Tech. Rep. EWD-123, Technical University of Eindhoven, the Netherlands, 1965.
EMERSON, E. A. AND HALPERN, J. Y. 1986. 'Sometime' and 'not never' revisited: On branching versus linear time temporal logic. J. ACM 33 1, 151-178.
EMERSON, E. A. AND SISTLA, A. P. 1993. Symmetry and model checking. In Computer-Aided Verification (CAV '93), C. Courcoubetis, Ed., Springer-Verlag, Berlin, New York, 463-478.
FOCARDI, R. AND GORRIERI, R. 1995. A classification of security properties for process algebras. J. Comput. Sec. 3, 1, 5-33.
FRANCEZ, N. 1986. Fairness. Springer-Verlag, Berlin, New York.
GABRIEL, K. J. 1995. Engineering microscopic machines. Sci. Am. (Sept.).
GERBER, R. AND LEE, I. 1994. A resource-based prioritized bisimulation for real-time systems. Inf. Comput. 113, 1 (Aug.), 102-142.
VAN GLABBEEK, R. J. 1990. Comparative concurrency semantics and refinement of actions. Ph.D. Thesis, Free University of Amsterdam, 1990. Available through URL http://theory. stanford.edu/∼rvg/thesis.html.
VAN GLABBEEK, R. J. 1993. Full abstraction in structural operational semantics. In Proceedings of the Third AMAST Conference, (Twente, The Netherlands, June), M. Nivat, C. Rattray, T. Rus, and G. Scollo, Eds. Workshops in Computing, Springer-Verlag, Berlin, New York, 77-84.
VAN GLABBEEK, R. J. AND PLOTKIN, G. 1995. Configuration structures. In Logic in Computer Science, IEEE Computer Society, Washington, DC, 199-209.
VAN GLABBEEK, R. J., SMOLKA, S. A., AND STEFFEN, B. 1995. Reactive, generative, and stratified models of probabilistic processes. Inf. Comput. 121, 1 (Aug.), 59-80.
GROOTE, J. F. AND VAANDRAGER, F. W. 1992. Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100, 2 (Oct.), 202-260.
GROSSMAN, R. L., NERODE, A., RAVN, A. P., AND RISCHEL, H., Eds. 1993. Hybrid Systems, vol. 736, (Lyngby, Denmark, Oct. 1992) Lecture Notes in Computer Science, Springer-Verlag. Berlin, New York.
GUPTA, V. AND PRATT, V. R. 1993. Gates accept concurrent behavior. In Proceedings of the Thirty-Fourth Annual IEEE Symposium on Foundations of Computer Science, (Nov.), 62-71.
HALBWACHS, N. 1993. Synchronous Programming of Reactive Systems. Kluwer Academic, Boston, MA.
HALPERN, J. AND MOSES, Y. 1990. Knowledge and common knowledge in a distributed environment. J. ACM 37, 3 (July), 549-587.
HALPERN, J. AND ZUCK, L. 1992. A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. J. ACM 39, 3 (July), 449-478.
HANSSON, H. A. 1994. Time and Probability in Formal Design of Distributed Systems, Real-Time Safety Critical Systems, Vol. 1, Elsevier, Amsterdam.
HAREL, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8, 231-274.
HAREL, D., LACHOVER, H., NAAMAD, A., PNUELI, A., POLITI, M., SHERMAN, R., SHTULL-TRAURING, A., AND TRAKTENBROT, M. 1990. Statemate: A working environment for the development of complex reactive systems. IEEE Trans. Softw. Eng. 16, 4 (April), 403-414.
HEIMDAHL, M. AND LEVESON, N. 1996. Completeness and consistency in hierarchical statebased requirements. IEEE Trans. Softw. Eng. SE-22, 6, 363-377.
HENNESSY, M. 1988. Algebraic Theory of Processes. MIT Press, Cambridge, MA.
HENNESSY, M. AND MILNER, R. 1985. Algebraic laws for nondeterminism and concurrency. J. ACM 32, 1, 137-161.
HENZINGER, T. A., HO, P.-H., AND WONG-TOI, H. 1995. HyTech: The next generation. In Sixteenth Annual IEEE Real-Time Systems Symposium, (Pisa, Italy, Dec.), Computer Society Press, 56-65.
HOARE, C. A. R. 1985. Communicating Sequential Processes. Prentice-Hall, London.
HOLZMANN, G., PELED, D., AND PRATT, V. R. 1996. Partial-Order Methods in Verification (POMIV '96). DIMACS Series in Discrete Mathematics and Computer Science. American Mathematical Society, Providence, RI.
JAGANNATHAN, S. AND WEEKS, S. 1994. Analyzing stores and references in a parallel symbolic language. In ACM Conference on LISP and Functional Programming, 294-305.
JONES, C. B. 1992. The search for tractable ways of reasoning about programs. Tech. Rep. TR UMCS-92-4-4, Department of Computer Science, University of Manchester, 1992. Available through URL http://www.cs-.man.ac.uk/csonly/cstechrep/Abstracts/UMCS-92-4-4.html.
KAHN, G. 1974. The semantics of a simple language for parallel programming. In Information Processing 74, J. L. Rosenfeld, Ed., North-Holland, Amsterdam.
KAHN, G. AND MACQUEEN, D. B. 1977. Coroutines and networks of parallel processes. In Information Processing 77, North-Holland, Amsterdam, 993-998.
KALTENBACH, M. 1996. Interactive verification exploiting program design knowledge: A model checker for UNITY. PhD thesis, University of Texas, Austin. Available through URL http://www.cs.utexas.edu/users/markus/ diss.html.
KANELLAKIS, P. C. AND SHVARTSMAN, A. A. 1992. Efficient parallel algorithms can be made robust. Distrib. Comput. 5, 4, 201-217.
KANELLAKIS, P. C. AND SMOLKA, S. A. 1990. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86, 1 (May), 43-68.
KELLER, R. 1976. Formal verification of parallel programs. Commun. ACM 19, 1 (July), 371-384.
KOZEN, D. 1983. Results on the prepositional mu-calculus, Theor. Comput. Sci. 27, 333-354.
LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2, 125-143.
LAMPORT, L. 1980. The "Hoare logic" of concurrent programs. Acta Inf. 14, 21-37.
LARSEN, K. G. AND SKOU, A. 1992. Bisimulation through probabilistic testing. Inf. Comput. 94, 1, (Sept.), 1-28.
LIN, H. 1991. PAM: A process algebra manipulator. In Computer Aided Verification (CAV '91), (Aalborg, Denmark, July), Lecture Notes in Computer Science, K. G. Larsen and A. Skou, Eds., Vol. 575, Springer-Verlag, Berlin, New York, 136-146.
LYNCH, N. A. AND TUTTLE, M. R. 1989. An introduction to input/output automata. CWI Quarterly 2, 3 (Sept.), 219-246.
MANNA, Z. AND PNUELI, A. 1991. The Temporal Logic of Reactive and Concurrent Systems: Specification. Berlin, New York, Springer-Verlag.
MANNA, Z. AND PNUELI, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, Berlin, New York.
MARGARIA, T. AND STEFFEN, B. 1996. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96) (Passau, Germany, March), Lecture Notes in Computer Science, Vol. 1055, Springer-Verlag, Berlin, New York.
MAZURKIEWICZ, A. 1987. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course (Bad Honnef, Sept.), W. Brauer, W. Reisig, and G. Rozenberg, Eds., Lecture Notes in Computer Science, Vol. 255, Springer-Verlag, Berlin, New York, 279-324.
MIFSUD, A., MILNER, R., AND POWER, J. 1995. Control structures. In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, (San Diego, CA, June) IEEE Computer Society Press, Los Alamitos, CA, 188-198.
MILNER, R. 1980. A calculus of communicating systems. Lecture Notes in Computer Science, Vol. 92, Springer-Verlag, Berlin, New York.
MILNER, R. 1989. Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cuffs, NJ.
MILNER, R. 1993. Action calculi, or syntactic action structures. In Proceedings of the Nineteenth MFCS, Lecture Notes in Computer Science, Vol. 711, Springer-Verlag, Berlin, New York, 105-121.
MILNER, R., TOFTE, M., AND HARPER, R. 1990. The Definition of Standard ML. MIT Press, Cambridge, MA.
MONTANARI, U. AND ROSSI, F. 1996. Graph rewriting and constraint solving for modelling distributed systems with synchronization. In Proceedings of COORDINATION'96, (Cesana, Italy, April) Lecture Notes in Computer Science, Vol 1061. P. Ciancarini and C. Hankin, Eds. Springer-Verlag, Berlin, New York.
NIELSON, F. AND NIELSON, H. R. 1993. Prom CML to process algebras. In Proceedings of CONCUR '93-Fourth International Conference on Concurrency Theory. Lecture Notes in Computer Science, Vol. 715, Springer-Verlag, Berlin, New York.
NIELSON, H. R. AND NIELSON, F. 1994. Higher-order concurrent programs with finite communication topology. In Proceedings of the Twenty-First Annual ACM SIGPLAN-SI-GACT Symposium on Principles of Programming Languages, (Portland, OR, Jan.) ACM Press, New York, 84-97.
NIERSTRASZ, O. 1990. Viewing objects as patterns of communicating agents. In Proceedings of ECOOP/OOPSLA '90; European Conference on Object-Oriented Programming/ Object-Oriented Programming Systems, Languages and Applications, SIGPLAN Not. 25, 10, 38-43.
OLDEROG, E.-R. 1991. Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship. Cambridge Tracts in Theoretical Computer Science 23. Cambridge University Press, New York.
OWICKI, S. AND GRIES, D. 1976. An axiomatic proof technique for parallel programs. Acta Inf. 6, 319-340.
OWRE, S., RUSHBY, J., AND SHANKAR, N. 1992. PVS: A prototype verification system. In Eleventh International Conference on Automated Deduction (CADE) (Saratoga Springs, NY, June), D. Kapur, Ed., Lecture Notes in Artificial Intelligence, Vol. 607, Springer-Verlag, Berlin, New York, 748-752.
PAIGE, R. AND TARJAN, R. E. 1987. Three partition refinement algorithms. SIAM J. Comput. 16 6 (Dec.), 973-989.
PELEG, D. 1987. Concurrent dynamic logic. J. ACM 34, 2 (April), 450-479.
PETRI, C. A. 1962. Kommunikation mit Automaten. Schriften des IIm 2, Institut für Instrumentelle Mathematik, Bonn, 1962.
English translation available as Communication with Automata, Tech. Rep. RADC-TR-65-377, Vol. 1, Suppl. 1, Applied Data Research, Princeton, NJ, 1966.
PIERCE, B. C. AND TURNER, D. N. 1995. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming, (Sendai, Japan, April), Lecture Notes in Computer Science, Vol. 907, Springer-Verlag, Berlin, New York.
PLOTKIN, G. D. 1981. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University.
PNUELI, A. 1977. The temporal logic of programs. In Eighteenth IEEE Symposium on Foundations of Computer Science, Computer Society Press, Los Alamitos, CA, 46-57.
PNUELI, A. AND SIFAKIS, J. 1995. Special Issue on Hybrid Systems of Theoretical Computer Science 138, 1 (Feb), Elsevier Science Publishers.
PRATT, V. R. 1986. Modeling concurrency with partial orders. Int. J. Parallel Program. 15, 1, 33-71.
PRATT, V. R. 1995. The Stone gamut: A coordinatization of mathematics. In Logic in Computer Science, IEEE Computer Society, Los Alamitos, CA, 444-454.
QUEILLE, J. P. AND SIFAKIS, J. 1982. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming (Berlin), Lecture Notes in Computer Science, Vol. 137, Springer-Verlag, Berlin, New York.
REISIG, W. 1985. Petri Nets - An Introduction. EATCS Monographs on Theoretical Computer Science, Vol. 4. Springer-Verlag, Berlin, New York.
REPPY, J. H. 1992. High-order concurrency. Ph.D. Thesis, Cornell University, 1992. Also Cornell University Computer Science Dept. Tech. Report 92-1285.
ROSCOE, A. W. 1994. Model checking CSP. In A Classical Mind: Essays in Honor of C. A. R. Hoare. Prentice-Hall International, Englewood Cliffs, NJ.
ROSCOE, A. W. 1995. CSP and determinism in security modelling. In Proceedings of the 1995 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos, CA, 114-127.
ROSENBERG, A. L. 1995. Thoughts on parallelism and concurrency in computing curricula. ACM Comput. Surv. 27, 2 (June), 280-283.
ROY, V. AND DE SIMONE, R. 1990. Auto/Autograph. In Computer Aided Verification (CAV '90) (Piscataway, NJ, June), E. M. Clarke and R. P. Kurshan, Eds. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society, Providence, RI, 235-250.
SANGIORGI, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. Thesis, University of Edinburgh, Edinburgh, Scotland.
SASTRY, S., MEYER, G., TOMLIN, C., LYGEROS, J., GODBOLE, D., AND PAPPAS, G. 1995. Hybrid control in air traffic management systems. In Proceedings of the Thirty-Fourth IEEE Conference on Decision and Control, 1478-1483.
THIAGARAJAN, P. S. 1994. A trace based extension of linear time temporal logic. In Ninth Annual Symposium on Logic in Computer Science (LICS '94) (Versailles, France, July), Computer Society Press, Washington, D. C., 438-447.
THOMSEN, B. 1995. A theory of higher order communicating systems. Inf. Comput. 116, 1 (Jan.), 38-57.
THOMSEN, B., LETH, L., AND KUO, T.-M. 1996. A Facile tutorial. In Proceedings of CONCUR '96 - Seventh International Conference on Concurrency Theory, (Pisa, Italy), Lecture Notes in Computer Science, Vol. 1119, Springer-Verlag, Berlin, New York, 278-298.
VARDI, M. AND WOLPER, P. 1986. An automatatheoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS '86) (Cambridge, MA, June), Computer Society Press, 332-344.
WINSKEL, G. 1987. Petri nets, algebras, morphisms, and compositionality. Inf. Comput. 72, 197-238.
WINSKEL, G. 1989. An introduction to event structures. In REX School and Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (Noordwijkerhout, The Netherlands, May/ June), Lecture Notes in Computer Science, Vol. 354, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds., Springer-Verlag, Berlin, New York, 364-397.
WINSKEL, G. AND NIELSEN, M. 1995. Models for concurrency. In Handbook of Logic in Computer Science, Vol. 4, S. Abramsky, D. Gabbay, and T. S. E. Maibaum, Eds. Oxford University Press, New York, 1-148.