Threads today: 7
Posts today: 43
Most active: FixpointFeline
Top topic: μ-calculus alternation hierarchy
▸ Sub-boards
📐 Hoare Logic & WP Calculus
Triples, loop invariants, weakest preconditions, total correctness
Threads: 88 • Posts: 1,204
🗂️ Separation Logic
Frame rule, separating conjunction, heap reasoning, CSL
Threads: 71 • Posts: 1,093
✓ Model Checking
CTL, LTL, BDD methods, CEGAR, symbolic model checking
Threads: 64 • Posts: 923
⚖️ SMT & Theorem Provers
Z3, CVC5, Lean, Coq, Isabelle, Dafny, VeriFast, Boogie
Threads: 55 • Posts: 801
🔍 Theory Spotlight — μ-Calculus
The modal μ-calculus extends propositional modal logic with least and greatest fixpoint operators
μ and ν.
Many temporal logics can be encoded in the μ-calculus,
including CTL* and its widely used fragments — linear temporal logic and computational tree logic.
Model checking in the μ-calculus is intimately related to two-player parity games. Satisfiability of a modal μ-calculus formula is EXPTIME-complete — a fact KleenePurr proved constructively in Lean last month.
→ Discuss fixpoint operators in μ-calculus | Parity games thread | Wiki entry
| Thread | Replies | Views | Last Post | |
|---|---|---|---|---|
| 📢 |
ANN
[READ FIRST] Subforum Rules, LaTeX Guide, and Posting Etiquette
Please typeset all proof obligations. \hoare{P}{C}{Q} macros in the sidebar. No informal handwaving without a disclaimer...
|
12 replies | 2,341 views |
KleenePurr 02 Mar 2025 |
| 📌 |
STICKY
Hoare Logic Megathread: Triples, Invariants, and Completeness
Collecting all introductory & advanced resources. Hoare logic is a formal system for proving program correctness using {P} C {Q} triples...
|
187 replies | 11,402 views |
FixpointFeline 27 Mar 2025 |
| 📌 |
STICKY
Separation Logic: Frame Rule, Heap Reasoning, Concurrent SL
Separation logic extends Hoare logic with the separating conjunction *, enabling local reasoning about heap-manipulating programs...
|
143 replies | 9,870 views |
AbstractKitty 26 Mar 2025 |
| 🔥 |
HOT
NEW
μ-calculus alternation hierarchy: is depth 2 really enough in practice?
+9
LTL and CTL both sit at alternation depth ≤2. Surely for reactive systems this suffices? KleenePurr says no, and has a counterexample...
|
41 replies | 1,283 views |
KleenePurr 27 Mar 2025 |
| 💬 |
NEW
Automating SL fragments via SMT: Z3 vs CVC5 for heap entailments
+4
Trying to reduce decidable SL fragments to first-order SMT. Z3 chokes on ∃-quantified heap constraints; CVC5 fares better with arrays...
|
18 replies | 734 views |
GaloisCat 27 Mar 2025 |
| ✅ |
SOLVED
Weakest precondition for nested while-loops: stuck on double invariant
I keep getting a circular dependency when deriving WP for nested loops with shared state. AbstractKitty solved it with a relational invariant...
|
22 replies | 891 views |
AbstractKitty 22 Mar 2025 |
| 🔥 |
HOT
SPIN vs TLA+: which model checker do you actually use for concurrent protocols?
SPIN uses LTL + Promela, TLA+ uses a temporal action logic. Both have serious industrial users. Which do you reach for first?...
|
58 replies | 2,104 views |
FixpointFeline 26 Mar 2025 |
| 💬 |
Concurrent Separation Logic: when does CSL fall short of Iris?
Classic CSL requires disjoint ownership. Iris's ghost state model is strictly more expressive. FixpointFeline has a great example involving fine-grained locking...
|
34 replies | 1,456 views |
KleenePurr 25 Mar 2025 |
| ✅ |
SOLVED
SMT solver shootout: Z3, CVC5, Bitwuzla for bit-vector arithmetic verification
Running the SMT-COMP 2024 benchmarks locally. Z3 still wins on QF_LIA, Bitwuzla dominates QF_BV. Full benchmark table inside...
|
29 replies | 1,887 views |
GaloisCat 20 Mar 2025 |
| 💬 |
Parity games and μ-calculus model checking: NP ∩ co-NP, but is it in P?
Zielonka 1998, Jurdzinski 1998, and the quasi-polynomial algorithm from Calude et al. 2017. Still open in the strong sense?...
|
47 replies | 2,288 views |
AbstractKitty 24 Mar 2025 |
| 💬 |
NEW
Dafny vs F*: choosing an automated verifier for my compiler project
+2
Dafny uses Boogie/Z3 as backend, F* is a full dependently-typed language. For a small compiler I want automated VCs not interactive proofs...
|
9 replies | 312 views |
GaloisCat 27 Mar 2025 |
| 🔒 |
LOCKED
Galois connections vs. fixpoint induction: which is more fundamental?
Locked after 120 replies due to off-topic debate. Summary post pinned at the end. TL;DR: they're equivalent via the Knaster-Tarski theorem...
|
120 replies | 5,501 views |
GaloisCat 15 Feb 2025 |
| 💬 |
CEGAR in practice: when does counterexample-guided refinement diverge?
The classic paper says convergence is guaranteed for finite state, but in practice spurious counterexamples accumulate. Anyone profiled BLAST or CPAchecker?
|
16 replies | 799 views |
FixpointFeline 12 Mar 2025 |
| 💬 |
Bi-abduction in Facebook Infer: the theory behind the industrial magic
Calcagno et al.'s bi-abduction combines abduction + entailment to automatically infer frame conditions. How does Infer's implementation trade soundness?
|
23 replies | 1,032 views |
KleenePurr 08 Mar 2025 |
| 💬 |
NEW
Relational Hoare Logic for proving program equivalence and non-interference
+1
Benton 2004, and its extensions for information flow. Running two programs in lockstep under a relational precondition is surprisingly tricky to automate...
|
5 replies | 187 views |
AbstractKitty 27 Mar 2025 |