Formula normalizations in verification
From MaRDI portal
Publication:6535699
DOI10.1007/978-3-031-37709-9_19zbMATH Open1547.68427MaRDI QIDQ6535699
Mario Bucev, Simon Guilloud, Viktor Kuncak, Dragana Milovančević
Publication date: 1 February 2024
Specification and verification (program logics, model checking, etc.) (68Q60) Classical propositional logic (03B05) Free lattices, projective lattices, word problems (06B25)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decision procedures. An algorithmic point of view
- A note on orthomodular lattices
- Term rewrite systems for lattice theory
- Free lattices.
- System Description: E 1.8
- Automatic Verification of TLA + Proof Obligations with SMT Solvers
- Binary Decision Diagrams
- HOL Light: An Overview
- A Brief Overview of Mizar
- The Isabelle Framework
- Free Ortholattices
- Finitely Presented Lattices
- Implementing Superposition in iProver (System Description)
- Function Summarization Modulo Theories
- A Completion Algorithm for Lattice Tree Automata
- Contract-based resource verification for higher-order functions with memoization
- Boolean Rings for Intersection-Based Satisfiability
- Satisfiability Checking of Non-clausal Formulas Using General Matings
- Making higher-order superposition work
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
This page was built for publication: Formula normalizations in verification
