Formula normalizations in verification
From MaRDI portal
Publication:6535699
DOI10.1007/978-3-031-37709-9_19zbMATH Open1547.68427MaRDI QIDQ6535699FDOQ6535699
Authors: Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kuncak 
Publication date: 1 February 2024
Classical propositional logic (03B05) Specification and verification (program logics, model checking, etc.) (68Q60) Free lattices, projective lattices, word problems (06B25)
Cites Work
- The Isabelle Framework
- A Brief Overview of Mizar
- System description: E 1.8
- Title not available (Why is that?)
- HOL Light: An Overview
- Title not available (Why is that?)
- A completion algorithm for lattice tree automata
- Title not available (Why is that?)
- Free Ortholattices
- A note on orthomodular lattices
- Decision procedures. An algorithmic point of view
- Title not available (Why is that?)
- Contract-based resource verification for higher-order functions with memoization
- Term rewrite systems for lattice theory
- Finitely Presented Lattices
- Free lattices.
- Boolean Rings for Intersection-Based Satisfiability
- Binary decision diagrams
- Making higher-order superposition work
- Function summarization modulo theories
- Implementing Superposition in iProver (System Description)
- Satisfiability Checking of Non-clausal Formulas Using General Matings
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
- 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)
