| 2026 | CAV | Lagrangian-Based Duality for Quantified SMT Algorithms. | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham |
| 2026 | IJCAR | Automatic Abstraction Refinement for Hyperproperties Verification. | Malak Marrid, Shachar Itzhaky, Sharon Shoham, Yakir Vizel |
| 2026 | LICS | Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property. | Neta Elad, Sharon Shoham |
| 2026 | TACAS | Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings. | Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham |
| 2025 | TACAS | Implicit Rankings for Verifying Liveness Properties in First-Order Logic. | Raz Lotan, Sharon Shoham |
| 2024 | ATVA | Proving Cutoff Bounds for Safety Properties in First-Order Logic. | Raz Lotan, Eden Frenkel, Sharon Shoham |
| 2024 | CAV | Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. | Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham |
| 2024 | CAV | mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic. | James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham |
| 2024 | ESOP | Hyperproperty Verification as CHC Satisfiability. | Shachar Itzhaky, Sharon Shoham, Yakir Vizel |
| 2024 | TACAS | Speculative SAT Modulo SAT. | Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel |
| 2023 | CAV | Fast Approximations of Quantifier Elimination. | Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel |
| 2022 | SAS | Invariant Inference with Provable Complexity from the Monotone Theory. | Yotam M. Y. Feldman, Sharon Shoham |
| 2022 | TACAS | Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. | Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken |
| 2021 | ESOP | Run-time Complexity Bounds Using Squeezers. | Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2021 | FMCAD | Logical Characterization of Coherent Uninterpreted Programs. | Hari Govind V. K., Sharon Shoham, Arie Gurfinkel |
| 2021 | SIGCOMM | Cost-effective capacity provisioning in wide area networks with Shoofly. | Rachee Singh, Nikolaj S. Bjrner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette |
| 2020 | CAV | Global Guidance for Local Generalization in Model Checking. | Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel |
| 2020 | VMCAI | Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. | Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2020 | VMCAI | Solving $\mathrm {LIA} ^\star $ Using Approximations. | Maxwell Levatich, Nikolaj S. Bjrner, Ruzica Piskac, Sharon Shoham |
| 2019 | CAV | Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. | Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham |
| 2019 | CAV | Inferring Inductive Invariants from Phase Structures. | Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv |
| 2019 | CAV | Property Directed Self Composition. | Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel |
| 2018 | ATVA | Quantifiers on Demand. | Arie Gurfinkel, Sharon Shoham, Yakir Vizel |
| 2018 | ATVA | Modular Verification of Concurrent Programs via Sequential Model Checking. | Dan Rasin, Orna Grumberg, Sharon Shoham |
| 2018 | FMCAD | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | ICSE | Programming not only by example. | Hila Peleg, Sharon Shoham, Eran Yahav |
| 2018 | PLDI | Modularity for decidability of deductive verification with applications to distributed systems. | Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos |
| 2018 | SAS | Abstract Interpretation of Stateful Networks. | Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner |
| 2018 | SAS | Interactive Verification of Distributed Protocols Using Decidable Logic. | Sharon Shoham |
| 2018 | VMCAI | Abstraction-Based Interaction Model for Synthesis. | Hila Peleg, Shachar Itzhaky, Sharon Shoham |
| 2017 | CAV | Synthesis with Abstract Examples. | Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav |
| 2017 | WSDM | Synthesis of Forgiving Data Extractors. | Adi Omari, Sharon Shoham, Eran Yahav |
| 2017 | SAS | Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. | Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky |
| 2017 | TACAS | Bounded Quantifier Instantiation for Checking Inductive Invariants. | Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | Property Directed Reachability for Proving Absence of Concurrent Modification Errors. | Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhotk, Oded Padon, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | IC3 - Flipping the E in ICE. | Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik |
| 2016 | CAV | Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2016 | ICSE | Cross-supervised synthesis of web-crawlers. | Adi Omari, Sharon Shoham, Eran Yahav |
| 2016 | KDD | Lossless Separation of Web Pages into Layout Code and Data. | Adi Omari, Benny Kimelfeld, Eran Yahav, Sharon Shoham |
| 2016 | PLDI | Ivy: safety verification by interactive generalization. | Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham |
| 2016 | POPL | Decidability of inferring inductive invariants. | Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv |
| 2016 | TACAS | Some Complexity Results for Stateful Network Verification. | Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham |
| 2016 | VMCAI | D^3 : Data-Driven Disjunctive Abstraction. | Hila Peleg, Sharon Shoham, Eran Yahav |
| 2016 | VMCAI | Property Directed Abstract Interpretation. | Noam Rinetzky, Sharon Shoham |
| 2015 | CAV | Property-Directed Inference of Universal Invariants or Proving Their Absence. | Aleksandr Karbyshev, Nikolaj S. Bjrner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2015 | FM | Automated Circular Assume-Guarantee Reasoning. | Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2015 | POPL | Decentralizing SDN Policies. | Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham |
| 2013 | SAS | Symbolic Automata for Static Specification Mining. | Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang |
| 2013 | TACAS | Intertwined Forward-Backward Reachability Analysis Using Interpolants. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2012 | FMCAD | Lazy abstraction and SAT-based reachability in hardware model checking. | Yakir Vizel, Orna Grumberg, Sharon Shoham |
| 2012 | OOPSLA | Typestate-based semantic code search over partial programs. | Alon Mishne, Sharon Shoham, Eran Yahav |
| 2009 | ATVA | A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. | Yael Meller, Orna Grumberg, Sharon Shoham |
| 2007 | ISSTA | Static specification mining using automata-based abstractions. | Sharon Shoham, Eran Yahav, Stephen Fink, Marco Pistoia |
| 2007 | SAS | Compositional Verification and 3-Valued Abstractions Join Forces. | Sharon Shoham, Orna Grumberg |
| 2006 | LICS | 3-Valued Abstraction: More Precision at Less Cost. | Sharon Shoham, Orna Grumberg |
| 2005 | ATVA | Multi-valued Model Checking Games. | Sharon Shoham, Orna Grumberg |
| 2005 | VMCAI | Untitled record | Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham |
| 2004 | TACAS | Monotonic Abstraction-Refinement for CTL. | Sharon Shoham, Orna Grumberg |
| 2003 | CAV | A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. | Sharon Shoham, Orna Grumberg |