Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477661zbMATH OpenOpenAlexFDO

Authors Veronika Ortner, Norbert W. Schirmer

Publication date 6 July 2006

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

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

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1617313
• scientific article; zbMATH DE number 2086515
• Formal Methods in Computer-Aided Design
• Formal Methods for Hardware Verification
• BDD-based symbolic model checking
• Checking normality of Boolean functions
• Sanity Checks in Formal Verification
• scientific article; zbMATH DE number 1946864
• Verification and validation
• scientific article; zbMATH DE number 1757129

Cited in

(4)

• Bddl: A Type System for Binary Decision Diagrams
• Formula normalizations in verification
• Implementing and reasoning about hash-consed data structures in Coq
• A mechanical analysis of program verification strategies

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Theorem Proving in Higher Order Logics

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