Inductive assertions and operational semantics

DOI10.1007/B93958MaRDI QIDQ5897074zbMATH OpenOpenAlexFDO

Authors J Strother Moore

Publication date 5 February 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b93958

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Inductive assertion method for logic pograms
• scientific article; zbMATH DE number 4037276
• Formal Methods in Computer-Aided Design
• Logic programs as specifications in the inductive verification of logic programs
• Assertion based inductive verification methods for logic programs

Cited in

(8)

• Reasoning about iteration and recursion uniformly based on big-step semantics
• Operational semantics and generalized weakest preconditions
• Well-definedness and observational equivalence for inductive–coinductive programs
• A program logic for resources
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
• Transforming programs into recursive functions
• Formal Methods in Computer-Aided Design
• A mechanical analysis of program verification strategies

This page was built for publication: Inductive assertions and operational semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5897074)