Verification of parallel programs

References

• Apt , K. R. 1986 . Correctness Proofs of Distributed Termination Algorithms . ACM Transaction on Programming Languages and Systems , 8 ( 3 ) : 388 – 405 .
   Web of Science ®Google Scholar
• Banerjee , U. 1988 . Dependence Analysis for Supercomputing , Kluwer Academics Publishers .
   Google Scholar
• Boiten , E. A. , Partsch , H. A. , Tuijnman , D. and Volker , N. 1992 . How to produce correct Software-An Introduction to Formal Specification and Program Development by Transformations . The Computer Journal , 35 ( 6 ) : 547 – 554 .
   Web of Science ®Google Scholar
• Bowen , J. P. 1988 . 2nd IEE/BCS Conf. Software Engin . Formal Specification in Z as a Design and Documentation Tool . 1988 . pp. 164 – 168 .
   Google Scholar
• Boyer , R. S. , Elspas , B. and Levitt , K.N. 1975 . Reliable Software Intl. Conf. . SELECT-A Formal System for Testing and Debugging Programs by Symbolic Execution . 1975 . pp. 234 – 245 .
   Google Scholar
• Cherniavsky , J. C. and Smith , C. H. . Proc. of Workshop on Software Testing . A Theory of Program Testing with Applications . Canada. pp. 110 – 121 . Computer Society Press .
   Google Scholar
• Clarke , L. A. and Richardson , D. J. 1984 . “ Symbolic Evaluation-an Aid to Testing and Verification ” . In Software Validation , Edited by: Hausen , H. L. 141 – 167 . North-Holland .
   Google Scholar
• Cohen , D. , Swartout , W. and Balzer , R. 1982 . Using Symbolic Execution to Characterize Behaviour . ACM SIGSOFT Software Eng. Notes , 7 ( 5 ) : 25 – 32 .
   Google Scholar
• De Millo , R. A. , Lipton , R. J. and Perlis , A. J. 1979 . Social Processes and Proofs of Theorems and Programs . Communication of the ACM 22-5 , : 271 – 280 .
   Google Scholar
• Dijkstra , E. W. 1976 . A Discipline of Programming , Prentice-Hall .
   Google Scholar
• Dillon , L. K. 1988 . 3rd IEEE Int. Conf. on ADA Applic. and Env . Symbolic Execution-based Verification of ADA Tasking Programs . 3-13 1988 .
   Google Scholar
• Dillon , L. K. 1990 . Verifying General Safety Properties of ADA Tasking Programs . IEEE Trans. on Software Eng. , 16-1
   Google Scholar
• Dillon , L. K. , Kemmerer , R. A. and Harrison , L. J. 1988 . 2nd Workshop on Software Testing, Verification and Analysis . An Experience with Two Symbolic Execution-Based Approaches to Formal Verfication of ADA T asking Programs . 1988 . pp. 114 – 122 .
   Google Scholar
• Ehrig , H. , Mahr , B. , Classen , I. and Orejas , F. 1992a . Introduction to Algebraic Specification Part 1: Formal Methods for Software Development . The Computer Journal , 35 ( 5 ) 460 – 467 .
   Web of Science ®Google Scholar
• Ehrig , H. , Mahr and Orejas , F. 1992b . Introduction to Algebraic Specification. Part 2: From Classical View to . The Computer Journal , 35 ( 5 ) 468 – 477 .
   Web of Science ®Google Scholar
• Evans , D. J. and Mohd-Saman , M. Y. 1993 . “ Determination of Parallelism in Programs ” . In In Software for Parallel Computation , Edited by: Kowalik , J. S. and Grandinelti , L. 163 – 175 . Springer-Verlag .
   Google Scholar
• Frankl , P. G. and Weyuker , E. J. . Proc. of Workshop on Software Testing . Data Flow Testing in the Prresence of Unexecutable Paths . Canada. pp. 4 – 13 . Computer Society Press .
   Google Scholar
• Good , D. I. , Cohen , R. M. and Keeton-Williams , J. 1979 . 6th ACM Symp. on Principles of Programming Language . Principles of Proving Concurrent Programs in Gypsy . 1979 . pp. 42 – 52 .
   Google Scholar
• Gries , D. 1977 . An Exercise in Proving Parallel Programs Correct . Communication of the ACM 20-12 , 921 – 930 .
   Google Scholar
• Gries , D. 1981 . The Science of Programming , Springer-Verlag .
   Google Scholar
• Guaspari , D. , Marceau , C. and Polak , W. 1990 . Formal Verification of ADA Programs . IEEE Trans. on Software Eng. , 16-9
   Google Scholar
• Hall , P.A.V. 1988 . 2nd IEE/BCS Conf. Software Engin. . Towards Testing with Respect to Formal Specification . 1988 . pp. 159 – 163 .
   Google Scholar
• Hantler , S. L. and King , J. C. 1976 . An Introduction to proving Correctness of programs . ACM Computing Surveys , 8 ( 3 ) 331 – 353 .
   Web of Science ®Google Scholar
• Harrison , L. J. and Kemmerer , R. A. 1988 . Proc. of Third IEE Conf. on Ada Application and Environment . An Interleaving Symbolic Execution Approach for the Formal Verification of Ada Programs with Tasking . 15-26 1988 .
   Google Scholar
• Hoare , C. A. R. 1969 . An axiomatic basis for computer programming . Comm. of the ACM 12-10 , 576 – 583 .
   Google Scholar
• Howden , W. E. 1977 . Symbolic Testing and the DISSECT Symbolic Evaluation System . IEEE Trans, on Software Eng. , SE-3 ( 4 ) 266 – 278 .
   Web of Science ®Google Scholar
• Kemmerer , R. A. and Eckman , S. T. 1985 . UNISEX: a UNIx-based Symbolic Executor for Pascal . Software-Practice and Experience , 15 ( 5 ) 439 – 458 .
   Web of Science ®Google Scholar
• King , J. C. 1976 . Symbolic Execution and Program Testing . Communication of the ACM , 19 ( 7 ) 385 – 394 .
   Web of Science ®Google Scholar
• Leveson , N. G. 1986 . Software Safety: Why, What and How . ACM Computing Surveys , 18-2 125 – 163 .
   Google Scholar
• Masterson , J. J. , Ishaq , K. , Patel , S. , Norris , M. T. and Orr , R. A. 1988 . 2nd IEE/BCS Confi Software Engin . Intelligent Tools for formal Specification . 1988 . pp. 149 – 153 .
   Google Scholar
• Mc Parland , P. and Kilpatrick , P. . 2nd IEE/BCS Conf. Software Engin . Software Tools for VDM . 1988 . pp. 154 – 158 .
   Google Scholar
• Misra , J. and Chandy , K. M. 1981 . Proofs of Networks of Processes . IEEE Trans. on SE , SE-7 ( 4 ) 417 – 426 .
   Google Scholar
• Mohd-Saman M. Y Automatic Parallelization of Programs PhD Loughborough University of Technology
   Google Scholar
• Mohd-Saman , M. Y. and Evans , D. J. 1993 . Investigation of a Set of Bernstein Tests for the Detection of Loop Parallelization . Parallel Computing , 19 197 – 207 .
   Google Scholar
• Moser , L. E. and Melliar-Smith , P. M. 1990 . Formal Verification of Safety-critical Systems . Software-Practice and Experience , 20 ( 8 ) 799 – 821 .
   Web of Science ®Google Scholar
• Owicki , S. and Gries , D. 1976 . Verifying Properties of Parallel Programs: An Axiomatic Approach . Communication of the ACM , 19 ( 5 ) 279 – 285 .
   Web of Science ®Google Scholar
• Perrot , R. H. 1987 . Parallel Programming , Addison-Wesley .
   Google Scholar
• Ploedeveda , E. 1984 . “ Symbolic Evaluation as a Basis for integrated validation ” . In Software validation , Edited by: Hansen , HC . 167 – 185 . North-Holland .
   Google Scholar
• Sneed , H. M. . Proc. of Workshop on Software Testing . Data Coverage Measurement in Program Testing . Canada. pp. 34 – 40 . Computer Society Press .
   Google Scholar
• Williams S. A. Approaches to the Determination for Parallelism for Computer Programs PhD Loughborough University of Technology 1978
   Google Scholar
• Wolfe , M. 1989 . Optimizing Supercompilers for Supercomputers , London : Pitman .
   Google Scholar
• Wordsworth , J. B. 1988 . 2nd IEE/BCS Conf. Software Engin. . Specifying and Refining Programs with Z . 1988 . pp. 8 – 16 .
   Google Scholar
• Young , M. and Taylor , R. N. . Proc. of Workshop on Software Testing . Combining Static Concurrency Analysis with Symbolic Execution . Canada. pp. 170 – 178 . Computer Society Press .
   Google Scholar