Inference rules for programming languages with side effects in expressions
作者： Paul E. Black , Phillip J. Windley
DOI: 10.1007/BFB0105396
关键词: Computer science 、 Natural language processing 、 Programming paradigm 、 Inductive programming 、 Procedural programming 、 Subroutine 、 Logic programming 、 Fifth-generation programming language 、 Functional logic programming 、 Artificial intelligence 、 Declarative programming 、 Programming language
摘要: Much of the work on verifying software has been done simple, often artificial, languages or subsets existing to avoid difficult details. In trying verify a secure application written in C, we have encountered and overcome some semantically complicated uses language.
springer.com
sci-hub.se 参考文章(17)
Michael J.C. Gordon, Programming language theory and its implementation Prentice Hall International (UK) Ltd.. ,(1988)
Paul Curzon, Deriving Correctness Properties of Compiled Code theorem proving in higher order logics. pp. 327- 346 ,(1992) , 10.1016/B978-0-444-89880-7.50027-9
Paul E. Black, Phillip J. Windley, Autotically Synthesized Term Denotation Predicates: A Proof Aid theorem proving in higher order logics. pp. 46- 57 ,(1995) , 10.1007/3-540-60275-5_56
Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl Levitt, Ron A. Olsson, A Hierarchical Method for Reasoning about Distributed Programming Languages theorem proving in higher order logics. pp. 385- 400 ,(1995) , 10.1007/3-540-60275-5_78
Holger Busch, A Practical Method for Reasoning about Distributed Systems in a Theorem Prover theorem proving in higher order logics. pp. 106- 121 ,(1995) , 10.1007/3-540-60275-5_60
Samuel P. Harbison, Guy L. Steele, C, a reference manual ,(1984)
William L. Harrison, Myla M. Archer, Karl N. Levitt, A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language theorem proving in higher order logics. pp. 347- 356 ,(1992) , 10.1016/B978-0-444-89880-7.50028-0
Sara Kalvala, A Formulation of TLA in Isabelle theorem proving in higher order logics. pp. 214- 228 ,(1995) , 10.1007/3-540-60275-5_67
Frederick B. Cohen, A secure world-wide-web daemon Computers & Security. ,vol. 15, pp. 707- 724 ,(1996) , 10.1016/S0167-4048(96)00009-0
Michael A. Arbib, Suad Alagić, Proof rules for gotos Acta Informatica. ,vol. 11, pp. 139- 148 ,(1979) , 10.1007/BF00264021