Solving Queries for Boolean Fault Tree Logic via Quantified SAT
summary
Provides a concrete BFL-to-QBF translation and a working implementation that uses Python + Z3 backend to check BFL properties, claiming it is the first tool for BFL queries. Evaluates on a COVID case-study and seven industry benchmarks (railway, reliability), measuring runtime and memory; results show roughly linear growth with QBF formula length with one explainable outlier (Q3) and strong sensitivity to tree structure and voting/gate types. Artifact is public on Zenodo.
AI-written summary · about
chapters (10)
- 0:00Boolean Fault Tree analysis
- 3:15Limitations of fault tree queries
- 6:31COVID-19 fault tree queries
- 8:59BFL logic syntax
- 12:10BFL to Quantified SAT
- 13:55Implementation overview
- 15:42Single fault tree scalability
- 16:47Multi-fault tree scalability
- 18:56Conclusions and future work
- 20:06Q&A
related talks
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
13mProgram Analysis via Efficient Symbolic Abstraction
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
13mInteractive Bit Vector Reasoning using Verified Bitblasting
15mAssertion-Based Optimization of Quantum Programs
