Sharon Shoham

According to our database, Sharon Shoham authored at least 80 papers between 2004 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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., January, 2024

Speculative SAT Modulo SAT.

Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Hyperproperty Verification as CHC Satisfiability.

Shachar Itzhaky, Sharon Shoham, Yakir Vizel

Proceedings of the Programming Languages and Systems, 2024

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., October, 2023

State Merging with Quantifiers in Symbolic Execution.

David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma

Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023

From Concept Learning to SAT-Based Invariant Inference (Invited Talk).

Sharon Shoham

Proceedings of the 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2023

Fast Approximations of Quantifier Elimination.

Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Runtime Complexity Bounds Using Squeezers.

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham

ACM Trans. Program. Lang. Syst., 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

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

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.

Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Invariant Inference with Provable Complexity from the Monotone Theory.

Yotam M. Y. Feldman, Sharon Shoham

Proceedings of the Static Analysis - 29th International Symposium, 2022

SAT-Based Invariant Inference and Its Relation to Concept Learning.

Yotam M. Y. Feldman, Sharon Shoham

Proceedings of the Reachability Problems - 16th International Conference, 2022

2021

Learning the boundary of inductive invariants.

Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox

Proc. ACM Program. Lang., 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

Cost-effective capacity provisioning in wide area networks with Shoofly.

Rachee Singh, Nikolaj S. Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette

Proceedings of the ACM SIGCOMM 2021 Conference, Virtual Event, USA, August 23-27, 2021., 2021

Logical Characterization of Coherent Uninterpreted Programs.

Hari Govind V. K., Sharon Shoham, Arie Gurfinkel

Proceedings of the Formal Methods in Computer Aided Design, 2021

Run-time Complexity Bounds Using Squeezers.

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham

Proceedings of the Programming Languages and Systems, 2021

2020

Proving highly-concurrent traversals correct.

Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham

Proc. ACM Program. Lang., 2020

Complexity and information in invariant inference.

Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 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

Programming by predicates: a formal model for interactive synthesis.

Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav

Acta Informatica, 2020

Solving $\mathrm {LIA} ^\star $ Using Approximations.

Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction.

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Global Guidance for Local Generalization in Model Checking.

Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

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

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

Property Directed Self Composition.

Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Inferring Inductive Invariants from Phase Structures.

Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.

Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

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

Automated circular assume-guarantee reasoning.

Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham

Formal Aspects Comput., 2018

Undecidability of Inferring Linear Integer Invariants.

Sharon Shoham

CoRR, 2018

Order out of Chaos: Proving Linearizability Using Local Views.

Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham

Proceedings of the 32nd International Symposium on Distributed Computing, 2018

Abstraction-Based Interaction Model for Synthesis.

Hila Peleg, Shachar Itzhaky, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Interactive Verification of Distributed Protocols Using Decidable Logic.

Sharon Shoham

Proceedings of the Static Analysis - 25th International Symposium, 2018

Abstract Interpretation of Stateful Networks.

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

Proceedings of the Static Analysis - 25th International Symposium, 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

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Programming not only by example.

Hila Peleg, Sharon Shoham, Eran Yahav

Proceedings of the 40th International Conference on Software Engineering, 2018

Inferring Program Extensions from Traces.

Roman Manevich, Sharon Shoham

Proceedings of the 14th International Conference on Grammatical Inference, 2018

Modular Verification of Concurrent Programs via Sequential Model Checking.

Dan Rasin, Orna Grumberg, Sharon Shoham

Proceedings of the Automated Technology for Verification and Analysis, 2018

Quantifiers on Demand.

Arie Gurfinkel, Sharon Shoham, Yakir Vizel

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

Paxos made EPR: decidable reasoning about distributed protocols.

Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 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

Modular Safety Verification for Stateful Networks.

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

CoRR, 2017

Synthesis of Forgiving Data Extractors.

Adi Omari, Sharon Shoham, Eran Yahav

Proceedings of the Tenth ACM International Conference on Web Search and Data Mining, 2017

IC3 - Flipping the E in ICE.

Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 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

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs.

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

Proceedings of the Static Analysis - 24th International Symposium, 2017

RATCOP: Relational Analysis Tool for Concurrent Programs.

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

Proceedings of the Hardware and Software: Verification and Testing, 2017

Synthesis with Abstract Examples.

Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

A framework for compositional verification of multi-valued systems via abstraction-refinement.

Yael Meller, Orna Grumberg, Sharon Shoham

Inf. Comput., 2016

Symbolic automata for representing big code.

Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang

Acta Informatica, 2016

Property Directed Abstract Interpretation.

Noam Rinetzky, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

D^3 : Data-Driven Disjunctive Abstraction.

Hila Peleg, Sharon Shoham, Eran Yahav

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

SMT-based verification of parameterized systems.

Arie Gurfinkel, Sharon Shoham, Yuri Meshman

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Decidability of inferring inductive invariants.

Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Ivy: safety verification by interactive generalization.

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Lossless Separation of Web Pages into Layout Code and Data.

Adi Omari, Benny Kimelfeld, Eran Yahav, Sharon Shoham

Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016

Cross-supervised synthesis of web-crawlers.

Adi Omari, Sharon Shoham, Eran Yahav

Proceedings of the 38th International Conference on Software Engineering, 2016

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement.

Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Decentralizing SDN Policies.

Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014

SAT-based Model Checking: Interpolation, IC3, and Beyond.

Orna Grumberg, Sharon Shoham, Yakir Vizel

Proceedings of the Software Systems Safety, 2014

2013

Intertwined Forward-Backward Reachability Analysis Using Interpolants.

Yakir Vizel, Orna Grumberg, Sharon Shoham

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Symbolic Automata for Static Specification Mining.

Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang

Proceedings of the Static Analysis - 20th International Symposium, 2013

2012

Multi-valued model checking games.

Sharon Shoham, Orna Grumberg

J. Comput. Syst. Sci., 2012

Typestate-based semantic code search over partial programs.

Alon Mishne, Sharon Shoham, Eran Yahav

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Lazy abstraction and SAT-based reachability in hardware model checking.

Yakir Vizel, Orna Grumberg, Sharon Shoham

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011

Local abstraction-refinement for the <i>μ</i>-calculus.

Harald Fecher, Sharon Shoham

Int. J. Softw. Tools Technol. Transf., 2011

2010

Compositional verification and 3-valued abstractions join forces.

Sharon Shoham, Orna Grumberg

Inf. Comput., 2010

2009

Abstraction-refinement and modularity in μ-calculus model checking.

Sharon Shoham

PhD thesis, 2009

2008

Static Specification Mining Using Automata-Based Abstractions.

Sharon Shoham, Eran Yahav, Stephen J. Fink, Marco Pistoia

IEEE Trans. Software Eng., 2008

Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules.

Sharon Shoham, Nissim Francez

Stud Logica, 2008

3-Valued abstraction: More precision at less cost.

Sharon Shoham, Orna Grumberg

Inf. Comput., 2008

State Focusing: Lazy Abstraction for the Mu-Calculus.

Harald Fecher, Sharon Shoham

Proceedings of the Model Checking Software, 2008

2007

A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.

Sharon Shoham, Orna Grumberg

ACM Trans. Comput. Log., 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

Local Abstraction-Refinement for the mu-Calculus.

Harald Fecher, Sharon Shoham

Proceedings of the Model Checking Software, 2007

2005

<i>Don't Know</i> in the µ-Calculus.

Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham

Proceedings of the Verification, 2005

2004

Monotonic Abstraction-Refinement for CTL.

Sharon Shoham, Orna Grumberg

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004