default search action
Sharon Shoham
Sharon Shoham Buchbinder
Person information
- affiliation: Tel Aviv University, Israel
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j27]Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham, Arie Gurfinkel:
Global guidance for local generalization in model checking. Formal Methods Syst. Des. 63(1): 81-109 (2024) - [j26]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): 970-1000 (2024) - [c63]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: 71-85 - [c62]Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham:
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. CAV (2) 2024: 86-108 - [c61]Shachar Itzhaky, Sharon Shoham, Yakir Vizel:
Hyperproperty Verification as CHC Satisfiability. ESOP (2) 2024: 212-241 - [c60]Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel:
Speculative SAT Modulo SAT. TACAS (1) 2024: 43-60 - [c59]Yoav Ben Shimon, Ori Lahav, Sharon Shoham:
Hyperproperty-Preserving Register Specifications. DISC 2024: 8:1-8:19 - [i32]Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham:
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. CoRR abs/2405.10308 (2024) - [i31]Raz Lotan, Eden Frenkel, Sharon Shoham:
Proving Cutoff Bounds for Safety Properties in First-Order Logic. CoRR abs/2408.10685 (2024) - [i30]Yoav Ben Shimon, Ori Lahav, Sharon Shoham:
Hyperproperty-Preserving Register Specifications (Extended Version). CoRR abs/2408.11015 (2024) - [i29]Neta Elad, Sharon Shoham:
Axe 'Em: Eliminating Spurious States with Induction Axioms. CoRR abs/2410.18671 (2024) - 2023
- [j25]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): 1878-1904 (2023) - [c58]Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Fast Approximations of Quantifier Elimination. CAV (2) 2023: 64-86 - [c57]Sharon Shoham:
From Concept Learning to SAT-Based Invariant Inference (Invited Talk). FSTTCS 2023: 4:1-4:1 - [c56]David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma:
State Merging with Quantifiers in Symbolic Execution. ESEC/SIGSOFT FSE 2023: 1140-1152 - [i28]Shachar Itzhaky, Sharon Shoham, Yakir Vizel:
Hyperproperty Verification as CHC Satisfiability. CoRR abs/2304.12588 (2023) - [i27]Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Fast Approximations of Quantifier Elimination. CoRR abs/2306.10009 (2023) - [i26]Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel:
Speculative SAT Modulo SAT. CoRR abs/2306.17765 (2023) - [i25]David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma:
State Merging with Quantifiers in Symbolic Execution. CoRR abs/2308.12068 (2023) - [i24]Neta Elad, Oded Padon, Sharon Shoham:
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. CoRR abs/2310.16762 (2023) - 2022
- [j24]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): 1-31 (2022) - [j23]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): 1-29 (2022) - [j22]Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Runtime Complexity Bounds Using Squeezers. ACM Trans. Program. Lang. Syst. 44(3): 17:1-17:36 (2022) - [c55]Yotam M. Y. Feldman, Sharon Shoham:
SAT-Based Invariant Inference and Its Relation to Concept Learning. RP 2022: 3-27 - [c54]Yotam M. Y. Feldman, Sharon Shoham:
Invariant Inference with Provable Complexity from the Monotone Theory. SAS 2022: 201-226 - [c53]Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken:
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. TACAS (1) 2022: 338-356 - [e3]Sharon Shoham, Yakir Vizel:
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science 13371, Springer 2022, ISBN 978-3-031-13184-4 [contents] - [e2]Sharon Shoham, Yakir Vizel:
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science 13372, Springer 2022, ISBN 978-3-031-13187-5 [contents] - [i23]Yotam M. Y. Feldman, Sharon Shoham:
Invariant Inference With Provable Complexity From the Monotone Theory. CoRR abs/2208.07451 (2022) - 2021
- [j21]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): 246-269 (2021) - [j20]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Learning the boundary of inductive invariants. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [c52]Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Run-time Complexity Bounds Using Squeezers. ESOP 2021: 320-347 - [c51]Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Logical Characterization of Coherent Uninterpreted Programs. FMCAD 2021: 77-85 - [c50]Rachee Singh, Nikolaj S. Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette:
Cost-effective capacity provisioning in wide area networks with Shoofly. SIGCOMM 2021: 534-546 - [e1]Fritz Henglein, Sharon Shoham, Yakir Vizel:
Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings. Lecture Notes in Computer Science 12597, Springer 2021, ISBN 978-3-030-67066-5 [contents] - [i22]Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Quantifiers on Demand. CoRR abs/2106.00664 (2021) - [i21]Dan Rasin, Orna Grumberg, Sharon Shoham:
Modular Verification of Concurrent Programs via Sequential Model Checking. CoRR abs/2106.00732 (2021) - [i20]Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. CoRR abs/2106.00937 (2021) - [i19]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR abs/2106.00966 (2021) - [i18]Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Some Complexity Results for Stateful Network Verification. CoRR abs/2106.01030 (2021) - [i17]Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Logical Characterization of Coherent Uninterpreted Programs. CoRR abs/2107.12902 (2021) - [i16]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR abs/2111.00324 (2021) - [i15]Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken:
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. CoRR abs/2112.05304 (2021) - 2020
- [j19]Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav:
Programming by predicates: a formal model for interactive synthesis. Acta Informatica 57(1-2): 165-193 (2020) - [j18]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): 128:1-128:29 (2020) - [j17]Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Complexity and information in invariant inference. Proc. ACM Program. Lang. 4(POPL): 5:1-5:29 (2020) - [c49]Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel:
Global Guidance for Local Generalization in Model Checking. CAV (2) 2020: 101-125 - [c48]Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. VMCAI 2020: 112-135 - [c47]Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham:
Solving $\mathrm {LIA} ^\star $ Using Approximations. VMCAI 2020: 360-378 - [i14]Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel:
Global Guidance for Local Generalization in Model Checking. CoRR abs/2005.13301 (2020) - [i13]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Learning the Boundary of Inductive Invariants. CoRR abs/2008.09909 (2020) - [i12]Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky:
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs. CoRR abs/2009.02775 (2020) - [i11]Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham:
Proving Highly-Concurrent Traversals Correct. CoRR abs/2010.00911 (2020)
2010 – 2019
- 2019
- [j16]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): 191-231 (2019) - [j15]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) - [c46]Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Property Directed Self Composition. CAV (1) 2019: 161-179 - [c45]Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham:
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. CAV (2) 2019: 245-266 - [c44]Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv:
Inferring Inductive Invariants from Phase Structures. CAV (2) 2019: 405-425 - [i10]Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Property Directed Self Composition. CoRR abs/1905.07705 (2019) - [i9]Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv:
Inferring Inductive Invariants from Phase Structures. CoRR abs/1905.07739 (2019) - [i8]Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham:
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. CoRR abs/1905.07805 (2019) - [i7]Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Complexity and Information in Invariant Inference. CoRR abs/1910.12256 (2019) - 2018
- [j14]Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham:
Automated circular assume-guarantee reasoning. Formal Aspects Comput. 30(5): 571-595 (2018) - [j13]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): 26:1-26:33 (2018) - [c43]Dan Rasin, Orna Grumberg, Sharon Shoham:
Modular Verification of Concurrent Programs via Sequential Model Checking. ATVA 2018: 228-247 - [c42]Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Quantifiers on Demand. ATVA 2018: 248-266 - [c41]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: 1-11 - [c40]Roman Manevich, Sharon Shoham:
Inferring Program Extensions from Traces. ICGI 2018: 139-154 - [c39]Hila Peleg, Sharon Shoham, Eran Yahav:
Programming not only by example. ICSE 2018: 1114-1124 - [c38]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: 662-677 - [c37]Sharon Shoham:
Interactive Verification of Distributed Protocols Using Decidable Logic. SAS 2018: 77-85 - [c36]Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Abstract Interpretation of Stateful Networks. SAS 2018: 86-106 - [c35]Hila Peleg, Shachar Itzhaky, Sharon Shoham:
Abstraction-Based Interaction Model for Synthesis. VMCAI 2018: 382-405 - [c34]Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham:
Order out of Chaos: Proving Linearizability Using Local Views. DISC 2018: 23:1-23:21 - [i6]Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham:
Order out of Chaos: Proving Linearizability Using Local Views. CoRR abs/1805.03992 (2018) - [i5]Sharon Shoham:
Undecidability of Inferring Linear Integer Invariants. CoRR abs/1812.01069 (2018) - 2017
- [j12]Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64(1): 7:1-7:33 (2017) - [j11]Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham:
Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA): 108:1-108:31 (2017) - [c33]Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav:
Synthesis with Abstract Examples. CAV (1) 2017: 254-278 - [c32]Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky:
RATCOP: Relational Analysis Tool for Concurrent Programs. Haifa Verification Conference 2017: 229-233 - [c31]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: 253-276 - [c30]Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Bounded Quantifier Instantiation for Checking Inductive Invariants. TACAS (1) 2017: 76-95 - [c29]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: 209-227 - [c28]Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik:
IC3 - Flipping the E in ICE. VMCAI 2017: 521-538 - [c27]Adi Omari, Sharon Shoham, Eran Yahav:
Synthesis of Forgiving Data Extractors. WSDM 2017: 385-394 - [i4]Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Modular Safety Verification for Stateful Networks. CoRR abs/1708.05904 (2017) - [i3]Hila Peleg, Sharon Shoham, Eran Yahav:
Programming Not Only by Example. CoRR abs/1710.01291 (2017) - [i2]Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham:
Paxos Made EPR: Decidable Reasoning about Distributed Protocols. CoRR abs/1710.07191 (2017) - [i1]Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Bounded Quantifier Instantiation for Checking Inductive Invariants. CoRR abs/1710.08668 (2017) - 2016
- [j10]Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang:
Symbolic automata for representing big code. Acta Informatica 53(4): 327-356 (2016) - [j9]Yael Meller, Orna Grumberg, Sharon Shoham:
A framework for compositional verification of multi-valued systems via abstraction-refinement. Inf. Comput. 247: 169-202 (2016) - [c26]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: 329-351 - [c25]Adi Omari, Sharon Shoham, Eran Yahav:
Cross-supervised synthesis of web-crawlers. ICSE 2016: 368-379 - [c24]Adi Omari, Benny Kimelfeld, Eran Yahav, Sharon Shoham:
Lossless Separation of Web Pages into Layout Code and Data. KDD 2016: 1805-1814 - [c23]Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham:
Ivy: safety verification by interactive generalization. PLDI 2016: 614-630 - [c22]Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv:
Decidability of inferring inductive invariants. POPL 2016: 217-231 - [c21]Arie Gurfinkel, Sharon Shoham, Yuri Meshman:
SMT-based verification of parameterized systems. SIGSOFT FSE 2016: 338-348 - [c20]Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham:
Some Complexity Results for Stateful Network Verification. TACAS 2016: 811-830 - [c19]Noam Rinetzky, Sharon Shoham:
Property Directed Abstract Interpretation. VMCAI 2016: 104-123 - [c18]Hila Peleg, Sharon Shoham, Eran Yahav:
D^3 : Data-Driven Disjunctive Abstraction. VMCAI 2016: 185-205 - 2015
- [c17]Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham:
Property-Directed Inference of Universal Invariants or Proving Their Absence. CAV (1) 2015: 583-602 - [c16]Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham:
Automated Circular Assume-Guarantee Reasoning. FM 2015: 23-39 - [c15]Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham:
Decentralizing SDN Policies. POPL 2015: 663-676 - 2014
- [p1]Orna Grumberg, Sharon Shoham, Yakir Vizel:
SAT-based Model Checking: Interpolation, IC3, and Beyond. Software Systems Safety 2014: 17-41 - 2013
- [c14]Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang:
Symbolic Automata for Static Specification Mining. SAS 2013: 63-83 - [c13]Yakir Vizel, Orna Grumberg, Sharon Shoham:
Intertwined Forward-Backward Reachability Analysis Using Interpolants. TACAS 2013: 308-323 - 2012
- [j8]Sharon Shoham, Orna Grumberg:
Multi-valued model checking games. J. Comput. Syst. Sci. 78(2): 414-429 (2012) - [c12]Yakir Vizel, Orna Grumberg, Sharon Shoham:
Lazy abstraction and SAT-based reachability in hardware model checking. FMCAD 2012: 173-181 - [c11]Alon Mishne, Sharon Shoham, Eran Yahav:
Typestate-based semantic code search over partial programs. OOPSLA 2012: 997-1016 - 2011
- [j7]Harald Fecher, Sharon Shoham:
Local abstraction-refinement for the μ-calculus. Int. J. Softw. Tools Technol. Transf. 13(4): 289-306 (2011) - 2010
- [j6]Sharon Shoham, Orna Grumberg:
Compositional verification and 3-valued abstractions join forces. Inf. Comput. 208(2): 178-202 (2010)
2000 – 2009
- 2009
- [b1]Sharon Shoham:
Abstraction-refinement and modularity in μ-calculus model checking. Technion - Israel Institute of Technology, Israel, 2009 - [c10]Yael Meller, Orna Grumberg, Sharon Shoham:
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. ATVA 2009: 271-288 - 2008
- [j5]Sharon Shoham, Orna Grumberg:
3-Valued abstraction: More precision at less cost. Inf. Comput. 206(11): 1313-1333 (2008) - [j4]Sharon Shoham, Nissim Francez:
Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules. Stud Logica 90(2): 161-188 (2008) - [j3]Sharon Shoham, Eran Yahav, Stephen J. Fink, Marco Pistoia:
Static Specification Mining Using Automata-Based Abstractions. IEEE Trans. Software Eng. 34(5): 651-666 (2008) - [c9]Harald Fecher, Sharon Shoham:
State Focusing: Lazy Abstraction for the Mu-Calculus. SPIN 2008: 95-113 - 2007
- [j2]