3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 83
Текст из файла (страница 83)
B. Saxe, andR. Stata[2002] Extended static checking for Java, in: PLDI, pp. 234–245. Cited on pages18 and 241.L. Flon and N. Suzuki[1978] Nondeterminism and the correctness of parallel programs, in: Formal Description of Programming Concepts, E. J. Neuhold, ed., North-Holland,Amsterdam, pp. 598–608. Cited on page 370.[1981] The total correctness of parallel programs, SIAM J. Comput., pp.
227–246.Cited on page 370.R. Floyd[1967a] Assigning meaning to programs, in: Proceedings of Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science, J. T.Schwartz, ed., American Mathematical Society, New York, pp. 19–32.Cited on pages 12 and 122.[1967b] Nondeterministic algorithms, J. Assoc. Comput. Mach., 14, pp.
636–644.Cited on page 452.M. Fokkinga, M. Poel, and J. Zwiers[1993] Modular completeness for communication closed layers, in: CONCUR’93,E. Best, ed., Lecture Notes in Computer Science 715, Springer, New York,pp. 50–65. Cited on pages 266 and 305.M. Foley and C. A. R. Hoare[1971] Proof of a recursive program: Quicksort, Computer Journal, 14, pp. 391–395. Cited on pages 101, 125, 172, and 183.Formal Systems (Europe) Ltd.[2003] Failures-Divergence Refinement: FDR 2 User Manual, Formal Systems(Europe) Ltd, May. Cited on page 406.N. Francez[1986] Fairness, Springer, New York.
Cited on page 455.[1992] Program Verification, Addison-Wesley, Reading, MA. Cited on page 405.N. Francez, R.-J. Back, and R. Kurki-Suonio[1992] On equivalence-completions of fairness assumptions, Formal Aspects ofComputing, 4, pp. 582–591. Cited on page 455.N. Francez, C. A. R. Hoare, D. J. Lehmann, and W. P. de Roever[1979] Semantics of nondeterminism, concurrency and communication, J.
Comput. System Sci., 19, pp. 290–308. Cited on page 405.References483N. Francez, D. J. Lehmann, and A. Pnueli[1984] A linear history semantics for languages for distributed computing, Theoretical Comput. Sci., 32, pp. 25–46. Cited on page 405.J.-Y. Girard, Y. Lafont, and P. Taylor[1989] Proofs and Types, Cambridge University Press, Cambridge, UK. Cited onpage 51.M. J. C. Gordon[1979] The Denotational Description of Programming Languages, An Introduction, Springer, New York. Cited on page 58.G.
A. Gorelick[1975] A complete axiomatic system for proving assertions about recursive andnonrecursive programs, Tech. Rep. 75, Department of Computer Science,University of Toronto. Cited on page 125.A. Grau, U. Hill, and H. Langmaack[1967] Translation of ALGOL 60, vol. 137 of “Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen”, Springer. Cited on pages150 and 183.D. Gries[1978] The multiple assignment statement, IEEE Trans. Softw. Eng., SE-4,pp. 89–93.
Cited on page 125.[1981] The Science of Programming, Springer, New York. Cited on pages 13,126, 361, and 370.[1982] A note on a standard strategy for developing loop invariants and loops,Sci. Comput. Programming, 2, pp. 207–214. Cited on pages 113 and 116.O. Grumberg, N. Francez, J. A. Makowsky, and W. P. de Roever[1985] A proof rule for fair termination of guarded commands, Information andControl, 66, pp. 83–102.
Cited on page 455.O. Grumberg and H. Veith[2008] eds., 25 Years of Model Checking – History, Achievements, Perspectives,vol. 5000 of Lecture Notes in Computer Science, Springer. Cited on page16.P. R. Halmos[1985] I Want to be a Mathematician: An Automatography, Springer, New York.Cited on page 26.D. Harel[1979] First-Order Dynamic Logic, Lecture Notes in Computer Science 68,Springer, New York. Cited on page 125.D.
Harel, D. Kozen, and J. Tiuryn[2000] Dynamic logic, MIT Press, Cambridge, MA. Cited on page 17.M. C. B. Hennessy and G. D. Plotkin[1979] Full abstraction for a simple programming language, in: Proceedings ofMathematical Foundations of Computer Science, Lecture Notes in Computer Science 74, Springer, New York, pp. 108–120. Cited on pages 14and 58.C. A. R. Hoare[1961a] Algorithm 64, Quicksort, Comm. ACM, 4, p. 321. Cited on pages 125and 183.[1961b] Algorithm 65, Find, Comm.
ACM, 4, p. 321. Cited on page 125.[1962] Quicksort, Comput. J., 5, pp. 10–15. Cited on pages 99, 125, 172,and 183.484References[1969]An axiomatic basis for computer programming, Comm. ACM, 12, pp. 576–580, 583. Cited on pages 12, 65, 68, and 125.[1971a] Procedures and parameters: an axiomatic approach, in: Proceedings ofSymposium on the Semantics of Algorithmic Languages, E. Engeler, ed.,vol. 188 of Lecture Notes in Mathematics, Springer, pp. 102–116.
Citedon pages 125 and 183.[1971b] Proof of a program: Find, Comm. ACM, 14, pp. 39–45. Cited on pages125 and 126.[1972] Towards a theory of parallel programming, in: Operating Systems Techniques, C. A. R. Hoare and R. H. Perrot, eds., Academic Press, London,pp. 61–71. Cited on pages 246, 254, 266, and 346.[1975] Parallel programming: an axiomatic approach, Computer Languages, 1,pp.
151–160. Cited on pages 14, 246, and 266.[1978] Communicating sequential processes, Comm. ACM, 21, pp. 666–677. Citedon pages 15, 374, and 405.[1985] Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, NJ. Cited on pages 15, 374, and 405.[1996] How did software get so reliable without proof?, in: FME’96: IndustrialBenefit and Advances in Formal Methods, M.-C.
Gaudel and J. C. P.Woodcock, eds., vol. 1051 of Lecture Notes in Computer Science, Springer,pp. 1–17. Cited on page 17.C. A. R. Hoare and N. Wirth[1973] An axiomatic definition of the programming language PASCAL, Acta Inf.,2, pp. 335–355. Cited on page 125.J. Hoenicke[2006] Combination of Processes, Data, and Time (Dissertation), Tech. Rep. Nr.9/06, University of Oldenburg, July. ISSN 0946-2910. Cited on page 406.J. Hoenicke and E.-R. Olderog[2002] CSP-OZ-DC: A combination of specification techniques for processes, dataand time, Nordic Journal of Computing, 9, pp. 301–334.
appeared March2003. Cited on page 406.J. Hooman and W. P. de Roever[1986] The quest goes on: a survey of proofsystems for partial correctness of CSP,in: Current Trends in Concurrency, Lecture Notes in Computer Science224, Springer, New York, pp. 343–395. Cited on page 405.M.
Huisman and B. Jacobs[2000] Java program verification via a Hoare logic with abrupt termination, in:FASE, T. S. E. Maibaum, ed., vol. 1783 of Lecture Notes in ComputerScience, Springer, pp. 284–303. Cited on page 240.INMOS Limited[1984] Occam Programming Manual, Prentice-Hall International, EnglewoodCliffs, NJ. Cited on pages 15, 374, and 406.B. Jacobs[2004] Weakest pre-condition reasoning for Java programs with JML annotations,Journal of Logic and Algebraic Programming, 58, pp.
61–88. Formal Methods for Smart Cards. Cited on page 240.W. Janssen, M. Poel, and J. Zwiers[1991] Action systems and action refinement in the development of parallel systems, in: CONCUR’91, J. C. M. Baeten and J. F. Groote, eds., LectureNotes in Computer Science 527, Springer, New York, pp. 669–716. Citedon page 305.References485C. B. Jones[1992] The Search for Tractable Ways of Reasoning about Programs, Tech. Rep.UMCS-92-4-4, Department of Computer Science, University of Manchester.
Cited on page 124.Y.-J. Joung[1996] Characterizing fairness implementability for multiparty interaction, in:Proceedings of International Colloquium on Automata Languages and Programming (ICALP ’96), F. M. auf der Heide and B. Monien, eds., LectureNotes in Computer Science 1099, Springer, New York, pp. 110–121. Citedon page 455.A. Kaldewaij[1990] Programming: The Derivation of Algorithms, Prentice-Hall International,Englewood Cliffs, N.J.
Cited on pages 13 and 183.E. Knapp[1992] Derivation of concurrent programs: two examples, Sci. Comput. Programming, 19, pp. 1–23. Cited on page 305.D. E. Knuth[1968] The Art of Computer Programming. Vol. 1: Fundamental Algorithms,Addison-Wesley, Reading, MA. Cited on page 272.D. König[1927] Über eine Schlußweise aus dem Endlichen ins Unendliche, Acta Litt. Ac.Sci., 3, pp. 121–130. Cited on page 272.L. Lamport[1977] Proving the correctness of multiprocess programs, IEEE Trans. Softw.Eng., SE-3:2, pp.
125–143. Cited on pages 12, 281, and 305.[1983] What good is temporal logic?, in: Proceedings of the IFIP Information Processing 1983, R. E. A. Mason, ed., North-Holland, Amsterdam, pp. 657–668. Cited on page 266.[1994] The temporal logic of actions, ACM Trans. Prog. Lang. Syst., 16, pp. 872–923. Cited on page 371.[2003] Specifying Systems – The TLA+ Language and Tools for Hardware andSoftware Engineers, Addison Wesley.
Cited on page 371.J.-L. Lassez and M. J. Maher[1984] Closures and fairness in the semantics of programming logic, TheoreticalComput. Sci., 29, pp. 167–184. Cited on page 455.P. E. Lauer[1971] Consistent formal theories of the semantics of programming languages,Tech. Rep. 25. 121, IBM Laboratory Vienna. Cited on pages 125 and 370.G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok[2005] How the design of JML accomodates both runtime assertion checking andformal verification, Sci. of Comput. Prog., 55, pp.
185–208. Cited on page17.D. J. Lehmann, A. Pnueli, and J. Stavi[1981] Impartiality, justice, and fairness: the ethics of concurrent termination,in: Proceedings of International Colloquium on Automata Languages andProgramming (ICALP ’81), O. Kariv and S. Even, eds., Lecture Notes inComputer Science 115, Springer, New York, pp. 264–277. Cited on page455.486ReferencesC. Lengauer[1993] Loop parallelization in the polytope model, in: CONCUR’93, E. Best, ed.,Lecture Notes in Computer Science 715, Springer, New York, pp. 398–416.Cited on page 371.G. Levin and D. Gries[1981] A proof technique for communicating sequential processes, Acta Inf., 15,pp.
281–302. Cited on pages 12 and 405.R. Lipton[1975] Reduction: a method of proving properties of parallel programs, Comm.ACM, 18, pp. 717–721. Cited on pages 15, 305, and 346.J. Loeckx and K. Sieber[1987] The Foundation of Program Verification, Teubner-Wiley, Stuttgart,2nd ed. Cited on pages 28, 125, and 150.B. P. Mahony and J. S. Dong[1998] Blending Object-Z and Timed CSP: an introduction to TCOZ, in: The20th International Conference on Software Engineering (ICSE’98), K. Futatsugi, R. Kemmerer, and K. Torii, eds., IEEE Computer Society Press,pp. 95–104. Cited on page 406.Z.
Manna and A. Pnueli[1991] The Temporal Logic of Reactive and Concurrent Systems – Specification,Springer, New York. Cited on pages 13 and 325.[1995] Temporal Verification of Reactive Systems – Safety, Springer, New York.Cited on pages 13 and 325.B. Meyer[1997] Object-Oriented Software Construction, Prentice Hall, 2nd ed. Cited onpage 17.R. Meyer, J. Faber, J.
Hoenicke, and A. Rybalchenko[2008] Model checking duration calculus: A practical approach, Formal Aspectsof Computing, 20, pp. 481–505. Cited on page 406.R. Milner[1980] A Calculus of Communicating Systems, Lecture Notes in Computer Science 92, Springer, New York. Cited on page 405.[1989] Communication and Concurrency, Prentice-Hall International, EnglewoodCliffs, NJ. Cited on page 405.J.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
