Shachar Itzhaky

Most-cited papers

VeriCon: towards verifying controller programs in software-defined networks
T. Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky +4 more
2014ACM-SIGPLAN Symposium on Programming Language Design and Implementation200 citations
Semantic Scholar
Verified lifting of stencil computations
S. Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama
2016ACM-SIGPLAN Symposium on Programming Language Design and Implementation100 citations Open access
Semantic Scholar
Property-Directed Inference of Universal Invariants or Proving Their Absence
Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, N. Rinetzky +1 more
2015International Conference on Computer Aided Verification79 citations Open access
Semantic Scholar
A simple inductive synthesis methodology and its applications
Shachar Itzhaky, Sumit Gulwani, N. Immerman, M. Sagiv
2010Conference on Object-Oriented Programming Systems, Languages, and Applications65 citations
Semantic Scholar
Effectively-Propositional Reasoning about Reachability in Linked Data Structures
Shachar Itzhaky, A. Banerjee, N. Immerman, Aleksandar Nanevski +1 more
2013International Conference on Computer Aided Verification61 citations Open access
Semantic Scholar
Property-Directed Shape Analysis
Shachar Itzhaky, Nikolaj S. Bjørner, T. Reps, S. Sagiv +1 more
2014International Conference on Computer Aided Verification43 citations Open access
Semantic Scholar
Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations
Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov +3 more
2016Conference on Object-Oriented Programming Systems, Languages, and Applications37 citations Open access
Semantic Scholar
Modular reasoning about heap paths via effectively propositional formulas
Shachar Itzhaky, A. Banerjee, N. Immerman, O. Lahav +2 more
2014ACM-SIGACT Symposium on Principles of Programming Languages34 citations Open access
Semantic Scholar
Cyclic program synthesis
Shachar Itzhaky, Hila Peleg, N. Polikarpova, R. Rowe +1 more
2021ACM-SIGPLAN Symposium on Programming Language Design and Implementation33 citations Open access
Semantic Scholar
Liquid information flow control
N. Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky +2 more
2016Proc. ACM Program. Lang.27 citations Open access
Semantic Scholar
Theory Exploration Powered By Deductive Synthesis
Eytan Singher, Shachar Itzhaky
2020International Conference on Computer Aided Verification24 citations Open access
Semantic Scholar
On the automated verification of web applications with embedded SQL
Shachar Itzhaky, T. Kotek, N. Rinetzky, S. Sagiv +3 more
2016International Conference on Database Theory22 citations
Semantic Scholar
Programming with a read-eval-synth loop
Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav
2020Proc. ACM Program. Lang.20 citations Open access
Semantic Scholar
Verifying Equivalence of Spark Programs
Shelly Grossman, Sara Cohen, Shachar Itzhaky, N. Rinetzky +1 more
2017International Conference on Computer Aided Verification20 citations
Semantic Scholar
Object spreadsheets: a new computational model for end-user development of data-centric web applications
Matt McCutchen, Shachar Itzhaky, D. Jackson
2016SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software20 citations Open access
Semantic Scholar
Computing summaries of string loops in C for better testing and refactoring
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, N. Rinetzky +1 more
2019ACM-SIGPLAN Symposium on Programming Language Design and Implementation18 citations
Semantic Scholar
Leveraging Rust Types for Program Synthesis
Jonáš Fiala, Shachar Itzhaky, P. Müller, N. Polikarpova +1 more
2023Proc. ACM Program. Lang.17 citations Open access
Semantic Scholar
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning
Shachar Itzhaky, Sumit Gulwani, N. Immerman, S. Sagiv
2013Logic Programming and Automated Reasoning17 citations
Semantic Scholar
AmiGo: Computational Design of Amigurumi Crochet Patterns
M. Edelstein, Hila Peleg, Shachar Itzhaky, M. Ben-Chen
2022Symposium on Computational Fabrication16 citations Open access
Semantic Scholar
A bounded symbolic-size model for symbolic execution
David Trabish, Shachar Itzhaky, N. Rinetzky
2021ESEC/SIGSOFT FSE13 citations
Semantic Scholar
Abstraction-Based Interaction Model for Synthesis
Hila Peleg, Shachar Itzhaky, Sharon Shoham
2018International Conference on Verification, Model Checking and Abstract Interpretation12 citations
Semantic Scholar
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
Cole Kurashige, Ru-Yi Ji, Aditya Giridharan, Mark Barbone +4 more
2024Proc. ACM Program. Lang.11 citations Open access
Semantic Scholar
Type-Driven Repair for Information Flow Security
N. Polikarpova, Jean Yang, Shachar Itzhaky, Armando Solar-Lezama
2016arXiv.org11 citations
Semantic Scholar
SMT Sampling via Model-Guided Approximation
Matan Peled, Bat-Chen Rothenberg, Shachar Itzhaky
2022World Congress on Formal Methods10 citations Open access
Semantic Scholar
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
Oren Ish-Shalom, Shachar Itzhaky, N. Rinetzky, Sharon Shoham
2020International Conference on Verification, Model Checking and Abstract Interpretation10 citations
Semantic Scholar
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham, Y. Vizel
2023European Symposium on Programming8 citations Open access
Semantic Scholar
Colored E-Graph: Equality Reasoning with Conditions
Eytan Singher, Shachar Itzhaky
2023arXiv.org7 citations Open access
Semantic Scholar
Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions
Eytan Singher, Shachar Itzhaky
2024Formal Methods in Computer-Aided Design6 citations
Semantic Scholar
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper)
Shachar Itzhaky, Hila Peleg, N. Polikarpova, R. Rowe +1 more
2021International Conference on Computer Aided Verification6 citations Open access
Semantic Scholar
Enforcing Information Flow Policies with Type-Targeted Program Synthesis
N. Polikarpova, Jean Yang, Shachar Itzhaky, Travis Hance +1 more
20166 citations
Semantic Scholar
Address-Aware Query Caching for Symbolic Execution
David Trabish, Shachar Itzhaky, N. Rinetzky
2021International Conference on Information Control Systems & Technologies5 citations
Semantic Scholar
Securing Access to Untrusted Services From TEEs with GateKeeper
Meni Orenbach, Barak Raveh, Alon Berkenstadt, Yan Michalevsky +2 more
2022arXiv.org3 citations Open access
Semantic Scholar
Automatic reasoning for pointer programs using decidable logics / Itzhaky Shachar
Shachar Itzhaky
20143 citations
Semantic Scholar
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
David Trabish, Shachar Itzhaky
2026Certified Programs and Proofs2 citations
Semantic Scholar
Dynamic Robustness Verification against Weak Memory
R. Margalit, Michalis Kokologiannakis, Shachar Itzhaky, O. Lahav
2025Proc. ACM Program. Lang.2 citations Open access
Semantic Scholar
Run-time Complexity Bounds Using Squeezers
Oren Ish-Shalom, Shachar Itzhaky, N. Rinetzky, Sharon Shoham
2021European Symposium on Programming2 citations Open access
Semantic Scholar
Programming by predicates: a formal model for interactive synthesis
Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav
2019Acta Informatica2 citations
Semantic Scholar
Initial report on Object Spreadsheets
Richard Matthew McCutchen, Shachar Itzhaky, D. Jackson
20162 citations
Semantic Scholar
Kotlin's Type System is (Also) Unsound
Elad Kinsbruner, Hila Peleg, Shachar Itzhaky
2024arXiv.org1 citations
Semantic Scholar
Cypress (PLDI 2021 Artifact): Code and Benchmarks
Shachar Itzhaky, Hila Peleg, N. Polikarpova, R. Rowe +1 more
20211 citations
Semantic Scholar
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
Oren Ish-Shalom, Shachar Itzhaky, R. Manevich, N. Rinetzky
2020International Conference on Verification, Model Checking and Abstract Interpretation1 citations
Semantic Scholar
Automatic Abstraction Refinement for Hyperproperties Verification
Malak Marrid, Shachar Itzhaky, Sharon Shoham, Y. Vizel
2026International Joint Conference on Automated Reasoning0 citations Open access
Semantic Scholar
Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis
Adi Harif, Shachar Itzhaky
2025Sensors Applications Symposium0 citations
Semantic Scholar
Constrictor: Immutability as a Design Concept (Artifact)
Elad Kinsbruner, Shachar Itzhaky, Hila Peleg
2024Dagstuhl Artifacts Ser.0 citations
Semantic Scholar
Scalable Spreadsheet-Driven End-User Applications with Incremental Computation
Sean Hadar, Shachar Itzhaky
2023SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software0 citations Open access
Semantic Scholar
Replication package for article: Liquid Information Flow Types
N. Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky +2 more
2020Artifact Digital Object Group0 citations
Semantic Scholar
Programming by Predicates A formal model for interactive synthesis
Hila Peleg, Shachar Itzhaky, Sharon, Shoham +1 more
20190 citations
Semantic Scholar
Replication Package for Cumputing Summaries of String Loops
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, N. Rinetzky +1 more
2019Artifact Digital Object Group0 citations
Semantic Scholar
Verifying Equivalence of Spark Programs Technical Report 1-Nov-2016
Shelly Grossman, Sara Cohen, Shachar Itzhaky, N. Rinetzky +1 more
20160 citations
Semantic Scholar
MIT Open Access Articles Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations
Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov +2 more
0 citations
Semantic Scholar