Efficient Well-Definedness Checking

DOI10.1007/978-3-540-71070-7_8MaRDI QIDQ3541692zbMATH OpenOpenAlexFDO

Authors Ádám Darvas, Farhad Mehta, Arsenii Rudich

Publication date 27 November 2008

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71070-7_8

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A practical approach to partial functions in CVC Lite
• Reasoning About Incompletely Defined Programs
• The connection between two ways of reasoning about partial functions
• Protective interface specifications
• A logic covering undefinedness in program proofs

Cites work

• A logic covering undefinedness in program proofs
• A practical approach to partial functions in CVC Lite
• Adapting Calculational Logic to the Undefined
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Computer Aided Verification
• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 192880 (Why is no real title available?)
• scientific article; zbMATH DE number 517385 (Why is no real title available?)
• scientific article; zbMATH DE number 2080004 (Why is no real title available?)
• scientific article; zbMATH DE number 3322506 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
• On a Formalization of the Non-Definedness Notion
• On notation for ordinal numbers
• Simplify: a theorem prover for program checking
• The B-Book
• The TPTP problem library

Cited in

(3)

• Classical logic with partial functions
• Classical logic with partial functions
• A completeness proof for a regular predicate logic with undefined truth value

This page was built for publication: Efficient Well-Definedness Checking

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