Formula normalizations in verification

DOI10.1007/978-3-031-37709-9_19MaRDI QIDQ6535699zbMATH OpenFDO

Authors Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kuncak

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37709-9_19

Mathematics Subject Classification ID

Classical propositional logic (03B05) Specification and verification (program logics, model checking, etc.) (68Q60) Free lattices, projective lattices, word problems (06B25)

Recommendations

• Theorem Proving in Higher Order Logics
• Equivalence checking for orthocomplemented bisemilattices in log-linear time
• Normal Forms for Knowledge Compilation
• Simplification of boolean verification conditions
• Short Conjunctive Normal Forms in Finitely Valued Logics

Cites work

• scientific article; zbMATH DE number 3889596 (Why is no real title available?)
• scientific article; zbMATH DE number 758787 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3103212 (Why is no real title available?)
• A Brief Overview of Mizar
• A completion algorithm for lattice tree automata
• A note on orthomodular lattices
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Binary decision diagrams
• Boolean Rings for Intersection-Based Satisfiability
• Contract-based resource verification for higher-order functions with memoization
• Decision procedures. An algorithmic point of view
• Equivalence checking for orthocomplemented bisemilattices in log-linear time
• Finitely Presented Lattices
• Free Ortholattices
• Free lattices.
• Function summarization modulo theories
• HOL Light: An Overview
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• System description: E 1.8
• Term rewrite systems for lattice theory
• The Isabelle Framework

Cited in

(2)

• Verifying a realistic mutable hash table. Case study (short paper)
• Equivalence checking for orthocomplemented bisemilattices in log-linear time

This page was built for publication: Formula normalizations in verification

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