אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

Many program‑safety verification tasks reduce to deciding the satisfiability of Constrained Horn Clauses (CHCs). When a program depends on bit‑level behavior such as bitwise logic, shifts, or overflow‑sensitive arithmetic, encoding its CHCs over the theory of fixed‑size bit‑vectors is exact but scales poorly, whereas encoding them over integer arithmetic is far more tractable but requires an expensive modeling of the bit‑level operations that can cancel out the gain. We present the first implementation of a theory‑modular framework, designed by our advisors, that avoids committing to either theory. It partitions a set of bit‑vector CHCs into a bit‑vector fragment and an integer fragment linked by interface constraints, and a backward‑reasoning algorithm discharges the two with separate, theory‑specific solvers, crossing between them and iteratively strengthening the interface to avoid re‑deriving already‑refuted reasoning. We further present a proof‑of‑concept abstraction‑refinement extension that abstracts bit‑manipulating subexpressions during translation and refines them on demand, lightening the load on the bit‑vector solver.