Sharon Shoham Buchbinder - Home Page

 

 

I am a senior lecturer in the School of Computer Science at Tel Aviv University.

My main areas of research are formal verification of systems and program analysis.

 

Contact Information

School of Computer Science,

Schreiber building
Tel Aviv University

E-mail:

sharon.shoham 'at' gmail.com

 

 


Teaching

·         Automatic Verification of Systems, Tel-Aviv University

·         Automatic Verification of Systems, Tel-Aviv Yaffo academic College

·         Seminar on Automatic Verification of Systems, Tel-Aviv Yaffo academic College

·         Computability, Tel-Aviv Yaffo academic College

·         Introduction to Logic and Set Theory, Tel-Aviv Yaffo academic College

·         Computability Theory, Technion (Teaching assistant)

·         Automatic Verification of Programs, Technion (Teaching assistant in charge)

·         Introduction to Software Verification, Technion (Teaching assistant in charge)

·         Logic in Computer Science 1, Technion (Teaching assistant)

·         Automata and Formal Languages, Technion (Teaching assistant in charge)

 


Book Chapter

·         Static Specification Mining Using Automata-Based Abstractions. Eran Yahav, Sharon Shoham, Stephen Fink and Marco Pistoia. Chapter 6 in Book on Mining Software Specifications: Methodologies and Applications. Editors: David Lo, Siau-Cheng Khoo, Chao Liu, and Jiawei Han. Published in Data Mining and Knowledge Discovery Book Series by CRC Press, April 2011.

Conference and Workshop Publications

·         Bounded Quantifier Instantiation for Checking Inductive Invariants. Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham, Accepted for publication in the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2017.

·         IC3 - Flipping the E in ICE. Yakir Vizel, Arie Gurfinkel, Sharon Shoham and Sharad Malik, In proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2017. [pdf]

·         Property Directed Reachability for Proving Absence of Concurrent Modification Errors. Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhotak, Oded Padon, Mooly Sagiv and Sharon Shoham, In proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2017. [pdf]

·         Synthesis of Forgiving Data Extractors. Adi Omari, Sharon Shoham and Eran Yahav, In proceedings of the ACM conference on Web Search and Dada Mining (WSDM) 2017. [pdf]

·         SMT-Based Verification of Parameterized Systems. Arie Gurfinkel, Sharon Shoham and Yuri Meshman, In proceedings of the ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE) 2016. [pdf]

·         Lossless Separation of Web Pages into Layout Code and Data. Adi Omari, Benny Kimelfeld, Sharon Shoham and Eran Yahav, In proceedings of the 22nd ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD), pages 1805-1814, 2016. [pdf]

·         Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham, In proceedings of the 28th International Conference on Computer Aided Verification (CAV), pages 329-351, 2016. [pdf]

·         Ivy: safety verification by interactive generalization. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv and Sharon Shoham, In proceedings of 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), pages 614-630, 2016. [pdf]

·         Cross Supervised Synthesis of Web-Crawlers. Adi Omari, Sharon Shoham and Eran Yahav, In proceedings of the International Conference on Software Engineering (ICSE), pages 368-379, 2016. [pdf]

·         Some Complexity Results for Stateful Network Verification. Yaron Velner, Kalev Aplernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, and Sharon Shoham, In proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 811-830, 2016. [pdf]

·         Property Directed Abstract Interpretation. Noam Rinetzky and Sharon Shoham, In proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 104-123, 2016. [pdf]

·         D3: Data-Driven Disjunctive Abstraction. Hila Peleg, Sharon Shoham, and Eran Yahav, In proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 185-205, 2016. [pdf]

·         Decidability of Inferring Inductive Invariants. Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, and Mooly Sagiv, In proceedings of the 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 217-231, 2016. [pdf]

·         Property-Directed Inference of Universal Invariants or Proving Their Absence. Aleksandr Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham, In proceedings of the 27th International Conference on Computer Aided Verification (CAV), pages 583-602, 2015. [pdf] Invited to Journal of the ACM.

·         Automated Circular Assume-Guarantee Reasoning. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham, In proceedings of the 20th International Symposium on Formal Methods (FM), 2015. [pdf] Invited to special issue in the Formal Aspects of Computing journal.

·         Decentralizing SDN Policies. Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv and Sharon Shoham, In proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2015. [pdf]

·         Symbolic Automata for Static Specification Mining. Hila Peleg, Sharon Shoham, Eran Yahav and Hongseok Yang, In proceedings of the International Static Analysis Symposium (SAS), 2013. [pdf]

·         Intertwined Forward-Backward Reachability Analysis Using Interpolants. Yakir Vizel, Orna Grumberg and Sharon Shoham, In proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2013. [pdf]

·         Lazy Abstraction and SAT-Based Reachability in Hardware Model Checking. Yakir Vizel, Orna Grumberg and Sharon Shoham, In proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2012. [pdf]

·         Typestate-Based Semantic Code Search over Partial Programs. Alon Mishne, Sharon Shoham and Eran Yahav, In proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2012. [pdf]

·         A Framework For Compositional Verification of Multi-Valued Systems Via Abstraction-Refinement. Yael Meller, Orna Grumberg, and Sharon Shoham, In proceedings of the 7th international symposium on Automated Technology for Verification and Analysis (ATVA), 2009. [pdf]

·         State focusing: Lazy abstraction for the mu-calculus. Harald Fecher and Sharon Shoham, In proceedings of the 15th International Workshop on Model Checking Software (SPIN'08), volume 5156 of LNCS, pages 95-113, Los Angeles, USA, August 2008. [pdf]

·         Compositional Verification and 3-Valued Abstractions Join Forces. Sharon Shoham and Orna Grumberg, In proceedings of the 14th International Static Analysis Symposium (SAS'07), volume 4634 of LNCS, pages 69-86, Kongens Lyngby, Denmark, August 2007. [pdf]

·         Static Specification Mining Using Automata-Based Abstractions. Sharon Shoham, Eran Yahav, Stephen Fink and Marco Pistoia, In proceedings of the International Symposium on Software Testing and Analysis (ISSTA'07), pages 174-184, London, United Kingdom, July 2007. Best paper award. [pdf]

·          Local abstraction-refinement for the mu-calculus. Harald Fecher and Sharon Shoham, In proceedings of the 14th International Workshop on Model Checking Software (SPIN'07), volume 4595 of LNCS, pages 4-23, Berlin, Germany, July 2007. [pdf]

·         3-Valued Abstraction: More Precision at Less Cost. Sharon Shoham and Orna Grumberg, In proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pages 399-408, Seattle, Washington, August 2006. [pdf]

·         Multi-Valued Model Checking Games. Sharon Shoham and Orna Grumberg, In proceedings of the third international symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of LNCS, pages 354-369, Taipei, Taiwan, October 2005. [pdf]

·         Don't Know in the mu-Calculus. Orna Grumberg, Martin Lange, Martin Leucker and Sharon Shoham, In proceedings of the 6th international conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of LNCS, pages 233-249, Paris, France, January 2005. [pdf]

·         Monotonic Abstraction-Refinement for CTL. Sharon Shoham and Orna Grumberg, In proceedings of the 10th international conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of LNCS, pages 546-560, Barcelona, Spain, March-April 2004. [pdf]

·         A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. Sharon Shoham and Orna Grumberg, In proceedings of the 15th international conference on Computer Aided Verification (CAV'03), volume 2725 of LNCS, pages 275-287, Boulder, Colorado, July 2003. [pdf]

Journal Publications

·         A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. Yael Meller, Orna Grumberg and Sharon Shoham, Accepted for publication in Information and Computation.

·         Symbolic Automata for Representing Big Code. Hila Peleg, Sharon Shoham, Eran Yahav and and Hongseok Yang, Accepted for publication in special issue of Acta Informatica devoted to COST Action IC0901.

·         Multi-Valued Model Checking Games. Sharon Shoham and Orna Grumberg, Journal of Computer and System Sciences (JCSS), Volume 78, Number 2, Pages 414-429, March 2012. Special issue on Games in Verification.  [pdf]

·         Local abstraction-refinement for the mu-calculus. Harald Fecher and Sharon Shoham, International Journal on Software Tools for Technology Transfer (STTT), Volume 13, Number 4, Pages 289-306, August 2011. Special issue of SPIN'07.  [pdf]

·         Compositional Verification and 3-Valued Abstractions Join Forces. Sharon Shoham and Orna Grumberg, Information and Computation, Volume 208, Number 2, Pages 178-202, February 2010. [pdf]

·         3-Valued Abstraction: More Precision at Less Cost. Sharon Shoham and Orna Grumberg, Information and Computation, Volume 206, Issue 11, Pages 1313-1333, November 2008. [pdf]

·         Game semantics for the Lambek-Calculus: capturing directionality and the absence of structural rules. Sharon Shoham and Nissim Francez, Studia Logica, Volume 90, Number 2, Pages 161-188, November 2008. [pdf]

·         Static Specification Mining Using Automata-Based Abstractions. Sharon Shoham, Eran Yahav, Stephen Fink and Marco Pistoia, IEEE Transactions on Software Engineering (TSE), Volume 34, Issue 5, Pages 651-666, September 2008. [pdf]

·         A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. Sharon Shoham and Orna Grumberg, ACM Transactions on Computational Logic (TOCL), Volume 9, Issue 1, December 2007. [pdf]  [proofs]

·         When Not Losing Is Better than Winning: Abstraction and Refinement for the Full mu-Calculus. Orna Grumberg, Martin Lange, Martin Leucker and Sharon Shoham. Information and Computation, Volume 205, Issue 8, Pages 1130-1148, August 2007. [pdf]

Survey

·           SAT-based Model Checking: Interpolation, IC3, and Beyond. Orna Grumberg, Sharon Shoham and Yakir Vizel In Nato Science Series, 2013.

M.Sc. Thesis

·         A Game-Based Framework for CTL Counterexamples and Abstraction-Refinement.
Computer Science Department, Technion, Israel, November 2003. [pdf]

Ph.D. Thesis

·         Abstraction-Refinement and Modularity in mu-Calculus Model Checking.
Computer Science Department, Technion, Israel, January 2009. [pdf]