Shachar Itzhaky

51 papers A* 7A 6B 8Journal 20Unranked 9
YearRankTypeTitle / Venue / Authors
2026 B conf
Enhancing Symbolic Execution with Machine-Checked Safety Proofs.
CPP
David Trabish, Shachar Itzhaky
2025 B conf
Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis.
SAS
Adi Harif, Shachar Itzhaky
2025 J jnl
Dynamic Robustness Verification Against Weak Memory (Extended Version).
CoRR
Roy David Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav
2025 J jnl
Dynamic Robustness Verification against Weak Memory.
Proc. ACM Program. Lang.
Roy David Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav
2024 J jnl
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs.
Proc. ACM Program. Lang.
Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova
2024 J jnl
Constrictor: Immutability as a Design Concept (Artifact).
Dagstuhl Artifacts Ser.
Elad Kinsbruner, Shachar Itzhaky, Hila Peleg
2024 A conf
Constrictor: Immutability as a Design Concept.
ECOOP
Elad Kinsbruner, Shachar Itzhaky, Hila Peleg
2024 B conf
Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions.
FMCAD
Eytan Singher, Shachar Itzhaky
2024 — conf
Hyperproperty Verification as CHC Satisfiability.
ESOP (2)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2024 J jnl
Kotlin's Type System is (Also) Unsound.
CoRR
Elad Kinsbruner, Hila Peleg, Shachar Itzhaky
2023 J jnl
Colored E-Graph: Equality Reasoning with Conditions.
CoRR
Eytan Singher, Shachar Itzhaky
2023 J jnl
Hyperproperty Verification as CHC Satisfiability.
CoRR
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2023 J jnl
Leveraging Rust Types for Program Synthesis.
Proc. ACM Program. Lang.
Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey
2023 B conf
SMT Sampling via Model-Guided Approximation.
FM
Matan Peled, Bat-Chen Rothenberg, Shachar Itzhaky
2023 — conf
Scalable Spreadsheet-Driven End-User Applications with Incremental Computation.
Onward!
Sean Hadar, Shachar Itzhaky
2022 — conf
AmiGo: Computational Design of Amigurumi Crochet Patterns.
SCF
Michal Edelstein, Hila Peleg, Shachar Itzhaky, Mirela Ben-Chen
2022 J jnl
AmiGo: Computational Design of Amigurumi Crochet Patterns.
CoRR
Michal Edelstein, Hila Peleg, Shachar Itzhaky, Mirela Ben-Chen
2022 J jnl
Runtime Complexity Bounds Using Squeezers.
ACM Trans. Program. Lang. Syst.
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2022 J jnl
SMT Sampling via Model-Guided Approximation.
CoRR
Matan Peled, Bat-Chen Rothenberg, Shachar Itzhaky
2022 J jnl
Securing Access to Untrusted Services From TEEs with GateKeeper.
CoRR
Meni Orenbach, Bar Raveh, Alon Berkenstadt, Yan Michalevsky, Shachar Itzhaky, Mark Silberstein
2021 — conf
A bounded symbolic-size model for symbolic execution.
ESEC/SIGSOFT FSE
David Trabish, Shachar Itzhaky, Noam Rinetzky
2021 A conf
Address-Aware Query Caching for Symbolic Execution.
ICST
David Trabish, Shachar Itzhaky, Noam Rinetzky
2021 A* conf
Cyclic program synthesis.
PLDI
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
2021 — conf
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper).
CAV (1)
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
2021 J jnl
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction.
CoRR
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2021 A conf
Run-time Complexity Bounds Using Squeezers.
ESOP
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2021 — conf
Theory Exploration Powered by Deductive Synthesis.
CAV (2)
Eytan Singher, Shachar Itzhaky
2020 B conf
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation.
VMCAI
Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich, Noam Rinetzky
2020 J jnl
Liquid information flow control.
Proc. ACM Program. Lang.
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama
2020 J jnl
Programming by predicates: a formal model for interactive synthesis.
Acta Informatica
Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav
2020 J jnl
Programming with a read-eval-synth loop.
Proc. ACM Program. Lang.
Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav
2020 B conf
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction.
VMCAI
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2020 J jnl
Theory Exploration Powered By Deductive Synthesis.
CoRR
Eytan Singher, Shachar Itzhaky
2019 A* conf
Computing summaries of string loops in C for better testing and refactoring.
PLDI
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Cristian Cadar
2018 B conf
Abstraction-Based Interaction Model for Synthesis.
VMCAI
Hila Peleg, Shachar Itzhaky, Sharon Shoham
2017 A conf
On the Automated Verification of Web Applications with Embedded SQL.
ICDT
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2017 J jnl
Property-Directed Inference of Universal Invariants or Proving Their Absence.
J. ACM
Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2017 — conf
Verifying Equivalence of Spark Programs.
CAV (2)
Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv
2016 A conf
Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations.
OOPSLA
Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles E. Leiserson, Rezaul Alam Chowdhury
2016 — conf
Object spreadsheets: a new computational model for end-user development of data-centric web applications.
Onward!
Matt McCutchen, Shachar Itzhaky, Daniel Jackson
2016 J jnl
On the automated verification of web applications with embedded SQL.
CoRR
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2016 J jnl
Type-Driven Repair for Information Flow Security.
CoRR
Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Armando Solar-Lezama
2016 A* conf
Verified lifting of stencil computations.
PLDI
Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama
2015 — conf
Property-Directed Inference of Universal Invariants or Proving Their Absence.
CAV (1)
Aleksandr Karbyshev, Nikolaj S. Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2014 — —
Automatic reasoning for pointer programs using decidable logics / Itzhaky Shachar
Shachar Itzhaky
2014 A* conf
Modular reasoning about heap paths via effectively propositional formulas.
POPL
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
2014 A* conf
Property-Directed Shape Analysis.
CAV
Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur
2014 A* conf
VeriCon: towards verifying controller programs in software-defined networks.
PLDI
Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky
2013 A* conf
Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
CAV
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
2013 B conf
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning.
LPAR
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
2010 A conf
A simple inductive synthesis methodology and its applications.
OOPSLA
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv