@inproceedings{HVC:MPSDR17,
Author=  {Suvam Mukherjee and Oded Padon and Sharon Shoham and Deepak D’Souza and Noam Rinetzky},
Title="RATCOP: Relational Analysis Tool for Concurrent Programs",
booktitle="13th Haifa Verification Conference (HVC)",
YEAR = 2017,
}

@inproceedings{SAS:MPSDR17,
Author=  {Suvam Mukherjee and Oded Padon and Sharon Shoham and Deepak D’Souza and Noam Rinetzky},
Title="Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs",
booktitle="22nd International Static Analysis Symposium (SAS)",
YEAR = 2017,
}

@article{JACM17,
 author = {Karbyshev, Aleksandr and Bj{\o}rner, Nikolaj and Itzhaky, Shachar and Rinetzky, Noam and Shoham, Sharon},
 title = {Property-Directed Inference of Universal Invariants or Proving Their Absence},
 journal = {J. ACM},
 issue_date = {March 2017},
 volume = {64},
 number = {1},
 month = mar,
 year = {2017},
 issn = {0004-5411},
 pages = {7:1--7:33},
 articleno = {7},
 numpages = {33},
 url = {http://doi.acm.org/10.1145/3022187},
 doi = {10.1145/3022187},
 acmid = {3022187},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {EPR, IC3, PDR, Universal invariants, property-directed reachability},
} 

@inproceedings{CAV17,
	author = {Shelly Grossman and Sara Cohen and  Shachar Itzhaky and Noam Rinetzky and  Mooly Sagiv},
	title = {Verifying Equivalence of Spark Programs},
	booktitle = {Conference on Computer Aided Verification (CAV)},
	year = {2017},
} 

@inproceedings{ICDT17,
	author = {Shachar Itzhaky and Tomer Kotek and Noam Rinetzky and Mooly Sagiv and Orr Tamir and Helmut Veith and Florian Zuleger},
	title = {On the automated verification of web applications with embedded SQL},
	booktitle = {International Conference on Database Theory  (ICDT)},
	year = {2017},
} 

@inproceedings{VMCAI:OPRS17,
	author = {Or Ozeri and Oded Padon and Noam Rinetzky  and Mooly Sagiv},
	title = {Conjunctive Abstract Interpretation using Paramodulation},
	booktitle = {International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
	year = {2017},
} 

@inproceedings{CAV:MDR16,
	author = {Roman Manevich and Boris Dogadov  and Noam Rinetzky,
	title = {From Shape Analysis to Termination Analysis in Linear Time},
	booktitle = {Conference on Computer Aided Verification (CAV)},
	year = {2016},
} 

@inproceedings{VMCAI:RS16,
	author = {Noam Rinetzky and Sharon Shoham},
	title = {Property Directed Abstract Interpretation},
	booktitle = {International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
	year = {2016},
} 

@inproceedings{OPODIS:TMR15,
	author = {Orr Tamir and Adam Morrison and Noam Rinetzky},
	title = {A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms},
	booktitle = {International Conference on Principles of Distributed Systems (OPODIS)},
	year = {2015},
} 

@inproceedings{DISC:HRV15,
	author = {Nir Hemed and Noam Rinetzky and Viktor Vafeiadis},
	title = {Modular Verification of Concurrency-Aware Linearizability},
	booktitle = {International Symposium on Distributed Computing (DISC)},
	year = {2015},
} 

@inproceedings{SAS:CNRSY15,
Author=  {Ghila Castelnuovo and Mayur Naik and Noam Rinetzky and Mooly Sagiv and Hongseok Yang},
Title="Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis",
booktitle="12th International Static Analysis Symposium (SAS)",
YEAR = 2015,
}

@inproceedings{CAV:KBIRS15,
	author = {Alexander Karbyshev and Nikolaj Bjorner and Shachar Itzhaky and Noam Rinetzky and Sharon Shoham},
	title = {Property-Directed Inference of Universal Invariants or Proving Their Absence},
	booktitle = {International Conference on Computer Aided Verification (CAV)},
	year = {2015},
} 

@inproceedings{DISC:AGHR14,
	author = {Hagit Attiya and Alexey Gotsman and Sandeep Hans and Noam Rinetzky},
	title = {Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient},
	booktitle = {ACM International Symposium on Distributed Computing (DISC)},
	year = {2014},
} 

@inproceedings{PODC:HR14,
	author = {Nir Hemed and Noam Rinetzky},
	title = {Brief Announcement: Concurrency-Aware Linearizability},
	booktitle = {ACM Symposium on Principles of Distributed Computing (PODC)},
	year = {2014},
} 

@inproceedings{WTTM:AGHR14,
	author = {Hagit Attiya and Alexey Gotsman and Sandeep Hans and Noam Rinetzky},
	title = {Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient},
	booktitle = {6th Workshop on the Theory of Transactional Memory EuroTM (WTTM)},
	year = {2014},
} 

@inproceedings{FSE:TR13,
	author = {Omer Tripp and Noam Rinetzky},
	title = {Tightfit: Adaptive Parallelization with Foresight},
	booktitle = {ACM Conference on the Foundations of Software Engineering (FSE)},
	year = {2013},
} 

@TechReport{modular-lattice-tr,
	author = {Ghila Castelnuovo and Mayur Naik and Noam Rinetzky and Mooly Sagiv and Hongseok Yang},
	title = {Modular Lattices for Compositional Interprocedural Analysis},
	institution = {School of Computer Science, Tel Aviv University},
	year = 	 2013,
	number = "TR-103/13"
}

@inproceedings{PODC:AGHR13,
	author = {Hagit Attiya and Alexey Gotsman and Sandeep Hans and Noam Rinetzky},
	title = {A Programming Language Perspective on Transactional Memory Consistency},
	booktitle = {ACM Symposium on Principles of Distributed Computing (PODC)},
	year = {2013},
} 

@inproceedings{ESOP:GRY13,
	author = {Alexey Gotsman and Noam Rinetzky and Hongseok Yang},
	title = {Verifying Concurrent Memory Reclamation Algorithms with Grace},
	booktitle = {European Symposium on Programming (ESOP)},
	year = {2013},
} 

@Techreport{TR:GRY13,
	author = {Alexey Gotsman and Noam Rinetzky and Hongseok Yang},
	title = {Verifying Concurrent Memory Reclamation Algorithms with Grace},
	year = {2013},
	INSTITUTION = "Tel Aviv University",
	TYPE = "Tech. Rep.",
	MONTH = jan,
	NUMBER = "7/13",
	YEAR = 2013,
	Note = "Available at ``\textit{http://www.cs.tau.ac.il/$\sim$maon}''"
}

@incollection{
year={2013},
isbn={978-3-642-37650-4},
booktitle={Programming Logics},
volume={7797},
series={Lecture Notes in Computer Science},
editor={Voronkov, Andrei and Weidenbach, Christoph},
doi={10.1007/978-3-642-37651-1_17},
title={Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs},
publisher={Springer Berlin Heidelberg},
author={Kreiker, J. and Reps, T. and Rinetzky, N. and Sagiv, M. and Wilhelm, Reinhard and Yahav, E.},
pages={414-445}
}

@INPROCEEDINGS{LNCS:KRRSWY11,
	Title="Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs",
	Author=  "J. Kreiker and T. Reps and N. Rinetzky and M. Sagiv and R. Wilhelm and E. Yahav",
	booktitle="Special LNCS Issue commemorating Harald Ganzinger",
	YEAR = 2011,
	Note = "(To be published.)"
}

@Techreport{TR:KRRSWY10,
	Title="Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs",
	Author=  "J. Kreiker and T. Reps and N. Rinetzky and M. Sagiv and R. Wilhelm and E. Yahav",
	INSTITUTION = "Queen Mary University of London",
	TYPE = "Tech. Rep.",
	MONTH = may,
	YEAR = 2010,
	Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@INPROCEEDINGS{FSE:LDBRS10,
  Title="Field-Sensitive Program Dependence Analysis",
  Author=  "S. Litvak and N. Dor and  R. Bodik and N. Rinetzky and M. Sagiv",
  booktitle="ACM SIGSOFT 18th International Symposium on the Foundations of Software Engineering (FSE)",
  year = {2010},
  pages = {287--296},
  publisher = {ACM},
}

@INPROCEEDINGS{PODC:ORVYY10,
  Title={Verifying Linearizability with Hindsight},
  Author=  {P. W. O'Hearn and N. Rinetzky and M. T. Vechev and E. Yahav and G. Yorsh},
  booktitle={29th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)},
  YEAR = 2010,
  pages = {85--94}
}

@Techreport{TR:ORVYY10,
Title="Verifying Linearizability with Hindsight",
Author=  "P. W. O'Hearn and N. Rinetzky and M. T. Vechev and E. Yahav and G. Yorsh",
INSTITUTION = "Queen Mary University of London",
TYPE = "Tech. Rep.",
MONTH = feb,
YEAR = 2010,
Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@INPROCEEDINGS{POPL:ARR10,
  Author=  "H. Attiya  and G. Ramalingam and N. Rinetzky",
  Title="Sequential Verification of Serializability",
  booktitle="37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)",
  year = 2010,
  pages = {31--42}
}

@Techreport{TR:ARR09,
Title="Sequential Verification of Serializability",
Author=  "H. Attiya and G. Ramalingam and N. Rinetzky",
INSTITUTION = "Queen Mary University of London",
TYPE = "Tech. Rep.",
MONTH = jul,
YEAR = 2009,
Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@inproceedings{EC2:RVYY09,
author = {N. Rinetzky and M. T. Vechev and E. Yahav and G. Yorsh},
title = {Verifying optimistic algorithms should be easy (position paper)},
booktitle = {Workshop on Exploiting Concurrency Efficiently and Correctly -- (EC)2},
year = {2009}
} 

@inproceedings{FOOL:JRPHSY09,
author = {J. Juhasz and N. Rinetzky and A. Poetzsch-Heffter and M. Sagiv and E. Yahav},
title = {Modular verification with shared abstractions},
booktitle = {International Workshop on Foundations of Object-Oriented Languages (FOOL)},
year = {2009}
} 

@inproceedings{ESOP:FORY09,
author = {Ivana Filipovic and Peter O’Hearn and Noam Rinetzky and Hongseok Yang},
title = {Abstraction for Concurrent Objects},
booktitle = {European Symposium on Programming (ESOP)},
year = {2009},
} 

@article{TCS:FilipovicORY10,
title = "Abstraction for concurrent objects",
journal = "Theoretical Computer Science",
volume = "411",
number = "51-52",
pages = "4379 - 4398",
year = "2010",
note = "European Symposium on Programming 2009 - ESOP 2009",
issn = "0304-3975",
doi = "DOI: 10.1016/j.tcs.2010.09.021",
url = "http://www.sciencedirect.com/science/article/B6V1G-514BPP0-3/2/dab9442b76a4fe5fbd946076b026abb4",
author = "Ivana Filipovic and Peter O'Hearn and Noam Rinetzky and Hongseok Yang",
keywords = "Linearizability",
keywords = "Sequential consistency",
keywords = "Observational equivalence",
keywords = "Observational refinement"
}

@Techreport{TR:FORY10,
author = {Ivana Filipovic and Peter O’Hearn and Noam Rinetzky and Hongseok Yang},
title = {Abstraction for Concurrent Objects},
booktitle = {European Symposium on Programming (ESOP)},
year = {2010},
INSTITUTION = "Queen Mary University of London",
TYPE = "Tech. Rep.",
MONTH = apr,
YEAR = 2010,
Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@article{TOPLAS:RRSY08,
author = {N. Rinetzky and G. Ramalingam and M. Sagiv and E. Yahav},
title = {On the complexity of partially-flow-sensitive alias analysis},
journal = {ACM Trans. Program. Lang. Syst.},
volume = {30},
number = {3},
year = {2008},
issn = {0164-0925},
pages = {13:1--13:28},
doi = {http://doi.acm.org/10.1145/1353445.1353447},
publisher = {ACM},
address = {New York, NY, USA},
}

@inproceedings{ISSTA:LYCFRN08,
	 author = {Alexey Loginov and Eran Yahav and Satish Chandra and Stephen Fink 
	 and Noam Rinetzky and Mangala Nanda},
	 title = {Verifying dereference safety via expanding-scope analysis},
	 booktitle = {ISSTA '08: Proceedings of the 2008 international symposium on 
	 Software testing and analysis},
	 year = {2008},
	 isbn = {978-1-60558-050-0},
	 pages = {213--224},
	 location = {Seattle, WA, USA},
	 doi = {http://doi.acm.org/10.1145/1390630.1390657},
	 publisher = {ACM},
	 address = {New York, NY, USA},
	 }

@inproceedings{APLAS:GBCRS07,
  author    = {Alexey Gotsman and
               Josh Berdine and
               Byron Cook and
               Noam Rinetzky and
               Mooly Sagiv},
  title     = {Local Reasoning for Storable Locks and Threads},
  booktitle = {The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS)},
  year      = {2007},
  pages     = {19-37},
}

@inproceedings{Cav:AmitRRSY07,
  AUTHOR =       {Daphna Amit and Noam Rinetzky and Tom Reps and Mooly Sagiv and Eran Yahav},
  TITLE =        {Comparison under abstraction for verifying linearizability},
  booktitle =  {19th International Conference on Computer Aided Verification (CAV)},
  YEAR =         {2007},
  pages = {477--490}
}

@Techreport{TR:RRSY06,
Title="Componentized Heap Abstractions",
Author=  "N. Rinetzky and G. Ramalingam and  M. Sagiv and E. Yahav",
INSTITUTION = "Tel Aviv University",
TYPE = "Tech. Rep.",
NUMBER = "164",
MONTH = dec,
YEAR = 2006,
Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@inproceedings{PLDI:VYBR07,
 author = {Martin T. Vechev and Eran Yahav and David F. Bacon and Noam Rinetzky},
 title = {CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors},
 booktitle = {Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation (PLDI)},
 year = {2007},
 pages = {456--467},
 location = {San Diego, California, USA},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@INPROCEEDINGS{ESOP:RPHRSY07,
Title="Modular Shape Analysis for Dynamically Encapsulated Programs",
Author=  "N. Rinetzky and A. Poetzsch-Heffter and G. Ramalingam and  M. Sagiv and E. Yahav",
booktitle = "16th European Symposium on Programming (ESOP)",
PAGES = "220--236",
YEAR = 2007
}

@Techreport{SPARKEQTR,
Title="Verifying Equivalence of Spark Programs",
Author=  "Shelly Grossman and Sara Cohen and Shachar Itzhaky and Noam Rinetzky and Mooly Sagiv",
INSTITUTION = "Tel Aviv University",
TYPE = "Tech. Rep.",
MONTH = nov,
YEAR = 2016,
Note = "Available at ``\textit{http://www.cs.tau.ac.il/$\sim$maon/pubs/sparkeq-tr.pdf}''"
}

@Techreport{TR:RPHRSY06,
Title="Modular Shape Analysis for Dynamically Encapsulated Programs",
Author=  "N. Rinetzky and A. Poetzsch-Heffter and G. Ramalingam and  M. Sagiv and E. Yahav",
INSTITUTION = "Tel Aviv University",
TYPE = "Tech. Rep.",
NUMBER = "107",
MONTH = oct,
YEAR = 2006,
Note = "Available at ``\textit{http://www.cs.tau.ac.il/$\sim$maon}''"
}

@INPROCEEDINGS{SAS:RSY05,
Author=  "N. Rinetzky and M. Sagiv and E. Yahav",
Title="Interprocedural Shape Analysis for Cutpoint-Free Programs",
booktitle="12th International Static Analysis Symposium (SAS)"
YEAR = 2005,
pages="284--302"
}

@Techreport{TR:RSY05,
Author=  "N. Rinetzky and M. Sagiv and E. Yahav",
Title="Interprocedural Shape Analysis for Cutpoint-Free Programs",
INSTITUTION = "Tel Aviv Uni.",
TYPE = "Tech. Rep.",
NUMBER = "104/05",
MONTH = apr,
YEAR = 2005,
Note = "Available at ``\textit{http://www.cs.tau.ac.il/$\sim$maon}''"
}

@INPROCEEDINGS{POPL:RBRSW05,
  Author=  "N. Rinetzky and J. Bauer and T. Reps and  M. Sagiv and R. Wilhelm",
  Title="A~Semantics for Procedure Local Heaps and its Abstractions",
  booktitle="32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)",
  year = 2005
}

@Techreport{TR:RBRSW04,
Author=  "N. Rinetzky and J. Bauer and T. Reps and  M. Sagiv and R. Wilhelm",
Title="A~Semantics for Procedure Local Heaps and its Abstractions",
INSTITUTION = "AVACS",
TYPE = "Tech. Rep.",
NUMBER = "1",
MONTH = sep,
YEAR = 2004,
Note = "Available at ``\textit{http://www.avacs.org}''"
}

@Techreport{TR:RSY04,
Author=  "N. Rinetzky and M. Sagiv and E. Yahav",
Title="Interprocedural Functional Shape Analysis using Local Heaps",
INSTITUTION = "Tel Aviv Uni.",
TYPE = "Tech. Rep.",
NUMBER = "26",
MONTH = nov,
YEAR = 2004,
Note = "Available at ``\textit{http://www.dcs.qmul.ac.uk/$\sim$maon}''"
}

@INPROCEEDINGS{VSTTE:DFGLALMRRRSWYY03,
  Author=  "N. Dor, J. Field, D. Gopan, T. Lev-Ami, A. Loginov, R. Manevich, G. Ramalingam, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm, E. Yahav, G. Yorsh",
  Title="Automatic verification of strongly dynamic software systems",
  booktitle="IFIP working conference on verified software: Theories, Tools, Experiments",
  year = 2003
}

@ARTICLE{IBMHRL:mass03,
  author = "A. Azagury and V. Dreizin and M. Factor and E. Henis and D. Naor and N. Rinetzky and O. Rodeh and J. Satran and A. Tavory and L. Yerushalmi",
  title = "Towards an Object Store",
  journal = "20 th IEEE/11 th NASA Goddard Conference on Mass Storage Systems and Technologies (MSS'03)",
  pages = "165--176",
  year = "2003"
}

@ARTICLE{IBMHRL:sisw02,
  author =       "A. Azagury and R. Canetti and M. Factor and S. Halevi and E. Henis and D. Naor and N. Rinetzky and O. Rodeh and J. Satran",
  journal =      "IEEE International Security In Storage Workshop",
  title =        "A Two Layered Approach for Securing an Object Store Network",
  pages =        "10--23",
  year =         "2002"
}

@article{RS:CC01,
    author = "Noam Rinetzky and Mooly Sagiv",
    title = "Interprocedural Shape Analysis for Recursive Programs",
    journal = "Lecture Notes in Computer Science",
    volume = "2027",
    pages = "133--149",
    year = "2001"
}

@PhdThesis{Rinetzky:PhD08,
    title="Interprocedural and Modular Local Heap Shape Analysis",
    Author="Noam Rinetzky",
    School="Tel Aviv University",
    Year=2008,
    month = "June",
}

@MastersThesis{Rinetzky:Master01,
    Author="Noam Rinetzky",
    title="Interprocedural Shape Analysis",
    School="Technion Israel Institute of Technology",
    Year=2001
}