Games and Decisions for Rigorous Systems Engineering
Sprache des Vortragstitels:
Dagstuhl Seminar 12461
Sprache des Tagungstitel:
A certificate of (un)satisfiability for a quantified Boolean formula (QBF)
represents concrete assignments to the variables of the formula. Certificates
are not only witnesses for the truth value returned by a QBF solver, but also
represent the solutions for practical applications of QBF like formal
verification and model checking.
Recently, an approach has been presented, which can be directly built on top of
DPLL based QBF solvers. Starting from resolution proofs produced by the solver
during clause and cube learning, the certificates are constructed by certain
syntactic properties of the proof tree.
Based on our integrated set of tools realizing resolution-based certificate
extraction for QBFs in prenex conjunctive normal form, in this talk, we discuss
the state-of-the-art of QBF certification and point out future challenges.
Sprache der Kurzfassung:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung