Mooly Sagiv
where else to find them
what they talk about
all 6 in the filters
where they keep going back
- OOPSLA3 editions2020–2024
- DeFi Security Summit2 editions2022–2024
- POPL2 editions2021–2022
all 5 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Sharon Shoham13 talks
- Shelly Grossman3 talks
- Oded Padon11 talks
- Michael Sammler16 talks
- Ranjit Jhala19 talks
- Peter Müller28 talks
| title | conference | date |
|---|---|---|
| Using LLM Generated Formal Specs to Prevent the Next DeFi Hack | ETHConf 2026 | 2026-06-08 |
LLM-generated specs convert informal intent into formal invariants (for example sum of balances equals the total) that feed provers like Certora’s, Rocq, Lean… | ||
| Why DeFi Security Matters | DeFi Security Summit 2024 | 2024-11-07 |
Conference founded four years ago to close concrete DeFi security gaps, running an annual marketing-free summit that now includes technical workshops, a career… | ||
| Practical Verification Of Smart Contracts Using Memory Splitting | OOPSLA 2024 | 2024-10-20 |
The paper implements a conservative memory analysis and a memory-splitting transformation for EVM bytecode, integrated into CertoraProver, that recovers… | ||
| Trust but Verify: Scaling Deductive Verification with Abstract Interpretation | N40AI 2024 | 2024-01-20 |
Certora Prover verifies EVM and Wasm bytecode by combining abstract interpretation with SMT solving, an internal decompiler to a TP IR, and mutation testing… | ||
| Counterexample Driven Quantifier Instantiations with Applications to Distribute... | OOPSLA 2023 | 2023-10-23 |
Replaces problematic function symbols with a one-to-one relational abstraction inside Ivy and drives refinements by solver counterexamples; SMT solvers that… | ||
| Welcome and Overview | DeFi Security Summit 2022 | 2022-08-27 |
Overview lays out concrete goals: make the summit recurring, build a community of DeFi builders, auditors, bug bounty platforms and toolmakers, and push for… | ||
| Property-Directed Reachability as Abstract Interpretation in the Monotone Theory | POPL 2022 | 2022-01-16 |
Claims that propositional PDR is an instance of abstract interpretation by defining Lambda-PDR (take all counterexample generalizations) and a logical abstract… | ||
| Learning the Boundary of Inductive Invariants | POPL 2021 | 2021-01-17 |
An interpolation-based invariant inference algorithm with model-based generalization (dropping literals) uses bounded model checking to implement membership… | ||
| Taming Callbacks for Smart Contract Modularity | OOPSLA 2020 | 2020-11-15 |
Paper claims the first sound semantic static algorithm to ensure callbacks don’t break modular reasoning, and ships ECFChecker that decompiles EVM bytecode… | ||
| nothing matches | ||