scientific article
From MaRDI portal
Publication:3384880
Leander Tentrup, Jesko Hecking-Harbusch
Publication date: 17 December 2021
Full work available at URL: https://arxiv.org/abs/1604.06752
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Applications of game theory (91A80) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
BOCoSy: Small but Powerful Symbolic Output-Feedback Control, Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification, Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems, Bounded model checking for hyperproperties, CAQE and QuAbS: Abstraction Based QBF Solvers
Cites Work
- Solving QBF with counterexample guided refinement
- Petri games: synthesis of distributed systems with causal memory
- A solver for QBFs in negation normal form
- A structure-preserving clause form translation
- Circuit-based search space pruning in QBF
- Dependency learning for QBF
- On expansion and resolution in CEGAR based QBF solving
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Lower Bounds
- Non-prenex QBF Solving Using Abstraction
- SAT-Based Synthesis Methods for Safety Specs
- Detecting Unrealizability of Distributed Fault-tolerant Systems
- Encodings of Bounded Synthesis
- Bounded Synthesis for Petri Games
- QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
- Nenofex: Expanding NNF for QBF Solving
- Beyond CNF: A Circuit-Based QBF Solver
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning
- Exploiting Circuit Representations in QBF Solving
