Monotonic Abstraction-Refinement for CTL. - Sharon Shoham; Orna Grumberg (TACAS, 2004)

Don't Know in the µ-Calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (VMCAI, 2005)

Local Abstraction-Refinement for the mu-Calculus. - Harald Fecher; Sharon Shoham (SPIN, 2007)

When not losing is better than winning: Abstraction and refinement for the full mu-calculus. - Orna Grumberg; Martin Lange; Martin Leucker; Sharon Shoham (Inf. Comput., 2007)

A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. - Sharon Shoham; Orna Grumberg (ACM Trans. Comput. Log., 2007)

State Focusing: Lazy Abstraction for the Mu-Calculus. - Harald Fecher; Sharon Shoham (SPIN, 2008)

3-Valued abstraction: More precision at less cost. - Sharon Shoham; Orna Grumberg (Inf. Comput., 2008)

Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules. - Sharon Shoham; Nissim Francez (Stud Logica, 2008)

Static Specification Mining Using Automata-Based Abstractions. - Sharon Shoham; Eran Yahav; Stephen J. Fink; Marco Pistoia (IEEE Trans. Software Eng., 2008)

Abstraction-refinement and modularity in μ-calculus model checking. - Sharon Shoham (2009)

Compositional verification and 3-valued abstractions join forces. - Sharon Shoham; Orna Grumberg (Inf. Comput., 2010)

Local abstraction-refinement for the μ-calculus. - Harald Fecher; Sharon Shoham (Int. J. Softw. Tools Technol. Transf., 2011)

Lazy abstraction and SAT-based reachability in hardware model checking. - Yakir Vizel; Orna Grumberg; Sharon Shoham (FMCAD, 2012)

Typestate-based semantic code search over partial programs. - Alon Mishne; Sharon Shoham; Eran Yahav (OOPSLA, 2012)

Multi-valued model checking games. - Sharon Shoham; Orna Grumberg (J. Comput. Syst. Sci., 2012)

Symbolic Automata for Static Specification Mining. - Hila Peleg; Sharon Shoham; Eran Yahav; Hongseok Yang (SAS, 2013)

Intertwined Forward-Backward Reachability Analysis Using Interpolants. - Yakir Vizel; Orna Grumberg; Sharon Shoham (TACAS, 2013)

SAT-based Model Checking: Interpolation, IC3, and Beyond. - Orna Grumberg; Sharon Shoham; Yakir Vizel (Software Systems Safety, 2014)

Decentralizing SDN Policies. - Oded Padon; Neil Immerman; Aleksandr Karbyshev; Ori Lahav 001; Mooly Sagiv; Sharon Shoham (POPL, 2015)

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. - Karam Abd Elkader; Orna Grumberg; Corina S. Pasareanu; Sharon Shoham (CAV (1), 2016)

Cross-supervised synthesis of web-crawlers. - Adi Omari; Sharon Shoham; Eran Yahav (ICSE, 2016)

Lossless Separation of Web Pages into Layout Code and Data. - Adi Omari; Benny Kimelfeld; Eran Yahav; Sharon Shoham (KDD, 2016)

Ivy: safety verification by interactive generalization. - Oded Padon; Kenneth L. McMillan; Aurojit Panda; Mooly Sagiv; Sharon Shoham (PLDI, 2016)

Decidability of inferring inductive invariants. - Oded Padon; Neil Immerman; Sharon Shoham; Aleksandr Karbyshev; Mooly Sagiv (POPL, 2016)

SMT-based verification of parameterized systems. - Arie Gurfinkel; Sharon Shoham; Yuri Meshman (SIGSOFT FSE, 2016)

D^3 : Data-Driven Disjunctive Abstraction. - Hila Peleg; Sharon Shoham; Eran Yahav (VMCAI, 2016)

Property Directed Abstract Interpretation. - Noam Rinetzky; Sharon Shoham (VMCAI, 2016)

Symbolic automata for representing big code. - Hila Peleg; Sharon Shoham; Eran Yahav; Hongseok Yang (Acta Informatica, 2016)

A framework for compositional verification of multi-valued systems via abstraction-refinement. - Yael Meller; Orna Grumberg; Sharon Shoham (Inf. Comput., 2016)

Synthesis with Abstract Examples. - Dana Drachsler-Cohen; Sharon Shoham; Eran Yahav (CAV (1), 2017)

RATCOP: Relational Analysis Tool for Concurrent Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (Haifa Verification Conference, 2017)

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (SAS, 2017)

Property Directed Reachability for Proving Absence of Concurrent Modification Errors. - Asya Frumkin; Yotam M. Y. Feldman; Ondrej Lhoták; Oded Padon; Mooly Sagiv; Sharon Shoham (VMCAI, 2017)

IC3 - Flipping the E in ICE. - Yakir Vizel; Arie Gurfinkel; Sharon Shoham; Sharad Malik (VMCAI, 2017)

Synthesis of Forgiving Data Extractors. - Adi Omari; Sharon Shoham; Eran Yahav (WSDM, 2017)

Modular Safety Verification for Stateful Networks. - Kalev Alpernas; Roman Manevich; Aurojit Panda; Mooly Sagiv; Scott Shenker; Sharon Shoham; Yaron Velner (CoRR, 2017)

Property-Directed Inference of Universal Invariants or Proving Their Absence. - Aleksandr Karbyshev; Nikolaj S. Bjørner; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (J. ACM, 2017)

Paxos made EPR: decidable reasoning about distributed protocols. - Oded Padon; Giuliano Losa; Mooly Sagiv; Sharon Shoham (Proc. ACM Program. Lang., 2017)

Quantifiers on Demand. - Arie Gurfinkel; Sharon Shoham; Yakir Vizel (ATVA, 2018)

Modular Verification of Concurrent Programs via Sequential Model Checking. - Dan Rasin; Orna Grumberg; Sharon Shoham (ATVA, 2018)

Inferring Program Extensions from Traces. - Roman Manevich; Sharon Shoham (ICGI, 2018)

Programming not only by example. - Hila Peleg; Sharon Shoham; Eran Yahav (ICSE, 2018)

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 (PLDI, 2018)

Abstract Interpretation of Stateful Networks. - Kalev Alpernas; Roman Manevich; Aurojit Panda; Mooly Sagiv; Scott Shenker; Sharon Shoham; Yaron Velner (SAS, 2018)

Interactive Verification of Distributed Protocols Using Decidable Logic. - Sharon Shoham (SAS, 2018)

Abstraction-Based Interaction Model for Synthesis. - Hila Peleg; Shachar Itzhaky; Sharon Shoham (VMCAI, 2018)

Order out of Chaos: Proving Linearizability Using Local Views. - Yotam M. Y. Feldman; Constantin Enea; Adam Morrison 001; Noam Rinetzky; Sharon Shoham (DISC, 2018)

Undecidability of Inferring Linear Integer Invariants. - Sharon Shoham (CoRR, 2018)

Automated circular assume-guarantee reasoning. - Karam Abd Elkader; Orna Grumberg; Corina S. Pasareanu; Sharon Shoham (Formal Aspects Comput., 2018)

Reducing liveness to safety in first-order logic. - Oded Padon; Jochen Hoenicke; Giuliano Losa; Andreas Podelski; Mooly Sagiv; Sharon Shoham (Proc. ACM Program. Lang., 2018)

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. - Idan Berkovits; Marijana Lazic; Giuliano Losa; Oded Padon; Sharon Shoham (CAV (2), 2019)

Inferring Inductive Invariants from Phase Structures. - Yotam M. Y. Feldman; James R. Wilcox; Sharon Shoham; Mooly Sagiv (CAV (2), 2019)

Property Directed Self Composition. - Ron Shemer; Arie Gurfinkel; Sharon Shoham; Yakir Vizel (CAV (1), 2019)

Some complexity results for stateful network verification. - Kalev Alpernas; Aurojit Panda; Alexander Rabinovich; Mooly Sagiv; Scott Shenker; Sharon Shoham; Yaron Velner (Formal Methods Syst. Des., 2019)

Bounded Quantifier Instantiation for Checking Inductive Invariants. - Yotam M. Y. Feldman; Oded Padon; Neil Immerman; Mooly Sagiv; Sharon Shoham (Log. Methods Comput. Sci., 2019)

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (VMCAI, 2020)

Solving $ mathrm {LIA} ^ star $ Using Approximations. - Maxwell Levatich; Nikolaj S. Bjørner; Ruzica Piskac; Sharon Shoham (VMCAI, 2020)

Programming by predicates: a formal model for interactive synthesis. - Hila Peleg; Shachar Itzhaky; Sharon Shoham; Eran Yahav (Acta Informatica, 2020)

A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (CoRR, 2020)

Complexity and information in invariant inference. - Yotam M. Y. Feldman; Neil Immerman; Mooly Sagiv; Sharon Shoham (Proc. ACM Program. Lang., 2020)

Proving highly-concurrent traversals correct. - Yotam M. Y. Feldman; Artem Khyzha; Constantin Enea; Adam Morrison 001; Aleksandar Nanevski; Noam Rinetzky; Sharon Shoham (Proc. ACM Program. Lang., 2020)

Run-time Complexity Bounds Using Squeezers. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (ESOP, 2021)

Logical Characterization of Coherent Uninterpreted Programs. - Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (FMCAD, 2021)

Cost-effective capacity provisioning in wide area networks with Shoofly. - Rachee Singh; Nikolaj S. Bjørner; Sharon Shoham; Yawei Yin; John Arnold; Jamie Gaudette (SIGCOMM, 2021)

Temporal prophecy for proving temporal properties of infinite-state systems. - Oded Padon; Jochen Hoenicke; Kenneth L. McMillan; Andreas Podelski; Mooly Sagiv; Sharon Shoham (Formal Methods Syst. Des., 2021)

Learning the boundary of inductive invariants. - Yotam M. Y. Feldman; Mooly Sagiv; Sharon Shoham; James R. Wilcox (Proc. ACM Program. Lang., 2021)

SAT-Based Invariant Inference and Its Relation to Concept Learning. - Yotam M. Y. Feldman; Sharon Shoham (RP, 2022)

Invariant Inference with Provable Complexity from the Monotone Theory. - Yotam M. Y. Feldman; Sharon Shoham (SAS, 2022)

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. - Jason R. Koenig; Oded Padon; Sharon Shoham; Alex Aiken (TACAS (1), 2022)

Property-directed reachability as abstract interpretation in the monotone theory. - Yotam M. Y. Feldman; Mooly Sagiv; Sharon Shoham; James R. Wilcox (Proc. ACM Program. Lang., 2022)

Solving constrained Horn clauses modulo algebraic data types and recursive functions. - Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (Proc. ACM Program. Lang., 2022)

Runtime Complexity Bounds Using Squeezers. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (ACM Trans. Program. Lang. Syst., 2022)

Fast Approximations of Quantifier Elimination. - Isabel Garcia-Contreras; Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (CAV (2), 2023)

From Concept Learning to SAT-Based Invariant Inference (Invited Talk). - Sharon Shoham (FSTTCS, 2023)

State Merging with Quantifiers in Symbolic Execution. - David Trabish; Noam Rinetzky; Sharon Shoham; Vaibhav Sharma 001 (ESEC/SIGSOFT FSE, 2023)

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. - Orr Tamir; Marcelo Taube; Kenneth L. McMillan; Sharon Shoham; Jon Howell; Guy Gueta; Mooly Sagiv (Proc. ACM Program. Lang., 2023)

Proving Cutoff Bounds for Safety Properties in First-Order Logic. - Raz Lotan; Eden Frenkel; Sharon Shoham (ATVA, 2024)

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. - Eden Frenkel; Tej Chajed; Oded Padon; Sharon Shoham (CAV (2), 2024)

mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic. - James R. Wilcox; Yotam M. Y. Feldman; Oded Padon; Sharon Shoham (CAV (2), 2024)

Hyperproperty Verification as CHC Satisfiability. - Shachar Itzhaky; Sharon Shoham; Yakir Vizel (ESOP (2), 2024)

Speculative SAT Modulo SAT. - Hari Govind V. K.; Isabel Garcia-Contreras; Sharon Shoham; Arie Gurfinkel (TACAS (1), 2024)

Hyperproperty-Preserving Register Specifications. - Yoav Ben Shimon; Ori Lahav 001; Sharon Shoham (DISC, 2024)

Hyperproperty-Preserving Register Specifications (Extended Version). - Yoav Ben Shimon; Ori Lahav 001; Sharon Shoham (CoRR, 2024)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. - Neta Elad; Oded Padon; Sharon Shoham (Proc. ACM Program. Lang., 2024)

Global guidance for local generalization in model checking. - Hari Govind Vediramana Krishnan; Yuting Chen; Sharon Shoham; Arie Gurfinkel (Formal Methods Syst. Des., 2024)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic. - Raz Lotan; Sharon Shoham (TACAS (1), 2025)

Axe 'Em: Eliminating Spurious States with Induction Axioms. - Neta Elad; Sharon Shoham (Proc. ACM Program. Lang., 2025)

A Primal-Dual Perspective on Program Verification Algorithms. - Takeshi Tsukada; Hiroshi Unno 001; Oded Padon; Sharon Shoham (Proc. ACM Program. Lang., 2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version). - Takeshi Tsukada; Hiroshi Unno 001; Oded Padon; Sharon Shoham (CoRR, 2025)

Preface of the special issue on the Conference on Computer-Aided Verification 2022. - Sharon Shoham; Yakir Vizel (Formal Methods Syst. Des., 2025)