Sharon Shoham

138 papers A* 10A 9B 23Journal 67Unranked 25
YearRankTypeTitle / Venue / Authors
2026 — conf
On the Power of Temporal Prophecy.
On the Pursuit of Insight and Elegance
Jochen Hoenicke, Oded Padon, Sharon Shoham
2026 J jnl
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions.
Proc. ACM Program. Lang.
Neta Elad, Adithya Murali, Sharon Shoham
2026 — conf
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings.
TACAS (2)
Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham
2026 J jnl
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings.
CoRR
Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version).
CoRR
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms.
Proc. ACM Program. Lang.
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 J jnl
Axe 'Em: Eliminating Spurious States with Induction Axioms.
Proc. ACM Program. Lang.
Neta Elad, Sharon Shoham
2025 — conf
Implicit Rankings for Verifying Liveness Properties in First-Order Logic.
TACAS (1)
Raz Lotan, Sharon Shoham
2025 J jnl
Preface of the special issue on the Conference on Computer-Aided Verification 2022.
Formal Methods Syst. Des.
Sharon Shoham, Yakir Vizel
2025 J jnl
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions.
CoRR
Neta Elad, Adithya Murali, Sharon Shoham
2024 J jnl
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.
Proc. ACM Program. Lang.
Neta Elad, Oded Padon, Sharon Shoham
2024 J jnl
Axe 'Em: Eliminating Spurious States with Induction Axioms.
CoRR
Neta Elad, Sharon Shoham
2024 — conf
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CAV (2)
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 J jnl
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CoRR
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 J jnl
Global guidance for local generalization in model checking.
Formal Methods Syst. Des.
Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
2024 — conf
Hyperproperty Verification as CHC Satisfiability.
ESOP (2)
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2024 J jnl
Hyperproperty-Preserving Register Specifications (Extended Version).
CoRR
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
2024 A conf
Hyperproperty-Preserving Register Specifications.
DISC
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
2024 J jnl
Implicit Rankings for Verifying Liveness Properties in First-Order Logic.
CoRR
Raz Lotan, Sharon Shoham
2024 B conf
Proving Cutoff Bounds for Safety Properties in First-Order Logic.
ATVA
Raz Lotan, Eden Frenkel, Sharon Shoham
2024 J jnl
Proving Cutoff Bounds for Safety Properties in First-Order Logic.
CoRR
Raz Lotan, Eden Frenkel, Sharon Shoham
2024 — conf
Speculative SAT Modulo SAT.
TACAS (1)
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
2024 — conf
mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic.
CAV (2)
James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham
2023 J jnl
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.
CoRR
Neta Elad, Oded Padon, Sharon Shoham
2023 J jnl
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols.
Proc. ACM Program. Lang.
Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
2023 — conf
Fast Approximations of Quantifier Elimination.
CAV (2)
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2023 J jnl
Fast Approximations of Quantifier Elimination.
CoRR
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2023 — conf
From Concept Learning to SAT-Based Invariant Inference (Invited Talk).
FSTTCS
Sharon Shoham
2023 J jnl
Hyperproperty Verification as CHC Satisfiability.
CoRR
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
2023 J jnl
Speculative SAT Modulo SAT.
CoRR
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
2023 — conf
State Merging with Quantifiers in Symbolic Execution.
ESEC/SIGSOFT FSE
David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma
2023 J jnl
State Merging with Quantifiers in Symbolic Execution.
CoRR
David Trabish, Noam Rinetzky, Sharon Shoham, Vaibhav Sharma
2022 — ed.
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I
CAV (1)
Sharon Shoham, Yakir Vizel
2022 — ed.
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II
CAV (2)
Sharon Shoham, Yakir Vizel
2022 — conf
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.
TACAS (1)
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
2022 J jnl
Invariant Inference With Provable Complexity From the Monotone Theory.
CoRR
Yotam M. Y. Feldman, Sharon Shoham
2022 B conf
Invariant Inference with Provable Complexity from the Monotone Theory.
SAS
Yotam M. Y. Feldman, Sharon Shoham
2022 J jnl
Property-directed reachability as abstract interpretation in the monotone theory.
Proc. ACM Program. Lang.
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2022 J jnl
Runtime Complexity Bounds Using Squeezers.
ACM Trans. Program. Lang. Syst.
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2022 — conf
SAT-Based Invariant Inference and Its Relation to Concept Learning.
RP
Yotam M. Y. Feldman, Sharon Shoham
2022 J jnl
Solving constrained Horn clauses modulo algebraic data types and recursive functions.
Proc. ACM Program. Lang.
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2021 A* conf
Cost-effective capacity provisioning in wide area networks with Shoofly.
SIGCOMM
Rachee Singh, Nikolaj S. Bjørner, Sharon Shoham, Yawei Yin, John Arnold, Jamie Gaudette
2021 J jnl
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.
CoRR
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
2021 J jnl
Learning the boundary of inductive invariants.
Proc. ACM Program. Lang.
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2021 B conf
Logical Characterization of Coherent Uninterpreted Programs.
FMCAD
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2021 J jnl
Logical Characterization of Coherent Uninterpreted Programs.
CoRR
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2021 J jnl
Modular Verification of Concurrent Programs via Sequential Model Checking.
CoRR
Dan Rasin, Orna Grumberg, Sharon Shoham
2021 J jnl
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory.
CoRR
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
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 J jnl
Quantifiers on Demand.
CoRR
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2021 A conf
Run-time Complexity Bounds Using Squeezers.
ESOP
Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
2021 J jnl
Some Complexity Results for Stateful Network Verification.
CoRR
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2021 J jnl
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
CoRR
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021 J jnl
Temporal prophecy for proving temporal properties of infinite-state systems.
Formal Methods Syst. Des.
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021 B ed.
Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings
VMCAI
Fritz Henglein, Sharon Shoham, Yakir Vizel
2020 J jnl
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs.
CoRR
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2020 J jnl
Complexity and information in invariant inference.
Proc. ACM Program. Lang.
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
2020 — conf
Global Guidance for Local Generalization in Model Checking.
CAV (2)
Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
2020 J jnl
Global Guidance for Local Generalization in Model Checking.
CoRR
Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel
2020 J jnl
Learning the Boundary of Inductive Invariants.
CoRR
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
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
Proving Highly-Concurrent Traversals Correct.
CoRR
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
2020 J jnl
Proving highly-concurrent traversals correct.
Proc. ACM Program. Lang.
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
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 B conf
Solving $\mathrm {LIA} ^\star $ Using Approximations.
VMCAI
Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham
2019 J jnl
Bounded Quantifier Instantiation for Checking Inductive Invariants.
Log. Methods Comput. Sci.
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2019 J jnl
Complexity and Information in Invariant Inference.
CoRR
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
2019 — conf
Inferring Inductive Invariants from Phase Structures.
CAV (2)
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
2019 J jnl
Inferring Inductive Invariants from Phase Structures.
CoRR
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
2019 — conf
Property Directed Self Composition.
CAV (1)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2019 J jnl
Property Directed Self Composition.
CoRR
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2019 J jnl
Some complexity results for stateful network verification.
Formal Methods Syst. Des.
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2019 — conf
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.
CAV (2)
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
2019 J jnl
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.
CoRR
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
2018 B conf
Abstract Interpretation of Stateful Networks.
SAS
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2018 B conf
Abstraction-Based Interaction Model for Synthesis.
VMCAI
Hila Peleg, Shachar Itzhaky, Sharon Shoham
2018 J jnl
Automated circular assume-guarantee reasoning.
Formal Aspects Comput.
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2018 — conf
Inferring Program Extensions from Traces.
ICGI
Roman Manevich, Sharon Shoham
2018 B conf
Interactive Verification of Distributed Protocols Using Decidable Logic.
SAS
Sharon Shoham
2018 B conf
Modular Verification of Concurrent Programs via Sequential Model Checking.
ATVA
Dan Rasin, Orna Grumberg, Sharon Shoham
2018 A* conf
Modularity for decidability of deductive verification with applications to distributed systems.
PLDI
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
2018 A conf
Order out of Chaos: Proving Linearizability Using Local Views.
DISC
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham
2018 J jnl
Order out of Chaos: Proving Linearizability Using Local Views.
CoRR
Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham
2018 A* conf
Programming not only by example.
ICSE
Hila Peleg, Sharon Shoham, Eran Yahav
2018 B conf
Quantifiers on Demand.
ATVA
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2018 J jnl
Reducing liveness to safety in first-order logic.
Proc. ACM Program. Lang.
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018 B conf
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
FMCAD
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018 J jnl
Undecidability of Inferring Linear Integer Invariants.
CoRR
Sharon Shoham
2017 — conf
Bounded Quantifier Instantiation for Checking Inductive Invariants.
TACAS (1)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017 J jnl
Bounded Quantifier Instantiation for Checking Inductive Invariants.
CoRR
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017 B conf
IC3 - Flipping the E in ICE.
VMCAI
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
2017 J jnl
Modular Safety Verification for Stateful Networks.
CoRR
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2017 J jnl
Paxos Made EPR: Decidable Reasoning about Distributed Protocols.
CoRR
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017 J jnl
Paxos made EPR: decidable reasoning about distributed protocols.
Proc. ACM Program. Lang.
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017 J jnl
Programming Not Only by Example.
CoRR
Hila Peleg, Sharon Shoham, Eran Yahav
2017 B conf
Property Directed Reachability for Proving Absence of Concurrent Modification Errors.
VMCAI
Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
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
RATCOP: Relational Analysis Tool for Concurrent Programs.
Haifa Verification Conference
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2017 A conf
Synthesis of Forgiving Data Extractors.
WSDM
Adi Omari, Sharon Shoham, Eran Yahav
2017 — conf
Synthesis with Abstract Examples.
CAV (1)
Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav
2017 B conf
Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs.
SAS
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2016 J jnl
A framework for compositional verification of multi-valued systems via abstraction-refinement.
Inf. Comput.
Yael Meller, Orna Grumberg, Sharon Shoham
2016 — conf
Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement.
CAV (1)
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2016 A* conf
Cross-supervised synthesis of web-crawlers.
ICSE
Adi Omari, Sharon Shoham, Eran Yahav
2016 B conf
D^3 : Data-Driven Disjunctive Abstraction.
VMCAI
Hila Peleg, Sharon Shoham, Eran Yahav
2016 A* conf
Decidability of inferring inductive invariants.
POPL
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv
2016 A* conf
Ivy: safety verification by interactive generalization.
PLDI
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
2016 A* conf
Lossless Separation of Web Pages into Layout Code and Data.
KDD
Adi Omari, Benny Kimelfeld, Eran Yahav, Sharon Shoham
2016 B conf
Property Directed Abstract Interpretation.
VMCAI
Noam Rinetzky, Sharon Shoham
2016 — conf
SMT-based verification of parameterized systems.
SIGSOFT FSE
Arie Gurfinkel, Sharon Shoham, Yuri Meshman
2016 A conf
Some Complexity Results for Stateful Network Verification.
TACAS
Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham
2016 J jnl
Symbolic automata for representing big code.
Acta Informatica
Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang
2015 B conf
Automated Circular Assume-Guarantee Reasoning.
FM
Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
2015 A* conf
Decentralizing SDN Policies.
POPL
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
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 — ch.
SAT-based Model Checking: Interpolation, IC3, and Beyond.
Software Systems Safety
Orna Grumberg, Sharon Shoham, Yakir Vizel
2013 A conf
Intertwined Forward-Backward Reachability Analysis Using Interpolants.
TACAS
Yakir Vizel, Orna Grumberg, Sharon Shoham
2013 B conf
Symbolic Automata for Static Specification Mining.
SAS
Hila Peleg, Sharon Shoham, Eran Yahav, Hongseok Yang
2012 B conf
Lazy abstraction and SAT-based reachability in hardware model checking.
FMCAD
Yakir Vizel, Orna Grumberg, Sharon Shoham
2012 J jnl
Multi-valued model checking games.
J. Comput. Syst. Sci.
Sharon Shoham, Orna Grumberg
2012 A conf
Typestate-based semantic code search over partial programs.
OOPSLA
Alon Mishne, Sharon Shoham, Eran Yahav
2011 J jnl
Local abstraction-refinement for the
Int. J. Softw. Tools Technol. Transf.
Harald Fecher, Sharon Shoham
2010 J jnl
Compositional verification and 3-valued abstractions join forces.
Inf. Comput.
Sharon Shoham, Orna Grumberg
2009 B conf
A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement.
ATVA
Yael Meller, Orna Grumberg, Sharon Shoham
2009 — —
Abstraction-refinement and modularity in μ-calculus model checking.
Sharon Shoham
2008 J jnl
3-Valued abstraction: More precision at less cost.
Inf. Comput.
Sharon Shoham, Orna Grumberg
2008 J jnl
Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules.
Stud Logica
Sharon Shoham, Nissim Francez
2008 — conf
State Focusing: Lazy Abstraction for the Mu-Calculus.
SPIN
Harald Fecher, Sharon Shoham
2008 J jnl
Static Specification Mining Using Automata-Based Abstractions.
IEEE Trans. Software Eng.
Sharon Shoham, Eran Yahav, Stephen J. Fink, Marco Pistoia
2007 J jnl
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
ACM Trans. Comput. Log.
Sharon Shoham, Orna Grumberg
2007 B conf
Compositional Verification and 3-Valued Abstractions Join Forces.
SAS
Sharon Shoham, Orna Grumberg
2007 — conf
Local Abstraction-Refinement for the mu-Calculus.
SPIN
Harald Fecher, Sharon Shoham
2007 A conf
Static specification mining using automata-based abstractions.
ISSTA
Sharon Shoham, Eran Yahav, Stephen Fink, Marco Pistoia
2007 J jnl
When not losing is better than winning: Abstraction and refinement for the full mu-calculus.
Inf. Comput.
Orna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham
2006 A* conf
3-Valued Abstraction: More Precision at Less Cost.
LICS
Sharon Shoham, Orna Grumberg
2005 B conf
Multi-valued Model Checking Games.
ATVA
Sharon Shoham, Orna Grumberg
2004 A conf
Monotonic Abstraction-Refinement for CTL.
TACAS
Sharon Shoham, Orna Grumberg
2003 A* conf
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.
CAV
Sharon Shoham, Orna Grumberg