Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68532OpenAlexW2484880499MaRDI QIDQ5477661FDOQ5477661

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

Recommendations

• Publication:2722044
• 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

Mathematics Subject Classification ID

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

Cited In (4)

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

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)