3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 82
Текст из файла (страница 82)
199–216. Cited on page370.R.-J. Back and R. Kurki-Suonio[1988] Serializability in distributed systems with handshaking, in: Proceedingsof International Colloquium on Automata Languages and Programming(ICALP ’88), T. Lepistö and A. Salomaa, eds., Lecture Notes in ComputerScience 317, Springer, New York, pp. 52–66. Cited on page 455.R.-J. Back and J.
von Wright[2008] Refinement Calculus: A Systematic Introduction, Springer, New York.Cited on pages 13 and 370.R. C. Backhouse[1986] Program Construction and Verification, Prentice-Hall International, Englewood Cliffs, NJ. Cited on page 13.C. Baier and J.-P. Katoen[2008] Principles of Model Checking, MIT Press, Cambridge, MA. Cited on page16.J. W. de Bakker[1980] Mathematical Theory of Program Correctness, Prentice-Hall International,Englewood Cliffs, NJ.
Cited on pages 52, 87, 122, 124, 125, and 370.References479T. Ball, A. Podelski, and S. Rajamani[2002] Relative completeness of abstraction refinement for software model checking, in: Tools and Algorithms for the Construction and Analysis of Systems, J.-P. Katoen and P. Stevens, eds., vol. 2280 of Lecture Notes inComputer Science, Springer, pp. 158–172. Cited on page 16.M.
Balser[2006] Verifying Concurrent Systems with Symbolic Execution – Temporal Reasoning is Symbolic Execution with a Little Induction, PhD thesis, University of Augsburg, Shaker Verlag. Cited on page 346.M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums[2000] Formal system development in KIV, in: Proc. Fundamental Approachesto Software Engineering, T. Maibaum, ed., vol. 1783 of Lecture Notes inComputer Science, Springer, pp. 363–366. Cited on pages 17 and 346.A.
Banerjee and D. A. Naumann[2005] Ownership confinement ensures representation independence for objectoriented programs, J. ACM, 52, pp. 894–960. Cited on page 240.M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino[2005] Boogie: A modular reusable verifier for object-oriented programs, in:FMCO, pp. 364–387. Cited on page 240.D. Basin, E.-R. Olderog, and P. E. Sevinç[2007] Specifying and analyzing security automata using CSP-OZ, in: Proceedingsof the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), ACM Press, March, pp. 70–81. Citedon page 406.B. Beckert, R.
Hähnle, and P. H. Schmitt[2007] eds., Verification of Object-Oriented Software: The KeY Approach,vol. 4334 of Lecture Notes in Computer Science, Springer. Cited on pages17, 18, and 241.M. Ben-Ari[1990] Principles of Concurrent and Distributed Programming, Prentice-Hall International, Englewood Cliffs, NJ. Cited on page 346.J. van den Berg, B. Jacobs, and E. Poll[2001] Formal specification and verification of Java Card’s application identifierclass, in: Java on Smart Cards: Programming and Security, I. Attali andT. Jensen, eds., vol. 2041 of Lecture Notes in Computer Science, Springer,pp. 137–150.
Cited on page 18.E. Best[1996] Semantics of Sequential and Parallel Programs, Prentice-Hall International, London. Cited on page 266.E. Best and C. Lengauer[1989] Semantic independence, Sci. Comput. Programming, 13, pp. 23–50. Citedon page 266.F. S. de Boer[1991a] A proof system for the language POOL, in: Foundations of Object-OrientedLanguages, J. W. de Bakker, W. P. de Roever, and G.
Rozenberg, eds.,vol. 489 of Lecture Notes in Computer Science, Springer, pp. 124–150.Cited on page 12.[1991b] Reasoning about dynamically evolving process structures (A proof theory ofthe parallel object-oriented language POOL), PhD thesis, Free Universityof Amsterdam. Cited on page 240.480[1994]ReferencesCompositionality in the inductive assertion method for concurrent systems, in: Programming Concepts, Methods and Calculi, E.-R. Olderog, ed.,Elsevier/North-Holland, Amsterdam, pp.
289–305. Cited on page 305.A. Bouajjani, J.-C. Fernandez, N. Halbwachs, and P. Raymond[1992] Minimal state graph generation, Sci. Comput. Programming, 18, pp. 247–269. Cited on page 16.J. P. Bowen, C. A. R. Hoare, H. Langmaack, E.-R. Olderog, and A. P.Ravn[1996] A ProCoS II project final report: Esprit basic research project 7071,Bulletin of the European Association for Theoretical Computer Science(EATCS), 59, pp. 76–99. Cited on page 406.S.
D. Brookes[1993] Full abstraction for a shared variable parallel language, in: Proceedings,Eighth Annual IEEE Symposium on Logic in Computer Science (LICS’93), IEEE Computer Society Press, pp. 98–109. Cited on page 305.S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe[1984] A theory of communicating processes, J. Assoc. Comput. Mach., 31,pp. 560–599. Cited on page 405.J. R. Burch, E. M. Clarke, K.
L. McMillan, D. L. Dill, and L. J. Hwang[1992] Symbolic model checking: 1020 states and beyond, Information and Computation, 98, pp. 142–170. Cited on page 16.L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens,K. R. M. Leino, and E. Poll[2005] An overview of jml tools and applications, International Journal on Software Tools for Technology Transfer, 7, pp. 212–232. Cited on page 240.L. Cardelli[1991] Typeful programming, in: State of the Art Book: Formal Description ofProgramming Concepts, E. J.
Neuhold and M. Paul, eds., Springer, NewYork, pp. 431–507. Cited on page 51.K. M. Chandy and J. Misra[1988] Parallel Program Design: A Foundation, Addison-Wesley, New York.Cited on page 370.E. M. Clarke[1979] Programming language constructs for which it is impossible to obtain goodHoare axiom systems, J. Assoc. Comput. Mach., 26, pp. 129–147. Citedon pages 125 and 183.[1980] Proving correctness of coroutines without history variables, Acta Inf., 13,pp. 169–188. Cited on page 266.[1985] The characterization problem for Hoare logics, in: Mathematical Logic andProgramming Languages, C. A.
R. Hoare and J. C. Shepherdson, eds.,Prentice-Hall International, Englewood Cliffs, NJ, pp. 89–106. Cited onpage 183.E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith[2003] Counterexample-guided abstraction refinement for symbolic model checking, J. Assoc. Comput.
Mach., 50, pp. 752–794. Cited on page 16.E. M. Clarke, O. Grumberg, and D. A. Peled[1999] Model Checking, MIT Press, Cambridge, MA. Cited on page 16.M. Clint[1973] Program proving: Coroutines, Acta Inf., 2, pp. 50–63. Cited on page 266.References481S. A. Cook[1978] Soundness and completeness of an axiom system for program verification,SIAM J. Comput., 7, pp. 70–90.
Cited on page 125.P. Cousot and R. Cousot[1977a] Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixedpoints, in: Proc. of 4thACM Symp. on Principles of Progr. Languages (POPL), ACM, Jan.,pp. 238–252. Cited on page 16.[1977b] Automatic synthesis of optimal invariant assertions: mathematical foundations, in: ACM Symposium on Artificial Intelligence and ProgrammingLanguages, SIGPLAN Notices 12 (8), pp. 1–12.
Cited on page 449.O.-J. Dahl and K. Nygaard[1966] Simula - an Algol based simulation language, CACM, 9, pp. 671–678. Citedon page 240.D. van Dalen[2004] Logic and Structure, Springer, 4th ed. Cited on page 52.W. Damm and B. Josko[1983] A sound and relatively complete Hoare-logic for a language with highertype procedures, Acta Inf., 20, pp.
59–101. Cited on page 183.E. W. Dijkstra[1968] Cooperating sequential processes, in: Programming Languages: NATO Advanced Study Institute, F. Genuys, ed., Academic Press, London, pp. 43–112. Cited on pages 324, 331, and 346.[1975] Guarded commands, nondeterminacy and formal derivation of programs,Comm. ACM, 18, pp. 453–457. Cited on pages 15, 86, 125, 349, and 370.[1976] A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ. Citedon pages 13, 14, 15, 56, 113, 126, 349, 350, 370, and 424.[1977] A correctness proof for communicating processes —a small exercise. EWD607, Burroughs, Nuenen, the Netherlands. Cited on page 403.[1982] Selected Writings on Computing, Springer, New York.
Cited on page 125.E. W. Dijkstra and C. S. Scholten[1990] Predicate Calculus and Program Semantics, Springer, New York. Cited onpage 26.T. Elrad and N. Francez[1982] Decompositions of distributed programs into communication closed layers,Sci. Comput. Programming, 2, pp. 155–173. Cited on page 305.M. H. van Emden[1997] Value constraints in the CLP scheme, Constraints, 2, pp. 163–184.
Citedon page 455.E. A. Emerson and E. M. Clarke[1982] Using branching time temporal logic to synthesize synchronization skeletons, Sci. Comput. Programming, 2, pp. 241–266. Cited on page 16.W. H. J. Feijen and A. J. M. van Gasteren[1999] On a Method of Multiprogramming, Springer, New York. Cited on page13.J.-C. Filliâtre[2007] Formal proof of a program: Find, Sci. Comput.
Program., 64, pp. 332–340.Cited on pages 125 and 126.482ReferencesC. Fischer[1997] CSP-OZ: A combination of Object-Z and CSP, in: Formal Methods forOpen Object-Based Distributed Systems (FMOODS), H. Bowman andJ. Derrick, eds., vol. 2, Chapman & Hall, pp. 423–438.
Cited on page406.C. Fischer and H. Wehrheim[1999] Model-checking CSP-OZ specifications with FDR, in: Proc. 1st International Conference on Integrated Formal Methods (IFM), K. Araki, A. Galloway, and K. Taguchi, eds., Springer, pp. 315–334. Cited on page 406.M. J. Fischer and M. S. Paterson[1983] Storage requirements for fair scheduling, Inf. Process. Lett., 17, pp. 249–250. Cited on page 426.C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
