Edmund M. Clarke
Research on Hoare Logic
- Thesis - Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems. Sept 1976. PDF
- Pathological Interaction of Programming Language Features. Clarke, E.M. CS-1976-15. PDF
- Hoare-axioms and the Semantics of Control Structures. Clarke, E.M. CS-1977-10. PDF
- Program Invariants as Fixed Points. Clarke, E.M. Proceedings: 18th Annual Symposium on Foundations of Computer Science, Providence, RI, October 31-November 2, 1977. PDF
- Programming Language Constructs for Which it is Impossible to Obtain Good Hoare-like Axiom Systems. Clarke, E.M. Journal of the Association for Computing Machinery, Vol. 26, No. l, pp. 129-147, January 1979. PDF
- Program Invariants as Fixed Points. Clarke, E.M. Computing, Vol. 21, No.4, pp. 273-294, 1979. PDF
- Synthesis of Resource Invariants for Concurrent Programs. Clarke, E.M. ACM TOPLAS, Vol. 2, No. 3, pp. 338-358, July 1980. PDF
- Proving the Correctness of Coroutines Without History Variables. Clarke, E.M.Acta Informatica, Vol.13, pp. 169-188, 1980. PDF
- On Effective Axiomatizations of Hoare Logics. Clarke, E.M., German, S.M., & Halpern, J.Y. Journal of the Association for Computing Machinery, Vol. 30, No. 3, pp. 612-636, July 1983. PDF
- The Characterization Problem for Hoare Logic. Clarke, E.M. Phil. Trans. R. Soc. Lond. A 312, 1984, pp.423-440. PDF
- Reasoning About Procedures as Parameters. S. M. German, E. M. Clarke, J. Y. Halpern. Information and Computation, Vol. 83, No. 3, pp 265-359, December 1989. PDF
- Reasoning about Procedures as Parameters in the Language L4. Clarke, E.M., German, S.M., & Halpern, J.Y.
Information and Computation, Vol. 83, No. 3, pp. 265-359, December 1989. PDF