SATisfiable Algebraic Circuit Verification

Description

Although algebraic reasoning is one of the most successful methods for verifying gate-level integer multipliers, it has limitations with particular components, necessitating the use of SAT solvers in addition. As a result, proofs in two different formats are required for validation certifications. The validation results can only be trusted up to compositional reasoning because approaches to unifying certificates are not scalable. The use of dual variables in the algebraic encoding and replicating SAT-based notions in polynomial reasoning, on the other hand, eliminates the need for SAT solvers in the verification flow, resulting in a single, uniform proof certificate. In this session, I will discuss open issues in incorporating dual variables into algebraic reasoning.

Period	16 Feb 2022
Event title	unbekannt/unknown
Event type	Conference
Location	GermanyShow on map