Inductive assertions and operational semantics

DOI10.1007/B93958zbMATH Open1179.68089OpenAlexW219731125MaRDI QIDQ5897074FDOQ5897074

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

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

Mathematics Subject Classification ID

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

Cited In (8)

• Reasoning about iteration and recursion uniformly based on big-step semantics
• Operational semantics and generalized weakest preconditions
• Transforming Programs into Recursive Functions
• 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
• 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)