Travelled to:1 × Austria
1 × Russia
1 × United Kingdom
3 × USA
Collaborated with:M.Sagiv N.Immerman N.Bjørner N.Rinetzky A.Solar-Lezama A.Banerjee A.Nanevski Matt McCutchen D.J.0001 A.Karbyshev S.Gulwani S.Kamil A.Cheung N.Rinetzky S.Shoham T.W.Reps A.V.Thakur S.Grossman S.Cohen T.Kapus Oren Ish-Shalom C.Cadar O.Lahav Rohit Singh 0002 K.Yessenov Yongquan Lu C.E.Leiserson R.A.Chowdhury T.Ball A.Gember M.Schapira A.Valadarsky
Talks about:program (3) verifi (3) comput (3) proposit (2) properti (2) reason (2) effect (2) direct (2) applic (2) about (2)
Person: Shachar Itzhaky
DBLP: Itzhaky:Shachar
Contributed to:
20152014
2014
20142013
20102017
2016201620162019Wrote 11 papers:
- CAV-2015-KarbyshevBIRS #invariant #proving
- Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.
- CAV-2014-ItzhakyBRST #analysis
- Property-Directed Shape Analysis (SI, NB, TWR, MS, AVT), pp. 35–51.
- PLDI-2014-BallBGIKSSV #named #network #source code #towards #verification
- VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
- POPL-2014-ItzhakyBILNS #composition #effectiveness #reasoning
- Modular reasoning about heap paths via effectively propositional formulas (SI, AB, NI, OL, AN, MS), pp. 385–396.
- CAV-2013-ItzhakyBINS #data type #effectiveness #linked data #open data #reachability #reasoning
- Effectively-Propositional Reasoning about Reachability in Linked Data Structures (SI, AB, NI, AN, MS), pp. 756–772.
- OOPSLA-2010-ItzhakyGIS #induction #synthesis
- A simple inductive synthesis methodology and its applications (SI, SG, NI, MS), pp. 36–46.
- CAV-2017-GrossmanCIRS #equivalence #source code #verification
- Verifying Equivalence of Spark Programs (SG, SC, SI, NR, MS), pp. 282–300.
- Onward-2016-McCutchenIJ #development #spreadsheet #web
- Object spreadsheets: a new computational model for end-user development of data-centric web applications (MM, SI, DJ0), pp. 112–127.
- OOPSLA-2016-Itzhaky0SYLLC #algorithm #divide and conquer #programming #using
- Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations (SI, RS0, ASL, KY, YL, CEL, RAC), pp. 145–164.
- PLDI-2016-KamilCIS
- Verified lifting of stencil computations (SK, AC, SI, ASL), pp. 711–726.
- PLDI-2019-KapusIIRC #c #refactoring #string #summary #testing
- Computing summaries of string loops in C for better testing and refactoring (TK, OIS, SI, NR, CC), pp. 874–888.