Michel Sintzoff
Abstract
The proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous computations; a hypothetical programming language is used, which includes functions and locations and allows their recursive composition. The application of the method in studying termination or correctness problems is discussed on particular programs.
- 1 Naur P., Checking of operand types in ALGOL compilers, BIT 5 (1965), 151-163.Google Scholar
Cross Ref
- 2 Van Wijngaarden A. (ed.), B. J. Mailloux, J.E.L. Peck and C.H.A. Koster, Report on the algorithmic language ALGOL68, Num. Math. 14 (1969), 79-218.Google ScholarDigital Library
- 3 Cooper D. C., Programs for mechanical program verification, in "Machine Intelligence 6", pp. 43-59, Edinburgh Univ. Press, 1971.Google Scholar
- 4 Curry H. B., R. Feys, Combinatory logic, North-Holl., Amsterdam, 1958.Google Scholar
- 5 King J. C., A program verifier, Ph.D. Thesis, Carnegie-Mellon Univ., 1969. Google ScholarDigital Library
- 6 Manna Z., Mc Carthy J., Properties of programs and partial function logic, in "Machine Intelligence5", pp. 27-38, Edin. Univ. Press, 1969.Google Scholar
- 7 Burstall R. M., Proving properties of programs by structural induction, Comp. J. 12(1969), 41-49.Google ScholarCross Ref
- 8 Reynolds J.C., GEDANKEN-A simple typeless language based on the principle of completeness and the reference concept, Comm. ACM 13(1970), 308-319. Google ScholarDigital Library
Index Terms
- Calculating properties of programs by valuations on specific models
Recommendations
Calculating properties of programs by valuations on specific models
Proceedings of ACM conference on Proving assertions about programsThe proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous ...
Calculating properties of programs by valuations on specific models
Proceedings of ACM conference on Proving assertions about programsThe proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous ...
Verifying General Safety Properties of Ada Tasking Programs
The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and ...
Comments