3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 84
Текст из файла (страница 84)
Misra[2001] A Discipline of Multiprogramming: Programming Theory for DistributedApplications, Springer, New York. Cited on page 13.J. C. Mitchell[1990] Type systems in programming languages, in: Handbook of TheoreticalComputer Science, J. van Leeuwen, ed., Elsevier, Amsterdam, pp. 365–458. Cited on page 51.M.
Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim[2008] Integrating a formal method into a software engineering process with UMLand Java, Formal Aspects of Computing, 20, pp. 161–204. Cited on page406.C. Morgan[1994] Programming from Specifications, Prentice-Hall International, London,2nd ed. Cited on page 13.References487J. M. Morris[1982] A general axiom of assignment/ assignment and linked data structures/a proof of the Schorr-Wait algorithm, in: Theoretical Foundations ofProgramming Methodology, Lecture Notes of an International SummerSchool. Reidel. Cited on page 240.P.
Mueller, A. Poetzsch-Heffter, and G. T. Leavens[2006] Modular invariants for layered object structures, Sci. Comput. Program.,62, pp. 253–286. Cited on page 241.M. H. A. Newman[1942] On theories with a combinatorial definition of “equivalence”, Annals ofMath., 43, pp. 223–243. Cited on page 250.F. Nielson, H. R. Nielson, and C. Hankin[2004] Principles of Program Analysis, Springer, New York. Cited on page 16.H.
R. Nielson and F. Nielson[2007] Semantics with Applications: An Appetizer, Springer, London. Cited onpage 124.T. Nipkow and L. P. Nieto[1999] Owicki/Gries in Isabelle/HOL, in: Fundamental Approaches in SoftwareEnginering (FASE), J. P. Finance, ed., vol. 1577 of Lecture Notes in Computer Science, Springer, pp. 188–203. Cited on page 345.T. Nipkow, L. C. Paulson, and M. Wenzel[2002] Isabelle/HOL – A Proof Assistant for Higher-Order Logic, vol.
2283 ofLecture Notes in Computer Science, Springer. Cited on pages 17 and 345.E.-R. Olderog[1981] Sound and complete Hoare-like calculi based on copy rules, Acta Inf., 16,pp. 161–197. Cited on page 183.[1983a] A characterization of Hoare’s logic for programs with Pascal-like procedures, in: Proc. of the 15th ACM Symp. on Theory of Computing (STOC),ACM, April, pp. 320–329. Cited on page 183.[1983b] On the notion of expressiveness and the rule of adaptation, TheoreticalComput. Sci., 30, pp. 337–347. Cited on page 183.[1984] Correctness of programs with Pascal-like procedures without global variables, Theoretical Comput.
Sci., 30, pp. 49–90. Cited on page 183.E.-R. Olderog and K. R. Apt[1988] Fairness in parallel programs, the transformational approach, ACM Trans.Prog. Lang. Syst., 10, pp. 420–455. Cited on pages 325 and 455.E.-R. Olderog and A. Podelski[2009] Explicit fair scheduling for dynamic control, in: Correctness, Concurrency,Compositionality: Essays in Honor of Willem-Paul de Roever, D. Dams,U. Hannemann, and M. Steffen, eds., Lecture Notes in Computer Science,Springer. To appear. Cited on page 455.E.-R. Olderog and S. Rössig[1993] A case study in transformational design of concurrent systems, in: Theoryand Practice of Software Development, M.-C.
Gaudel and J.-P. Jouannaud,eds., vol. 668 of LNCS, Springer, pp. 90–104. Cited on page 406.S. Owicki[1978] Verifying concurrent programs with shared data classes, in: Proceedingsof the IFIP Working Conference on Formal Description of ProgrammingConcepts, E. J.
Neuhold, ed., North-Holland, Amsterdam, pp. 279–298.Cited on page 305.488ReferencesS. Owicki and D. Gries[1976a] An axiomatic proof technique for parallel programs, Acta Inf., 6, pp. 319–340. Cited on pages 12, 14, 15, 80, 257, 261, 262, 266, 268, 276, 292,305, 307, 308, 311, 314, 320, 321, and 345.[1976b] Verifying properties of parallel programs: an axiomatic approach, Comm.ACM, 19, pp. 279–285. Cited on pages 12 and 346.S. Owre and N. Shankar[2003] Writing PVS proof strategies, in: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), M. Archer, B.
D.Vito, and C. Muñoz, eds., no. CP-2003-212448 in: NASA Conference Publication, NASA Langley Research Center, Hampton, VA, Sept., pp. 1–15.Cited on page 17.D. Park[1979] On the semantics of fair parallelism, in: Proceedings of Abstract SoftwareSpecifications, D.
Bjørner, ed., Lecture Notes in Computer Science 86,Springer, New York, pp. 504–526. Cited on page 424.G. L. Peterson[1981] Myths about the mutual exclusion problem, Inf. Process. Lett., 12, pp. 223–252. Cited on page 327.C. Pierik and F. S. de Boer[2005] A proof outline logic for object-oriented programming, Theor. Comput.Sci., 343, pp. 413–442. Cited on page 240.G. D. Plotkin[1981] A Structural Approach to Operational Semantics, Tech. Rep. DAIMI-FN19, Department of Computer Science, Aarhus University.
Cited on pages14, 58, and 488.[1982] An operational semantics for CSP, in: Formal Description of ProgrammingConcepts II, D. Bjørner, ed., North-Holland, Amsterdam, pp. 199–225.Cited on page 405.[2004] A structural approach to operational semantics, J. of Logic and AlgebraicProgramming, 60–61, pp. 17–139. Revised version of Plotkin [1981]. Citedon page 14.A. Pnueli[1977] The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57. Cited on page13.J.-P.
Queille and J. Sifakis[1981] Specification and verification of concurrent systems in CESAR, in: Proceedings of the 5th International Symposium on Programming, Paris. Citedon page 16.M. Raynal[1986] Algorithms for Mutual Exclusion, MIT Press, Cambridge, MA. Cited onpage 346.J. C. Reynolds[1981] The Craft of Programming, Prentice-Hall International, Englewood Cliffs,NJ. Cited on page 124.[2002] Separation logic: A logic for shared mutable data structures, in: LICS,pp. 55–74. Cited on page 240.W. P. de Roever, F. S. de Boer, U. Hannemann, J.
Hooman, Y. Lakhnech,M. Poel, and J. Zwiers[2001] Concurrency Verification – Introduction to Compositional and Noncompositional Methods, Cambridge University Press. Cited on page 406.References489A. W. Roscoe[1994] Model-checking CSP, in: A Classical Mind – Essays in Honour of C.A.R.Hoare, A. Roscoe, ed., Prentice-Hall, pp. 353–378. Cited on page 406.[1998] The Theory and Practice of Concurrency, Prentice-Hall. Cited on page405.B. K. Rosen[1974] Correctness of parallel programs: the Church-Rosser approach, Tech. Rep.IBM Research Report RC 5107, T.
J. Watson Research Center, YorktownHeights, NY. Cited on page 266.S. Sagiv, T. W. Reps, and R. Wilhelm[2002] Parametric shape analysis via 3-valued logic, ACM Trans. Prog. Lang.Syst., 24, pp. 217–298. Cited on page 16.A. Salwicki and T. Müldner[1981] On the algorithmic properties of concurrent programs, in: Proceedings ofLogics of Programs, E. Engeler, ed., Lecture Notes in Computer Science125, Springer, New York, pp. 169–197. Cited on page 266.M. Schenke[1999] Transformational design of real-time systems – part 2: from program specifications to programs, Acta Informatica 36, pp. 67–99. Cited on page406.M. Schenke and E.-R. Olderog[1999] Transformational design of real-time systems – part 1: from requirementsto program specifications, Acta Informatica 36, pp. 1–65.
Cited on page406.F. B. Schneider and G. R. Andrews[1986] Concepts of concurrent programming, in: Current Trends in Concurrency,J. W. de Bakker, W. P. de Roever, and G. Rozenberg, eds., Lecture Notesin Computer Science 224, Springer, New York, pp. 669–716. Cited on page345.D. S. Scott and J. W. de Bakker[1969] A theory of programs. Notes of an IBM Vienna Seminar. Cited on page150.D. S. Scott and C. Strachey[1971] Towards a mathematical semantics for computer languages, Tech. Rep.PRG–6, Programming Research Group, University of Oxford. Cited onpage 58.W.
Stephan, B. Langenstein, A. Nonnengart, and G. Rock[2005] Verification support environment, in: Mechanizing Mathematical Reasoning, Essays in Honour of Jörg H. Siekmann on the Occasion of His 60thBirthday, D. Hutter and W. Stephan, eds., vol. 2605 of Lecture Notes inComputer Science, Springer, pp.
476–493. Cited on page 17.J. E. Stoy[1977] Denotational Semantics: The Scott-Strachey Approach to ProgrammingLanguage Theory, MIT Press, Cambridge, MA. Cited on page 58.A. Tarski[1955] A lattice-theoretic fixpoint theorem and its applications, Pacific J. Math,5, pp. 285–309. Cited on page 448.Terese[2003]Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press, Cambridge, UK.
Cited on page 266.490ReferencesJ. V. Tucker and J. I. Zucker[1988] Program Correctness over Abstract Data Types, with Error-State Semantics, North-Holland and CWI Monographs, Amsterdam. Cited on pages51 and 124.A. M. Turing[1949] On checking a large routine, Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69. Univ. Math. Laboratory, Cambridge, 1949. See also: F. L.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
