No photo of Sharon Shoham Buchbinder

View Scopus Profile

Sharon Shoham Buchbinder

Professor

Former affiliation
 https://orcid.org/0000-0002-7226-3526
20032025

Research activity per year

Filter
Conference contribution

Search results

  • 2025

    Proving Cutoff Bounds for Safety Properties in First-Order Logic

    Lotan, R., Frenkel, E. & Shoham, S., 2025, Automated Technology for Verification and Analysis - 22nd International Symposium, Proceedings. Akshay, S., Niemetz, A. & Sankaranarayanan, S. (eds.). Springer Science and Business Media Deutschland GmbH, p. 135-159 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 15054 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • 2024

    Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas

    Frenkel, E., Chajed, T., Padon, O. & Shoham, S., 2024, Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings. Gurfinkel, A. & Ganesh, V. (eds.). Springer Science and Business Media Deutschland GmbH, p. 86-108 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14682 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Hyperproperty-Preserving Register Specifications

    Ben Shimon, Y., Lahav, O. & Shoham, S., 24 Oct 2024, 38th International Symposium on Distributed Computing, DISC 2024. Alistarh, D. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 8. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 319).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Hyperproperty Verification as CHC Satisfiability

    Itzhaky, S., Shoham, S. & Vizel, Y., 2024, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. Weirich, S. (ed.). Springer Science and Business Media Deutschland GmbH, p. 212-241 30 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14577 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    2 Scopus citations

  • mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic

    Wilcox, J. R., Feldman, Y. M. Y., Padon, O. & Shoham, S., 2024, Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings. Gurfinkel, A. & Ganesh, V. (eds.). Springer Science and Business Media Deutschland GmbH, p. 71-85 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14682 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    1 Scopus citations

  • Speculative SAT Modulo SAT

    Hari Govind, V. K., Garcia-Contreras, I., Shoham, S. & Gurfinkel, A., 2024, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings. Finkbeiner, B. & Kovács, L. (eds.). Springer Science and Business Media Deutschland GmbH, p. 43-60 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14570 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
  • 2023

    Fast Approximations of Quantifier Elimination

    Garcia-Contreras, I., Govind, V. K. H., Shoham, S. & Gurfinkel, A., 2023, Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings. Enea, C. & Lal, A. (eds.). Springer Science and Business Media Deutschland GmbH, p. 64-86 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13965 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    3 Scopus citations

  • State Merging with Quantifiers in Symbolic Execution

    Trabish, D., Rinetzky, N., Shoham, S. & Sharma, V., 30 Nov 2023, ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Chandra, S., Blincoe, K. & Tonella, P. (eds.). Association for Computing Machinery, Inc, p. 1140-1152 13 p. (ESEC/FSE 2023 - Proceedings of the 31st ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
  • 2022

    Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

    Koenig, J. R., Padon, O., Shoham, S. & Aiken, A., 2022, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Fisman, D. & Rosu, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 338-356 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13243 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    10 Scopus citations

  • Invariant Inference with Provable Complexity from the Monotone Theory

    Feldman, Y. M. Y. & Shoham, S., 2022, Static Analysis - 29th International Symposium, SAS 2022, Proceedings. Singh, G. & Urban, C. (eds.). Springer Science and Business Media Deutschland GmbH, p. 201-226 26 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13790 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

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

    Feldman, Y. M. Y. & Shoham, S., 2022, Reachability Problems - 16th International Conference, RP 2022, Proceedings. Lin, A. W., Lin, A. W., Zetzsche, G. & Potapov, I. (eds.). Springer Science and Business Media Deutschland GmbH, p. 3-27 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13608 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • 2021

    Cost-effective capacity provisioning in wide area networks with Shoofly

    Singh, R., Bjorner, N., Shoham, S., Yin, Y., Arnold, J. & Gaudette, J., 9 Aug 2021, SIGCOMM 2021 - Proceedings of the ACM SIGCOMM 2021 Conference. Association for Computing Machinery, Inc, p. 534-546 13 p. (SIGCOMM 2021 - Proceedings of the ACM SIGCOMM 2021 Conference).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    19 Scopus citations

  • Logical Characterization of Coherent Uninterpreted Programs

    Hari Govind, V. K., Shoham, S. & Gurfinkel, A., 2021, Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021. Piskac, R., Whalen, M. W., Hunt, W. A. & Weissenbacher, G. (eds.). Institute of Electrical and Electronics Engineers Inc., p. 77-85 9 p. (Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

  • Run-time Complexity Bounds Using Squeezers

    Ish-Shalom, O., Itzhaky, S., Rinetzky, N. & Shoham, S., 2021, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings. Yoshida, N. (ed.). Springer Science and Business Media Deutschland GmbH, p. 320-347 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12648 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    1 Scopus citations
  • 2020

    Global Guidance for Local Generalization in Model Checking

    Vediramana Krishnan, H. G., Chen, Y. T., Shoham, S. & Gurfinkel, A., 2020, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lahiri, S. K. & Wang, C. (eds.). Springer, p. 101-125 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12225 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    23 Scopus citations

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

    Ish-Shalom, O., Itzhaky, S., Rinetzky, N. & Shoham, S., 2020, Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. Beyer, D. & Zufferey, D. (eds.). Springer, p. 112-135 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11990 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    7 Scopus citations

  • Solving Using Approximations

    Levatich, M., Bjørner, N., Piskac, R. & Shoham, S., 2020, Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, Proceedings. Beyer, D. & Zufferey, D. (eds.). Springer, p. 360-378 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11990 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    5 Scopus citations
  • 2019

    Inferring inductive invariants from phase structures

    Feldman, Y. M. Y., Wilcox, J. R., Shoham, S. & Sagiv, M., 2019, Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Dillig, I. & Tasiran, S. (eds.). Springer Verlag, p. 405-425 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11562 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    25 Scopus citations

  • Property Directed Self Composition

    Shemer, R., Gurfinkel, A., Shoham, S. & Vizel, Y., 2019, Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Dillig, I. & Tasiran, S. (eds.). Springer Verlag, p. 161-179 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11561 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    32 Scopus citations

  • Verification of threshold-based distributed algorithms by decomposition to decidable logics

    Berkovits, I., Lazić, M., Losa, G., Padon, O. & Shoham, S., 2019, Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Dillig, I. & Tasiran, S. (eds.). Springer Verlag, p. 245-266 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11562 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    28 Scopus citations
  • 2018

    Abstract Interpretation of Stateful Networks

    Alpernas, K., Manevich, R., Panda, A., Sagiv, M., Shenker, S., Shoham, S. & Velner, Y., 2018, Static Analysis - 25th International Symposium, SAS 2018, Proceedings. Podelski, A. (ed.). Springer Verlag, p. 86-106 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11002 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    9 Scopus citations

  • Abstraction-based interaction model for synthesis

    Peleg, H., Itzhaky, S. & Shoham, S., 2018, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Proceedings. Dillig, I. & Palsberg, J. (eds.). Springer Verlag, p. 382-405 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10747 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    5 Scopus citations

  • Interactive Verification of Distributed Protocols Using Decidable Logic

    Shoham, S., 2018, Static Analysis - 25th International Symposium, SAS 2018, Proceedings. Podelski, A. (ed.). Springer Verlag, p. 77-85 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11002 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Modularity for decidability of deductive verification with applications to distributed systems

    Taube, M., Losa, G., McMillan, K. L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J. R. & Woos, D., 11 Jun 2018, PLDI 2018 - Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Foster, J. S., Grossman, D. & Foster, J. S. (eds.). Association for Computing Machinery (ACM), p. 662-677 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    40 Scopus citations

  • Modular Verification of Concurrent Programs via Sequential Model Checking

    Rasin, D., Grumberg, O. & Shoham, S., 2018, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Proceedings. Wang, C. & Lahiri, S. K. (eds.). Springer Verlag, p. 228-247 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11138 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1 Scopus citations

  • Order out of chaos: Proving linearizability using local views

    Feldman, Y. M. Y., Enea, C., Morrison, A., Rinetzky, N. & Shoham, S., 1 Oct 2018, 32nd International Symposium on Distributed Computing, DISC 2018. Schmid, U. & Widder, J. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 23. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 121).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    8 Scopus citations

  • Programming not only by example

    Peleg, H., Shoham, S. & Yahav, E., 27 May 2018, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018. IEEE Computer Society, p. 1114-1124 11 p. (Proceedings - International Conference on Software Engineering).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    24 Scopus citations

  • Quantifiers on Demand

    Gurfinkel, A., Shoham, S. & Vizel, Y., 2018, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Proceedings. Wang, C. & Lahiri, S. K. (eds.). Springer Verlag, p. 248-266 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11138 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    25 Scopus citations

  • Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems

    Padon, O., Hoenicke, J., McMillan, K. L., Podelski, A., Sagiv, M. & Shoham, S., 2 Jul 2018, Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. Bjorner, N. & Gurfinkel, A. (eds.). Institute of Electrical and Electronics Engineers Inc., p. 74-84 11 p. 8603008. (Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    11 Scopus citations
  • 2017

    Bounded quantifier instantiation for checking inductive invariants

    Feldman, Y. M. Y., Padon, O., Immerman, N., Sagiv, M. & Shoham, S., 2017, Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Margaria , T. & Legay, A. (eds.). Springer Verlag, p. 76-95 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10205 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    13 Scopus citations

  • IC3 - Flipping the E in ICE

    Vizel, Y., Gurfinkel, A., Shoham, S. & Malik, S., 2017, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Bouajjani, A. & Monniaux, D. (eds.). Springer Verlag, p. 521-538 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10145 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    6 Scopus citations

  • Property directed reachability for proving absence of concurrent modification errors

    Frumkin, A., Feldman, Y. M. Y., Lhoták, O., Padon, O., Sagiv, M. & Shoham, S., 2017, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Bouajjani, A. & Monniaux, D. (eds.). Springer Verlag, p. 209-227 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10145 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Scopus citations

  • RATCOP: Relational analysis tool for concurrent programs

    Mukherjee, S., Padon, O., Shoham, S., D’Souza, D. & Rinetzky, N., 2017, Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Proceedings. Tzoref-Brill, R. & Strichman, O. (eds.). Springer Verlag, p. 229-233 5 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10629 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Synthesis of forgiving data extractors

    Omari, A., Shoham, S. & Yahav, E., 2 Feb 2017, WSDM 2017 - Proceedings of the 10th ACM International Conference on Web Search and Data Mining. Association for Computing Machinery, Inc, p. 385-394 10 p. (WSDM 2017 - Proceedings of the 10th ACM International Conference on Web Search and Data Mining).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    12 Scopus citations

  • Synthesis with abstract examples

    Drachsler-Cohen, D., Shoham, S. & Yahav, E., 2017, Computer Aided Verification - 29th International Conference, CAV 2017, Proceedings. Kuncak, V. & Majumdar, R. (eds.). Springer Verlag, p. 254-278 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10426 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    16 Scopus citations

  • Thread-local semantics and its efficient sequential abstractions for race-free programs

    Mukherjee, S., Padon, O., Shoham, S., D’Souza, D. & Rinetzky, N., 2017, Static Analysis - 24th International Symposium, SAS 2017, Proceedings. Ranzato, F. (ed.). Springer Verlag, p. 253-276 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10422 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    5 Scopus citations
  • 2016

    Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement

    Elkader, K. A., Grumberg, O., Păsăreanu, C. S. & Shoham, S., 2016, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Farzan, A. & Chaudhuri, S. (eds.). Springer Verlag, p. 329-351 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9779).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    8 Scopus citations

  • Cross-supervised synthesis of web-crawlers

    Omari, A., Shoham, S. & Yahav, E., 14 May 2016, Proceedings - 2016 IEEE/ACM 38th IEEE International Conference on Software Engineering Companion, ICSE 2016. IEEE Computer Society, p. 368-379 12 p. (Proceedings - International Conference on Software Engineering; vol. 14-22-May-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    10 Scopus citations

  • D3: Data-driven disjunctive abstraction

    Peleg, H., Shoham, S. & Yahav, E., 2016, Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Proceedings. Rustan, K., Leino, M. & Jobstmann, B. (eds.). Springer Verlag, p. 185-205 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9583).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    6 Scopus citations

  • Decidability of inferring inductive invariants

    Padon, O., Immerman, N., Shoham, S., Karbyshev, A. & Sagiv, M., 11 Jan 2016, POPL '16 : Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Majumdar, R. & Bodik, R. (eds.). Association for Computing Machinery (ACM), p. 217-231 15 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 20-22-January-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    14 Scopus citations

  • Ivy: Safety verification by interactive generalization

    Padon, O., McMillan, K. L., Panda, A., Sagiv, M. & Shoham, S., 2 Jun 2016, PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. Krintz, C. & Berger, E. (eds.). Association for Computing Machinery (ACM), p. 614-630 17 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); vol. 13-17-June-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    141 Scopus citations

  • Lossless separation of web pages into layout code and data

    Omari, A., Kimelfeld, B., Yahav, E. & Shoham, S., 13 Aug 2016, KDD 2016 - Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. Association for Computing Machinery, p. 1805-1814 10 p. (Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining; vol. 13-17-August-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    7 Scopus citations

  • Property directed abstract interpretation

    Rinetzky, N. & Shoham, S., 2016, Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Proceedings. Rustan, K., Leino, M. & Jobstmann, B. (eds.). Springer Verlag, p. 104-123 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9583).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    2 Scopus citations

  • SMT-Based verification of parameterized systems

    Gurfinkel, A., Shoham, S. & Meshman, Y., 1 Nov 2016, FSE 2016 - Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. Su, Z., Zimmermann, T. & Cleland-Huang, J. (eds.). Association for Computing Machinery, p. 338-348 11 p. (Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering; vol. 13-18-November-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    35 Scopus citations

  • Some complexity results for stateful network verification

    Velner, Y., Alpernas, K., Panda, A., Rabinovich, A., Sagiv, M., Shenker, S. & Shoham, S., 2016, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Raskin, J.-F. & Chechik, M. (eds.). Springer Verlag, p. 811-830 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9636).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    21 Scopus citations
  • 2015

    Automated circular assume-guarantee reasoning

    Elkader, K. A., Grumberg, O., Păsăreanu, C. S. & Shoham, S., 2015, FM 2015: Formal Methods - 20th International Symposium, Proceedings. Bjorner, N. & de Boer, F. (eds.). Springer Verlag, p. 23-39 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9109).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    9 Scopus citations

  • Decentralizing SDN policies

    Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M. & Shoham, S., 14 Jan 2015, POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery (ACM), p. 663-676 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 2015-January).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    22 Scopus citations

  • Property-directed inference of universal invariants or proving their absence

    Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N. & Shoham, S., 2015, Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Pasareanu, C. S., Kroening, D., Pasareanu, C. S. & Kroening, D. (eds.). Springer Verlag, p. 583-602 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9206).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    24 Scopus citations
  • 2013

    Intertwined forward-backward reachability analysis using interpolants

    Vizel, Y., Grumberg, O. & Shoham, S., 2013, Tools and Algorithms for the Construction and Analysis of Systems - 19th Int. Conf., TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.. p. 308-323 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7795 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    17 Scopus citations

  • Symbolic automata for static specification mining

    Peleg, H., Shoham, S., Yahav, E. & Yang, H., 2013, Static Analysis - 20th International Symposium, SAS 2013, Proceedings. p. 63-83 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7935 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    8 Scopus citations