Colloquia and Seminars

Granular synchrony assigns a timing type to each communication link, and existing solvability results prove both safety and liveness under the promise that the synchronous subgraph satisfies a graph-theoretic reachability condition. That condition is global and hard to verify, and a protocol that silently relies on it can violate agreement when it fails. We ask instead whether agreement and validity can be made to hold on every timing graph, with the graph condition confined to termination — a guarantee we call condition-independent safety.

We show that the answer depends sharply on topology knowledge and fault type. For crash faults with f >= n/2, no graph-agnostic protocol can be safe on every timing graph while terminating on every graph meeting the CFT condition, but knowing only the identities of one's synchronous neighbors is enough to break this impossibility. For Byzantine faults with 2f + 1 <= n <= 3f − 2, even local knowledge fails: faulty processes can hide the topology that distinguishes a good graph from a bad one.

We then give deterministic and randomized locally graph-aware CFT protocols with condition-independent safety. Both replace quorum intersection with a specialized collection primitive. A process disseminates its safety-relevant state to its synchronous neighbors before participating, so intersecting collections share not merely an identity but the value it contributed.

LLMs are known to exhibit highly sparse computation patterns during training and inference, with multiple works exploiting these for improved model performance or reduced compute costs.

We present PAMM, a simple matrix-multiply approximation algorithm which enables runtime memory compression during both training and inference of LLMs.
Using PAMM we show that the QKV linear maps of the attention mechanism are extremely sparse during model pretraining, enabling as high as 512x memory compression for these modules.

We also demonstrate that PAMM can be used to compress the KV cache of an LLM during inference, by up to 20x with near-zero induced error on the model's performance.

Large language models increasingly translate and explain politically contested events, yet their outputs can introduce narrative bias while preserving the underlying facts.

We create two datasets covering the Russia–Ukraine war and the Israel–Palestine conflict, pairing neutral event descriptions with competing narratives curated from news outlets and Telegram channels.

We introduce a framework for measuring perspectival divergence: systematic alignment with competing narratives about the same events. We characterize model-specific tendencies through narrative framing, emotional manipulation, source credibility, social identity, and contested naming.

Across both datasets and four languages, we show that apparent neutrality varies with the conflict, language, and prompting context. To mitigate these effects, we adapt self-distancing, a psychological intervention that prompts models to adopt a distant observer’s perspective.

Across eight models, self-distancing reduces measured divergence by 45% on average while preserving event content in 93% of outputs. We further introduce Self-Distancing Activation Steering (SDAS), which extracts the internal representational shift induced by self-distancing and applies it during generation without fine-tuning or modifying the original prompt.

Across five open-weight models, SDAS reduces divergence by 58% while preserving event content in 91% of outputs. Steering directions also transfer between conflicts without additional tuning, offering a practical approach to measuring and reducing narrative bias without prescribing a preferred political viewpoint.

AI is driving unprecedented growth in data center compute, with the market projected to approach $2 trillion by 2030 and revenue growth averaging approximately 24% annually from 2025 to 2030. As AI adoption progresses from infrastructure and physical systems to scientific discovery, it is creating a major opportunity for verification and in particular formal verification - the crown of design. Natural-language interfaces and AI-driven productivity are introducing a new level of abstraction, while emerging examples of AI-assisted mathematical reasoning demonstrate the potential to extend scientific and engineering capabilities.

This keynote traces the evolution from the man–machine communication vision presented at DAC 1964, through collective intelligence and human-in-the-loop formal methods presented at JUG 2013, to today’s agentic verification workflows in Cadence ChipStack. These workflows combine specialized formal agents, proof engines, machine learning, and expert guidance to address properties that remain difficult to prove manually. By interleaving design and verification, and using platforms such as Cadence ChipStack, the Formal Verification AI Flywheel can transform productivity at scale into greater proof power, enabling engineers to build increasingly complex systems with higher confidence and much less manual effort.

Short bio:  Ziyad Hanna is a Corporate Vice President at Cadence Design Systems and R&D General Manager of Cadence Israel. He leads system verification products and Cadence-wide AI initiatives for autonomous chip-design development. Previously, he served as Senior Vice President of Jasper and senior PE and management roles at Intel, where he developed three generations of formal-verification suites widely deployed since the start of Pentium. Hanna earned degrees from Tel Aviv University and a PhD from Oxford University, where he is a visiting professor. An IEEE Senior Member, he has published over 30 articles, 20 patents, and delivered hundreds of industrial and academic presentations and talks. His honors include Intel IAA awards and an honorary doctorate from Ruppin Collage. Ziyad initiated a formal-verification course at the Technion that attracts hundreds of students interested in pursuing advanced studies in the field.