# Sharon Shoham

According to our database1, Sharon Shoham authored at least 60 papers between 2004 and 2020.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2020
Complexity and information in invariant inference.
Proc. ACM Program. Lang., 2020

Programming by predicates: a formal model for interactive synthesis.
Acta Informatica, 2020

Solving $\mathrm {LIA} ^\star$ Using Approximations.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Global Guidance for Local Generalization in Model Checking.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Bounded Quantifier Instantiation for Checking Inductive Invariants.
Log. Methods Comput. Sci., 2019

Some complexity results for stateful network verification.
Formal Methods Syst. Des., 2019

Property Directed Self Composition.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Inferring Inductive Invariants from Phase Structures.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Reducing liveness to safety in first-order logic.
Proc. ACM Program. Lang., 2018

Automated circular assume-guarantee reasoning.
Formal Asp. Comput., 2018

Undecidability of Inferring Linear Integer Invariants.
CoRR, 2018

Order out of Chaos: Proving Linearizability Using Local Views.
Proceedings of the 32nd International Symposium on Distributed Computing, 2018

Abstraction-Based Interaction Model for Synthesis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Interactive Verification of Distributed Protocols Using Decidable Logic.
Proceedings of the Static Analysis - 25th International Symposium, 2018

Abstract Interpretation of Stateful Networks.
Proceedings of the Static Analysis - 25th International Symposium, 2018

Modularity for decidability of deductive verification with applications to distributed systems.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Programming not only by example.
Proceedings of the 40th International Conference on Software Engineering, 2018

Inferring Program Extensions from Traces.
Proceedings of the 14th International Conference on Grammatical Inference, 2018

Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Modular Verification of Concurrent Programs via Sequential Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2018

Quantifiers on Demand.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Paxos made EPR: decidable reasoning about distributed protocols.
Proc. ACM Program. Lang., 2017

Property-Directed Inference of Universal Invariants or Proving Their Absence.
J. ACM, 2017

Modular Safety Verification for Stateful Networks.
CoRR, 2017

Synthesis of Forgiving Data Extractors.
Proceedings of the Tenth ACM International Conference on Web Search and Data Mining, 2017

IC3 - Flipping the E in ICE.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Property Directed Reachability for Proving Absence of Concurrent Modification Errors.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs.
Proceedings of the Static Analysis - 24th International Symposium, 2017

RATCOP: Relational Analysis Tool for Concurrent Programs.
Proceedings of the Hardware and Software: Verification and Testing, 2017

Synthesis with Abstract Examples.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
A framework for compositional verification of multi-valued systems via abstraction-refinement.
Inf. Comput., 2016

Symbolic automata for representing big code.
Acta Informatica, 2016

Property Directed Abstract Interpretation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

D^3 : Data-Driven Disjunctive Abstraction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

SMT-based verification of parameterized systems.
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Decidability of inferring inductive invariants.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Ivy: safety verification by interactive generalization.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Lossless Separation of Web Pages into Layout Code and Data.
Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016

Cross-supervised synthesis of web-crawlers.
Proceedings of the 38th International Conference on Software Engineering, 2016

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
Decentralizing SDN Policies.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

2014
SAT-based Model Checking: Interpolation, IC3, and Beyond.
Proceedings of the Software Systems Safety, 2014

2013
Intertwined Forward-Backward Reachability Analysis Using Interpolants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Symbolic Automata for Static Specification Mining.
Proceedings of the Static Analysis - 20th International Symposium, 2013

2012
Multi-valued model checking games.
J. Comput. Syst. Sci., 2012

Typestate-based semantic code search over partial programs.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Lazy abstraction and SAT-based reachability in hardware model checking.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011
Local abstraction-refinement for the <i>μ</i>-calculus.
Int. J. Softw. Tools Technol. Transf., 2011

2010
Compositional verification and 3-valued abstractions join forces.
Inf. Comput., 2010

2008
Static Specification Mining Using Automata-Based Abstractions.
IEEE Trans. Software Eng., 2008

Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules.
Studia Logica, 2008

3-Valued abstraction: More precision at less cost.
Inf. Comput., 2008

State Focusing: Lazy Abstraction for the Mu-Calculus.
Proceedings of the Model Checking Software, 2008

2007
A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
ACM Trans. Comput. Log., 2007

When not losing is better than winning: Abstraction and refinement for the full mu-calculus.
Inf. Comput., 2007

Local Abstraction-Refinement for the mu-Calculus.
Proceedings of the Model Checking Software, 2007

2005
<i>Don't Know</i> in the µ-Calculus.
Proceedings of the Verification, 2005

2004
Monotonic Abstraction-Refinement for CTL.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004