Sharon Shoham

ORCID

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 92

Top Venues

CoRR

Proc. ACM Program. Lang.

VMCAI

CAV (2)

Publications

Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. CAV (2) (2024)
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
Speculative SAT Modulo SAT. TACAS (1) (2024)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperty Verification as CHC Satisfiability. ESOP (2) (2024)
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. CoRR (2024)
James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham
mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic. CAV (2) (2024)
Neta Elad, Oded Padon, Sharon Shoham
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. Proc. ACM Program. Lang. 8 (POPL) (2024)
David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma
State Merging with Quantifiers in Symbolic Execution. ESEC/SIGSOFT FSE (2023)
Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Sharon Shoham
From Concept Learning to SAT-Based Invariant Inference (Invited Talk). FSTTCS (2023)
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
Speculative SAT Modulo SAT. CoRR (2023)
Neta Elad, Oded Padon, Sharon Shoham
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. CoRR (2023)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperty Verification as CHC Satisfiability. CoRR (2023)
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Fast Approximations of Quantifier Elimination. CAV (2) (2023)
David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma
State Merging with Quantifiers in Symbolic Execution. CoRR (2023)
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Fast Approximations of Quantifier Elimination. CoRR (2023)
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. TACAS (1) (2022)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Property-directed reachability as abstract interpretation in the monotone theory. Proc. ACM Program. Lang. 6 (POPL) (2022)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6 (POPL) (2022)
Yotam M. Y. Feldman, Sharon Shoham
SAT-Based Invariant Inference and Its Relation to Concept Learning. RP (2022)
Yotam M. Y. Feldman, Sharon Shoham
Invariant Inference With Provable Complexity From the Monotone Theory. CoRR (2022)
Yotam M. Y. Feldman, Sharon Shoham
Invariant Inference with Provable Complexity from the Monotone Theory. SAS (2022)
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Runtime Complexity Bounds Using Squeezers. ACM Trans. Program. Lang. Syst. 44 (3) (2022)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR (2021)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Logical Characterization of Coherent Uninterpreted Programs. FMCAD (2021)
Dan Rasin, Orna Grumberg, Sharon Shoham
Modular Verification of Concurrent Programs via Sequential Model Checking. CoRR (2021)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Logical Characterization of Coherent Uninterpreted Programs. CoRR (2021)
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Some Complexity Results for Stateful Network Verification. CoRR (2021)
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. CoRR (2021)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Learning the boundary of inductive invariants. Proc. ACM Program. Lang. 5 (POPL) (2021)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. CoRR (2021)
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Run-time Complexity Bounds Using Squeezers. ESOP (2021)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR (2021)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57 (2) (2021)
Rachee Singh, Nikolaj Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
Cost-effective capacity provisioning in wide area networks with Shoofly. SIGCOMM (2021)
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. CoRR (2021)
Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav
Programming by predicates: a formal model for interactive synthesis. Acta Informatica 57 (1-2) (2020)
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs. CoRR (2020)
Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
Global Guidance for Local Generalization in Model Checking. CAV (2) (2020)
Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel
Global Guidance for Local Generalization in Model Checking. CoRR (2020)
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
Proving Highly-Concurrent Traversals Correct. CoRR (2020)
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. VMCAI (2020)
Maxwell Levatich, Nikolaj Bjørner, Ruzica Piskac, Sharon Shoham
Solving $\mathrm {LIA} ^\star $ Using Approximations. VMCAI (2020)
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
Proving highly-concurrent traversals correct. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
Complexity and information in invariant inference. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Learning the Boundary of Inductive Invariants. CoRR (2020)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. Log. Methods Comput. Sci. 15 (3) (2019)
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
Complexity and Information in Invariant Inference. CoRR (2019)
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. CoRR (2019)
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
Inferring Inductive Invariants from Phase Structures. CoRR (2019)
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Some complexity results for stateful network verification. Formal Methods Syst. Des. 54 (2) (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CAV (1) (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CoRR (2019)
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
Inferring Inductive Invariants from Phase Structures. CAV (2) (2019)
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. CAV (2) (2019)
Hila Peleg, Sharon Shoham, Eran Yahav
Programming not only by example. ICSE (2018)
Sharon Shoham
Undecidability of Inferring Linear Integer Invariants. CoRR (2018)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. ATVA (2018)
Sharon Shoham
Interactive Verification of Distributed Protocols Using Decidable Logic. SAS (2018)
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
Automated circular assume-guarantee reasoning. Formal Aspects Comput. 30 (5) (2018)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD (2018)
Dan Rasin, Orna Grumberg, Sharon Shoham
Modular Verification of Concurrent Programs via Sequential Model Checking. ATVA (2018)
Hila Peleg, Shachar Itzhaky, Sharon Shoham
Abstraction-Based Interaction Model for Synthesis. VMCAI (2018)
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
Modularity for decidability of deductive verification with applications to distributed systems. PLDI (2018)
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham
Order out of Chaos: Proving Linearizability Using Local Views. CoRR (2018)
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Abstract Interpretation of Stateful Networks. SAS (2018)
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2 (POPL) (2018)
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham
Order out of Chaos: Proving Linearizability Using Local Views. DISC (2018)
Roman Manevich, Sharon Shoham
Inferring Program Extensions from Traces. ICGI (2018)
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Paxos Made EPR: Decidable Reasoning about Distributed Protocols. CoRR (2017)
Adi Omari, Sharon Shoham, Eran Yahav
Synthesis of Forgiving Data Extractors. WSDM (2017)
Hila Peleg, Sharon Shoham, Eran Yahav
Programming Not Only by Example. CoRR (2017)
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Modular Safety Verification for Stateful Networks. CoRR (2017)
Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav
Synthesis with Abstract Examples. CAV (1) (2017)
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
RATCOP: Relational Analysis Tool for Concurrent Programs. Haifa Verification Conference (2017)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. TACAS (1) (2017)
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
IC3 - Flipping the E in ICE. VMCAI (2017)
Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
Property Directed Reachability for Proving Absence of Concurrent Modification Errors. VMCAI (2017)
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. SAS (2017)
Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64 (1) (2017)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. CoRR (2017)
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Noam Rinetzky, Sharon Shoham
Property Directed Abstract Interpretation. VMCAI (2016)
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv
Decidability of inferring inductive invariants. POPL (2016)
Adi Omari, Sharon Shoham, Eran Yahav
Cross-supervised synthesis of web-crawlers. ICSE (2016)
Adi Omari, Benny Kimelfeld, Eran Yahav, Sharon Shoham
Lossless Separation of Web Pages into Layout Code and Data. KDD (2016)
Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang
Symbolic automata for representing big code. Acta Informatica 53 (4) (2016)
Hila Peleg, Sharon Shoham, Eran Yahav
D^3 : Data-Driven Disjunctive Abstraction. VMCAI (2016)
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. CAV (1) (2016)
Yael Meller, Orna Grumberg, Sharon Shoham
A framework for compositional verification of multi-valued systems via abstraction-refinement. Inf. Comput. 247 (2016)
Arie Gurfinkel, Sharon Shoham, Yuri Meshman
SMT-based verification of parameterized systems. SIGSOFT FSE (2016)
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
Ivy: safety verification by interactive generalization. PLDI (2016)
Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham
Some Complexity Results for Stateful Network Verification. TACAS (2016)
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
Automated Circular Assume-Guarantee Reasoning. FM (2015)
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
Decentralizing SDN Policies. POPL (2015)
Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
Property-Directed Inference of Universal Invariants or Proving Their Absence. CAV (1) (2015)
Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang
Symbolic Automata for Static Specification Mining. SAS (2013)
Yakir Vizel, Orna Grumberg, Sharon Shoham
Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS (2013)
Sharon Shoham, Orna Grumberg
Multi-valued model checking games. J. Comput. Syst. Sci. 78 (2) (2012)
Yakir Vizel, Orna Grumberg, Sharon Shoham
Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD (2012)
Alon Mishne, Sharon Shoham, Eran Yahav
Typestate-based semantic code search over partial programs. OOPSLA (2012)

Sharon Shoham.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Sharon Shoham