Reasoning about procedures as parameters in the language L4
DOI10.1016/0890-5401(89)90040-0zbMath0692.68011OpenAlexW1990487099MaRDI QIDQ583874
Steven M. German, Edmund M. Clarke, Joseph Y. Halpern
Publication date: 1989
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0890-5401(89)90040-0
completenessaxiom systemexpressivenessreasoning about programsAlgol-like languagelanguage L4partial correctness assertionsprocedures passed as parameters
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Related Items (4)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Correctness of programs with Pascal-like procedures without global variables
- On termination problems for finitely interpreted ALGOL-like programs
- A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs
- On relative completeness of Hoare logics
- The characterization problem for Hoare logics
- Effective Axiomatizations of Hoare Logics
- Ten Years of Hoare's Logic: A Survey—Part I
- Soundness and Completeness of an Axiom System for Program Verification
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
This page was built for publication: Reasoning about procedures as parameters in the language L4