Sharon
Shoham Buchbinder
I am a professor in the School of Computer Science
at Tel
Aviv University.
My
main areas of research are formal verification and program analysis.
Prospective students:
I'm looking for strong PhD students, postdocs and visiting scholars. If you are
interested, please send me an email including your CV. You are also encouraged
to include letters of reference.
Contact Information
School of
Computer Science,
Checkpoint
building, room 343
Tel Aviv University
Email:
sharon.shoham 'at' gmail.com
Service
Conference Organization:
54th
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2027.
Program Chair.
34th
International Conference on Computer Aided
Verification (CAV) 2022. Program co-chair, together with Yakir Vizel.
22nd
International Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI) 2021. Program co-chair,
together with Fritz Henglein and Yakir Vizel.
Workshop Organization:
Best of
Model Checking (BeMC) workshop, July 13th,
2019, New York, co-located with CAV
2019. Co-chaired with Yakir Vizel.
Program committee member:
2026 38th International Conference on Computer Aided
Verification (CAV'26)
2025 31st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'25)
2025 Associate Chair for 52nd ACM SIGPLAN Symposium
on Principles of Programming Languages (POPL'25)
2024 36th International Conference on Computer Aided
Verification (CAV'24)
2024 30th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'24)
2023 35th International Conference on Computer Aided
Verification (CAV'23)
2023 29th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'23)
2022 International Conference on Formal Methods in
Computer-Aided Design (FMCAD'22)
2021 33rd International Conference on Computer Aided
Verification (CAV'21)
2020 32nd International Conference on Computer Aided
Verification (CAV'20)
2019 31st International Conference on Computer Aided
Verification (CAV'19)
2019 ACM SIGPLAN Conference on Programming Language
Design and Implementation (PLDI'19), Extended Review Committee (ERC)
member
2019 20th International Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI'19)
2018 International Conference on Formal Methods in
Computer-Aided Design (FMCAD'18)
2018 30th International Conference on Computer Aided
Verification (CAV'18)
2017 ACM SIGPLAN Conference on Programming Language
Design and Implementation (PLDI'17)
2017 44th ACM SIGPLAN Symposium on Principles of
Programming Languages (POPL'17)
2016 16th conference on Formal Methods in Computer
Aided Design (FMCAD'16)
2016 28th International Conference on Computer Aided
Verification (CAV'16)
2016 17th International Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI'16)
2015 11th Haifa Verification Conference (HVC'15)
2015 27th International Conference on Computer Aided
Verification (CAV'15)
2014 10th Haifa Verification Conference (HVC'14)
2013 4th International Symposium on Games, Automata,
Logics, and Formal Verification (GANDALF'13)
Recent Talks
·
Taming
Infinity for Verification in First Order Logic. 30th
International Conference on
Automated Deduction (CADE), Stuttgart, Germany, July 2025. [slides]
·
From
Concept Learning to SAT-Based Invariant Inference. 43rd
conference on Foundations
of Software Technology and Theoretical Computer Science (FSTTCS) 2023, IIIT
Hyderabad, India, December 2023. [slides]
·
Towards a
Theoretical Understanding of Property-Directed Reachability. 24th
International Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI) 2023, co-located with
POPL’23, Boston, MA, USA, January 2023. [slides]
·
SAT-Based
Invariant Inference and Its Relation to Concept Learning. 16th
International Conference on Reachability
Problems (RP) 2022, Kaiserslautern, Germany, October 2022. [pdf] [slides]
·
Verification
of Distributed Protocols Using Decidable Logic. Programming
Languages Mentoring Workshop (PLMW) 2019, Cascais,
Portugal, January 2019. [slides]
·
Interactive
Verification of Distributed Protocols Using Decidable Logic. 25th
Static
Analysis Symposium, Freiburg im Breisgau, Germany, August 2018. [slides]
·
Verification
of Infinite-State Systems Using Decidable Logic. Verification and Deduction Mentoring Workshop, co-located
with the Federated Logic Conference (FLOC’18), Oxford, UK, July 2018. [slides]
·
Safety
Verification of Stateful Networks.
Fourth Workshop on Networking and Programming Languages (NetPL),
co-located with POPL’18, Los Angeles, CA, USA, January, 2018. [slides]
·
Interactive
Verification of Distributed Protocols. Workshop on Software
Correctness and Reliability, ETH, Zurich, Switzerland, October 2017. [slides]
·
Synthesizing
Universally-Quantified Inductive Invariants. 6th
Workshop on Synthesis (SYNT), collocated with the 29th International
Conference on Computer Aided Verification (CAV), Heidelberg, Germany, 2017. [slides]
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
|
·
Lagrangian-Based Duality for Quantified SMT
Algorithms. Ivana Bocevska, Takeshi
Tsukada, Hiroshi Unno, Oded Padon and Sharon Shoham, In
Proceedings of the 38th International Conference on Computer Aided
Verification (CAV) 2026. ·
Automatic Abstraction Refinement for Hyperproperties
Verification. Malak Marrid, Shachar Itzhaky, Sharon Shoham
and Yakir Vizel, In
Proceedings of the 13th International Joint Conference on Automated Reasoning
(IJCAR) 2026. [zenodo] ·
Decidability Results for Fragments of First-Order Logic via a
Symbolic Model Property. Neta Elad and Sharon
Shoham, In Proceedings of the 41st ACM/IEEE Symposium on Logic in Computer
Science (LICS) 2026. [arxiv] ·
Simplifying Safety Proofs with Forward-Backward Reasoning and
Prophecy. Eden Frenkel, Kenneth L. McMillan, Oded Padon and Sharon Shoham, In
Proceedings of the ACM on Programming Languages (PACMPL), PLDI 2026. [arxiv] ·
Verifying First-Order Temporal Properties of Infinite-State
Systems via Timers and Rankings. Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham, In
Proceedings of the 32nd International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS) 2026. [pdf] [arxiv] ·
Separating the Wheat from the Chaff: Understanding
(In-)Completeness of Proof Mechanisms for Separation Logic with Inductive
Definitions. Neta Elad, Adithya Murali and Sharon
Shoham, In Proceedings of the ACM on Programming Languages (PACMPL), POPL
2026. [pdf]
[arxiv] ·
Implicit Rankings for Verifying Liveness Properties in
First-Order Logic. Raz Lotan and Sharon Shoham, In Proceedings of
the 31st International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS) 2025. [pdf] [arxiv] ·
Axe 'Em: Eliminating Spurious States
with Induction Axioms. Neta Elad and Sharon Shoham, In Proceedings of
the ACM on Programming Languages (PACMPL), POPL 2025. [pdf] [arxiv] ·
A Primal-Dual Perspective on Program Verification Algorithms. Takeshi
Tsukada, Hiroshi Unno, Oded Padon and Sharon Shoham, In Proceedings of the
ACM on Programming Languages (PACMPL), POPL 2025. Distinguished paper
award [pdf] [arxiv] ·
Hyperproperty-Preserving
Register Specifications. Yoav Ben
Shimon, Ori Lahav and Sharon Shoham, In Proceedings of the 38th
International Symposium on Distributed Computing (DISC) 2024. Best
paper award and best student paper award [pdf] [arxiv] ·
Proving Cutoff Bounds for Safety Properties in First-Order
Logic. Raz Lotan, Eden Frenkel and Sharon Shoham, In
Proceedings of the 22nd International Symposium on Automated Technology for
Verification and Analysis (ATVA) 2024. [pdf] [arxiv] ·
Efficient Implementation of an Abstract Domain of Quantified
First-Order Formulas. Eden Frenkel, Tej Chajed, Oded Padon and Sharon
Shoham, In Proceedings of the 36th International Conference on Computer
Aided Verification (CAV) 2024. [pdf] [arxiv] ·
mypyvy: A Research Platform for
Verification of Transition Systems in First-Order Logic. James
R. Wilcox, Yotam M. Y. Feldman, Oded Padon and Sharon Shoham, In
Proceedings of the 36th International Conference on Computer Aided
Verification (CAV) 2024. [pdf] ·
Hyperproperty
Verification as CHC Satisfiability. Shachar Itzhaky, Sharon Shoham and Yakir Vizel, In
Proceedings of the 33rd European Symposium on Programming (ESOP) 2024. [pdf] [arxiv]
[artifact] ·
Speculative SAT Modulo SAT. Hari Govind V. K., Isabel
Garcia-Contreras, Sharon Shoham and Arie Gurfinkel, In Proceedings of the
30th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS) 2024. [pdf] ·
An Infinite Needle in a Finite Haystack: Finding Infinite
Counter-Models in Deductive Verification. Neta Elad, Oded Padon
and Sharon Shoham, In Proceedings of the ACM on Programming Languages
(PACMPL), POPL 2024. Distinguished paper award [pdf] [arxiv] ·
State Merging with Quantifiers in Symbolic Execution. David
Trabish, Noam Rinetzky, Sharon Shoham and Vaibhav
Sharma, In Proceedimgs of the ACM Joint European
Software Engineering Conference and Symposium on the Foundations of Software
Engineering (ESEC/FSE), December 2023. [pdf] [arxiv] ·
Counterexample Driven Quantifier Instantiations with
Applications to Distributed Protocols, Orr Tamir, Marcelo
Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta,and Mooly
Sagiv, In Proceedings of the ACM on Programming
Languages (PACMPL), OOPSLA, 2023. [pdf] ·
Fast Approximations of Quantifier Elimination, Isabel
Garcia-Contreras, Hari Govind V. K., Sharon Shoham and Arie Gurfinkel, In
Proceedings of the 35th International Conference on Computer Aided
Verification (CAV) 2023. Distinguished paper award [pdf] [arxiv]
·
Invariant Inference with Provable Complexity from the Monotone
Theory. Yotam M. Y. Feldman and Sharon Shoham, In
Proceedings of the 29th Static Analysis Symposium (SAS), Auckland, New
Zealand, 2022. [pdf] [arxiv] ·
Inferring Invariants with Quantifier Alternations: Taming the
Search Space Explosion. Jason R. Koenig, Oded Padon, Sharon Shoham and
Alex Aiken, In proceedings of the 28th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS) 2022.
[pdf] [arxiv] ·
Property-directed reachability as abstract interpretation in
the monotone theory. Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham
and James R. Wilcox, In Proceedings of the ACM on Programming Languages
(PACMPL), POPL 2022. [pdf]
[arxiv] ·
Solving constrained Horn clauses modulo algebraic data types
and recursive functions. Hari Govind V. K., Sharon Shoham and Arie
Gurfinkel, In Proceedings of the ACM on Programming Languages (PACMPL) , POPL 2022. [pdf] ·
Cost-effective capacity provisioning in wide area networks
with Shoofly. Rachee Singh, Nikolaj S. Bjørner, Sharon
Shoham, Yawei Yin, John Arnold and Jamie Gaudette, In ACM SIGCOMM Conference 2021. [link] ·
Logical Characterization of Coherent Uninterpreted
Programs. Hari Govind V. K., Sharon Shoham and Arie
Gurfinkel, In Proceedings of Formal Methods in Computer-Aided Design
(FMCAD) 2021. [pdf]
[arxiv] ·
Run-time Complexity Bounds Using Squeezers. Oren
Ish-Shalom, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham, In
Proceedings of the 30th European Symposium on Programming (ESOP) 2021. [pdf] ·
Learning the boundary of inductive invariants. Yotam
M. Y. Feldman, Mooly Sagiv, Sharon Shoham and James R. Wilcox, In
Proceedings of the ACM on Programming Languages (PACMPL), POPL 2021. [pdf] [arxiv] ·
Proving highly-concurrent traversals correct. Yotam
M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar
Nanevski, Noam Rinetzky and Sharon Shoham, In Proceedings of the ACM on
Programming Languages (PACMPL), OOPSLA 2020. [pdf] [arxiv] ·
Global Guidance for Local Generalization in Model Checking. Hari
Govind Vediramana
Krishnan, YuTing Chen, Sharon Shoham and Arie
Gurfinkel, In Proceedings of the 32nd International Conference
on Computer Aided Verification (CAV) 2020. [pdf] [arxiv] · Complexity and information in invariant inference. Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv and Sharon Shoham, In Proceedings of the ACM on Programming Languages (PACMPL), POPL 2020. [pdf] [arxiv] ·
Putting the Squeeze on Array Programs: Loop Verification via
Inductive Rank Reduction. Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky
and Sharon Shoham, In Proceedings of the 21st International
Conference on Verification, Model Checking, and Abstract Interpretation
(VMCAI), New Orleans, LA, USA, January 2020. [pdf] [arxiv] ·
Solving LIA* Using Approximations. Maxwell
Levatich, Nikolaj Bjørner, Ruzica Piskac and
Sharon Shoham, In Proceedings of the 21st International
Conference on Verification, Model Checking, and Abstract Interpretation
(VMCAI), New Orleans, LA, USA, January 2020. [pdf] ·
Verification of Threshold-based Distributed Algorithms by
Decomposition to Decidable Logics. Idan Berkovits, Marijana Lazic, Giuliano Lossa, Oded Padon and Sharon Shoham, In
Proceedings of the 31st International Conference on Computer Aided
Verification (CAV) 2019. [pdf]
[arxiv] ·
Property Directed Self Composition. Ron
Shemer, Arie Gurfinkel, Sharon Shoham and Yakir Vizel, In Proceedings of
the 31st International Conference on Computer Aided Verification
(CAV) 2019. [pdf]
[arxiv] ·
Inferring Inductive Invariants from Phase Structures. Yotam
M. Y. Feldman, James R. Wilcox, Sharon Shoham and Mooly Sagiv, In
Proceedings of the 31st International Conference on Computer Aided
Verification (CAV) 2019. [pdf]
[arxiv] ·
Order out of Chaos: Proving Linearizability
Using Local Views. Yotam M. Y. Feldman, Constantin Enea, Adam
Morrison, Noam Rinetzky and Sharon Shoham, In Proceedings of the
International Symposium on DIStributed Computing
(DISC), New Orleans, USA, October 2018. [pdf] [arxiv] ·
Temporal Prophecy for Proving Temporal Properties of
Infinite-State Systems. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan,
Andreas Podelski, Mooly Sagiv and Sharon Shoham, In Proceedings of
Formal Methods in Computer-Aided Design (FMCAD), University of Texas, Austin,
Texas, 30 Oct - 2 Nov, 2018. [pdf]
[arxiv] ·
Quantifiers on Demand. Arie Gurfinkel, Sharon
Shoham and Yakir Vizel, In Proceedings of the International
Symposium on Automated Technology for Verification and Analysis (ATVA), Los
Angeles, USA, October 2018. [pdf]
[arxiv] ·
Modular Verification of Concurrent Programs via Sequential
Model Checking. Dan Rasin, Orna Grumberg and Sharon
Shoham, In Proceedings of the International Symposium on Automated
Technology for Verification and Analysis (ATVA), Los Angeles, USA, October
2018. [pdf]
[arxiv] ·
Inferring Program Extensions from Traces. Roman
Manevich and Sharon Shoham, In Proceedings of the 14th
International Conference on Grammatical Inference (ICGI), Wrocław,
Poland, September 2018. [pdf] ·
Abstract Interpretation of Stateful
Network. Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham and Yaron
Velner, In Proceedings of the 25th
Static Analysis Symposium (SAS), Freiburg im Breisgau, Germany, August 2018. [pdf] [arxiv] ·
Discovering Universally Quantified Solutions for Constrained Horn
Clauses. Arie Gurfinkel, Sharon Shoham and Yakir Vizel, International
Workshop on Satisfiability Modulo Theories (SMT), July 2018, Oxford, UK,
Affiliated with IJCAR 2018, part of FLoC 2018. [pdf] ·
Modularity for decidability of deductive verification with
applications to distributed systems. Marcelo Taube, Giuliano
Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R.
Wilcox and Doug Woos, In Proceedings of the 39th ACM SIGPLAN
Conference on Programming Language Design and Implementation (PLDI) 2018.
[pdf] ·
Programming Not Only by Example. Hila
Peleg, Sharon Shoham and Eran Yahav, In Proceedings of the 40th
International Conference on Software Engineering (ICSE) 2018. [pdf] ·
Reducing liveness to safety in first-order logic. Oded
Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv and
Sharon Shoham, In Proceedings of the ACM on Programming Languages (POPL)
2018. [pdf]
[web] ·
Abstraction-Based Interaction Model for Synthesis. Hila
Peleg, Shachar Itzhaky and Sharon Shoham, In Proceedings of the
International Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI) 2018. [pdf] ·
Paxos made EPR: decidable reasoning
about distributed protocols. Oded Padon, Giuliano Losa, Mooly Sagiv and Sharon
Shoham, In
Proceedings of the ACM on Programming Languages (OOPSLA) 2017. [pdf] [web] ·
RATCOP: Relational Analysis Tool for Concurrent Programs. Suvam
Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza and Noam Rinetzky, In Proceedings of the Haifa Verification
Conference (HVC) 2017. [pdf] ·
Thread-Local Semantics and its Efficient Sequential
Abstractions for Race-Free Programs. Suvam Mukherjee, Oded
Padon, Sharon Shoham, Deepak D'Souza and Noam Rinetzky, In proceedings of the 24th Static Analysis Symposium
(SAS) 2017. [pdf] ·
Synthesis with Abstract Examples. Dana
Drachsler Cohen, Sharon Shoham, and Eran Yahav, In proceedings of the 29th International
Conference on Computer Aided Verification (CAV) 2017. [pdf] ·
Bounded Quantifier Instantiation for Checking Inductive
Invariants. Yotam M. Y. Feldman, Oded Padon, Neil Immerman,
Mooly Sagiv, and Sharon Shoham, In
proceedings of the 23rd International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS) 2017. [pdf] ·
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]
[artifact] ·
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. Best
paper award. [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
|
· Global guidance for local generalization in model checking. Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham and Arie Gurfinkel, Formal Methods in System Design (FMSD) 63(1): 81-109, 2024. Special issue of CAV’20-21 [link] [arxiv] · Runtime Complexity Bounds Using Squeezers. Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham, ACM Trans. Program. Lang. Syst. (TOPLAS) 44(3): 17:1-17:36, 2022. [link] [arxiv] · Temporal prophecy for proving temporal properties of infinite-state systems. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv and Sharon Shoham, Formal Methods in System Design (FMSD) 57(2): 246-269, 2021. [link] [arxiv] · Programming by Predicates: A formal model for interactive synthesis. Hila Peleg, Shachar Itzhaky, Sharon Shoham and Eran Yahav, Acta Informatica, Volume 57 Number 1-2, Special Issue on Synthesis, Pages 165–193, 2020. [pdf] · Some complexity results for stateful network verification. Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham and Yaron Velner, Formal Methods in System Design (FMSD), Volume 54, Number 2, Pages 191-231, 2019. [pdf] [arxiv] · Bounded Quantifier Instantiation for Checking Inductive Invariants. Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv and Sharon Shoham, Logical Methods in Computer Science (LMCS), Volume 15, Number 3, 2019. [pdf] [arxiv] · Automated circular assume-guarantee reasoning. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham, Formal Aspects of Computing, special issue of FM’15, Volume 30, Number 5, Pages 571-595, 2018. [pdf] · Property-Directed Inference of Universal Invariants or Proving Their Absence. Aleksandr Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham, Journal of the ACM, Volume 64, Number 1, Pages 7:1-7:33, 2017. [pdf] · A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement. Yael Meller, Orna Grumberg and Sharon Shoham, Information and Computation, Volume 247, Pages 169-202, 2016. [pdf] · Symbolic Automata for Representing Big Code. Hila Peleg, Sharon Shoham, Eran Yahav and and Hongseok Yang, Special issue of Acta Informatica devoted to COST Action IC0901, Volume 53, Number 4, Pages 327-356, 2016. [pdf] · 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. |
Ph.D. Thesis
|
·
Abstraction-Refinement and Modularity in mu-Calculus Model
Checking. |
Students' Theses
·
Karam Abd Elkader, M.Sc., Computer Science Department, Technion, 2016. Automated
Circular Assume-Guarantee Reasoning. [pdf]
·
Kalev Alpernas, M.Sc., Computer
Science, Tel-Aviv University, 2016. Safety
Verification of Stateful Networks. [pdf]
·
Asya Frumkin, M.Sc., Computer Science, Tel-Aviv University,
2017. Property Directed Reachability for
Proving Absence of Concurrent Modification Errors. [pdf]
·
Yotam M. Y. Feldman, M.Sc., Computer
Science, Tel-Aviv University, 2017. Bounded
Quantifier Instantiation for Checking Inductive Invariants. [pdf]
·
Dan Rasin, M.Sc., Computer Science Department, Technion,
2018. Modular Verification of Concurrent
Programs via Sequential Model Checking. [pdf]
·
Adi Omari, Ph.D., Computer
Science Department, Technion, 2018. Scalable Data Extraction via Program Synthesis. [pdf]
·
Ron Shemer, M.Sc., Computer
Science, Tel-Aviv University, 2019. Property
Directed Self Composition. [pdf]
·
Idan Berkovits, M.Sc., Computer Science, Tel-Aviv University,
2020. Verification of Threshold-Based
Distributed Algorithms by Decomposition to Decidable Logics. [pdf]
·
Yotam Feldman, Ph.D., Computer
Science, Tel-Aviv University, 2022. Towards a
Theory of Learning Inductive Invariants. [pdf]
·
Raz Lotan, M.Sc., Computer
Science, Tel-Aviv University, 2025. Approximating
Undefinable Concepts for Verification in First-Order Logic. [pdf]
Teaching
·
Logic for
Computer Science, Tel-Aviv University
·
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)