Person: Sharon Shoham

DBLP: Shoham:Sharon

Contributed to:

2015

2015

2015

2013

2013

2012

2007

2007

2006

2005

2004

2003

2016

2016

2017

2019

2019

2017

2016

2016

2018

2018

2020

Wrote 24 papers:

CAV-2015-KarbyshevBIRS #invariant #proving

Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.

FM-2015-ElkaderGPS #automation #reasoning

Automated Circular Assume-Guarantee Reasoning (KAE, OG, CSP, SS), pp. 23–39.

POPL-2015-PadonIKLSS #policy

Decentralizing SDN Policies (OP, NI, AK, OL, MS, SS), pp. 663–676.

SAS-2013-PelegSYY #automaton #mining #specification

Symbolic Automata for Static Specification Mining (HP, SS, EY, HY), pp. 63–83.

TACAS-2013-VizelGS #analysis #reachability #using

Intertwined Forward-Backward Reachability Analysis Using Interpolants (YV, OG, SS), pp. 308–323.

OOPSLA-2012-MishneSY #code search #semantics #source code

Typestate-based semantic code search over partial programs (AM, SS, EY), pp. 997–1016.

ISSTA-2007-ShohamYFP #abstraction #mining #specification #using

Static specification mining using automata-based abstractions (SS, EY, SF, MP), pp. 174–184.

SAS-2007-ShohamG #abstraction #composition #verification

Compositional Verification and 3-Valued Abstractions Join Forces (SS, OG), pp. 69–86.

LICS-2006-ShohamG #abstraction #precise

3-Valued Abstraction: More Precision at Less Cost (SS, OG), pp. 399–410.

VMCAI-2005-GrumbergLLS #calculus

Don’t Know in the µ-Calculus (OG, ML, ML, SS), pp. 233–249.

TACAS-2004-ShohamG #abstraction

Monotonic Abstraction-Refinement for CTL (SS, OG), pp. 546–560.

CAV-2003-ShohamG #abstraction #framework #game studies

A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement (SS, OG), pp. 275–287.

FSE-2016-GurfinkelSM #smt #verification

SMT-based verification of parameterized systems (AG, SS, YM), pp. 338–348.

CAV-2016-ElkaderGPS #automation #composition #reasoning #refinement

Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement (KAE, OG, CSP, SS), pp. 329–351.

CAV-2017-Drachsler-Cohen #synthesis

Synthesis with Abstract Examples (DDC, SS, EY), pp. 254–278.

CAV-2019-ShemerGSV #composition

Property Directed Self Composition (RS, AG, SS, YV), pp. 161–179.

CAV-2019-BerkovitsLLPS #algorithm #composition #decidability #distributed #logic #verification

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (IB, ML, GL, OP, SS), pp. 245–266.

CAV-2019-FeldmanWSS #induction #invariant

Inferring Inductive Invariants from Phase Structures (YMYF, JRW, SS, MS), pp. 405–425.

OOPSLA-2017-PadonLSS #decidability #distributed #protocol #reasoning

Paxos made EPR: decidable reasoning about distributed protocols (OP, GL, MS, SS), p. 31.

PLDI-2016-PadonMPSS #interactive #named #safety #verification

Ivy: safety verification by interactive generalization (OP, KLM, AP, MS, SS), pp. 614–630.

POPL-2016-PadonISKS #decidability #induction #invariant

Decidability of inferring inductive invariants (OP, NI, SS, AK, MS), pp. 217–231.

PLDI-2018-TaubeLMPSSWW #composition #decidability #deduction #distributed #verification

Modularity for decidability of deductive verification with applications to distributed systems (MT, GL, KLM, OP, MS, SS, JRW, DW), pp. 662–677.

POPL-2018-PadonHLPSS #first-order #liveness #logic #safety

Reducing liveness to safety in first-order logic (OP, JH, GL, AP, MS, SS), p. 33.

POPL-2020-FeldmanISS #complexity #invariant

Complexity and information in invariant inference (YMYF, NI, MS, SS), p. 29.