BibSLEIGH — Mooly

Travelled to:

1 × China
1 × Estonia
1 × Hungary
1 × India
1 × Italy
1 × Korea
1 × Russia
1 × Spain
2 × Austria
2 × Germany
2 × Portugal
2 × United Kingdom
22 × USA
5 × France

Collaborated with:

E.Yahav T.W.Reps A.Aiken T.Lev-Ami G.Golan-Gueta S.Shoham N.Rinetzky G.Ramalingam N.Immerman S.Itzhaky O.Padon O.Tripp S.Gulwani R.Manevich K.L.McMillan B.Cook T.Ball G.Yorsh N.G.Bronson M.Naik H.Yang J.Berdine O.Shacham P.Hawkins K.Fisher M.C.Rinard G.Losa J.Field ∅ Y.M.Y.Feldman A.Karbyshev G.Castelnuovo I.Dillig T.Dillig G.Arnold S.Litvak N.Dor R.Bodík G.Ramalingam J.R.Wilcox A.Banerjee A.Nanevski S.Grossman O.Lahav E.Koskinen B.McCloskey A.Kuehlmann O.Kupferman A.Loginov A.Schuster N.Bjørner M.T.Vechev L.Ryzhyk O.Zomer S.Burckhardt D.Leijen M.Fähndrich J.M.Tamayo P.Liang C.Weidenbach I.Bogudlov A.Gotsman R.Shaham O.Ziv A.V.Thakur B.Li J.Hölzl A.S.Köksal A.Rybalchenko A.Chawdhary D.Weiss D.Amit A.Poetzsch-Heffter A.M.Rabinovich A.Meyer A.Bouajjani S.Cohen A.Panda J.Hoenicke A.Podelski Kalev Alpernas C.Flanagan Sadjad Fouladi Thomas Schmitz Keith Winstein I.Abraham Yan Michalevsky Y.Zohar A.Gember M.Schapira A.Valadarsky Marcelo Taube D.Woos Elazar Gershuni N.Amit A.Gurfinkel N.Narodytska J.A.Navas

Talks about:

analysi (12) shape (11) program (9) abstract (7) modular (7) concurr (5) verifi (5) heap (5) data (5) synthesi (4)

Person: Mooly Sagiv

DBLP: Sagiv:Mooly

Facilitated 2 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2017

2019

2017

2018

2016

2018

2019

2020

Wrote 62 papers:

PLDI-2015-ZivAGRS #concurrent: Composing concurrency control (OZ, AA, GGG, GR, MS), pp. 240–249.
POPL-2015-PadonIKLSS #policy: Decentralizing SDN Policies (OP, NI, AK, OL, MS, SS), pp. 663–676.
PPoPP-2015-Golan-GuetaRSY #automation #scalability #semantics: Automatic scalable atomicity via semantic locking (GGG, GR, MS, EY), pp. 31–41.
SAS-2015-CastelnuovoNRSY #analysis #bottom-up #case study #composition #top-down: Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis (GC, MN, NR, MS, HY), pp. 252–274.
CAV-2014-ItzhakyBRST #analysis: Property-Directed Shape Analysis (SI, NB, TWR, MS, AVT), pp. 35–51.
ESOP-2014-ZomerGRS #encapsulation: Checking Linearizability of Encapsulated Extended Operations (OZ, GGG, GR, MS), pp. 311–330.
ISSTA-2014-ShachamYGABSV #independence #verification: Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.
PLDI-2014-BallBGIKSSV #named #network #source code #towards #verification: VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
POPL-2014-ItzhakyBILNS #composition #effectiveness #reasoning: Modular reasoning about heap paths via effectively propositional formulas (SI, AB, NI, OL, AN, MS), pp. 385–396.
PPoPP-2014-Golan-GuetaRSY #automation #semantics: Automatic semantic locking (GGG, GR, MS, EY), pp. 385–386.
CAV-2013-ItzhakyBINS #data type #effectiveness #linked data #open data #reachability #reasoning: Effectively-Propositional Reasoning about Reachability in Linked Data Structures (SI, AB, NI, AN, MS), pp. 756–772.
OOPSLA-2013-TrippKS #nondeterminism #parallel: Turning nondeterminism into parallelism (OT, EK, MS), pp. 589–604.
PLDI-2013-Golan-GuetaRSY #concurrent #library: Concurrent libraries with foresight (GGG, GR, MS, EY), pp. 263–274.
TACAS-2013-LiDDMS #abduction #composition #proving #synthesis: Synthesis of Circular Compositional Program Proofs via Abduction (BL, ID, TD, KLM, MS), pp. 370–384.
ESOP-2012-BurckhardtLFS #consistency #transaction: Eventually Consistent Transactions (SB, DL, MF, MS), pp. 67–86.
ESOP-2012-HawkinsAFRS #reasoning: Reasoning about Lock Placements (PH, AA, KF, MCR, MS), pp. 336–356.
OOPSLA-2012-TamayoABS #behaviour #comprehension #database: Understanding the behavior of database operations under program control (JMT, AA, NGB, MS), pp. 983–996.
PLDI-2012-HawkinsAFRS #concurrent #data transformation #representation #synthesis: Concurrent data representation synthesis (PH, AA, KF, MCR, MS), pp. 417–428.
PLDI-2012-TrippMFS #named #parallel: JANUS: exploiting parallelism via hindsight (OT, RM, JF, MS), pp. 145–156.
POPL-2012-NaikYCS #abstraction #testing: Abstractions from tests (MN, HY, GC, MS), pp. 373–386.
OOPSLA-2011-Golan-GuetaBARSY #automation #using: Automatic fine-grain locking using shape properties (GGG, NGB, AA, GR, MS, EY), pp. 225–242.
OOPSLA-2011-ShachamBASVY #concurrent #testing: Testing atomicity of composed concurrent operations (OS, NGB, AA, MS, MTV, EY), pp. 51–64.
OOPSLA-2011-TrippYFS #data flow #effectiveness #named #parallel: HAWKEYE: effective discovery of dataflow impediments to parallelization (OT, GY, JF, MS), pp. 207–224.
PLDI-2011-DilligDAS #composition #precise #source code #summary: Precise and compact modular procedure summaries for heap manipulating programs (ID, TD, AA, MS), pp. 567–577.
PLDI-2011-HawkinsAFRS #data transformation #representation #synthesis: Data representation synthesis (PH, AA, KF, MCR, MS), pp. 38–49.
FSE-2010-LitvakDBRS #analysis #dependence: Field-sensitive program dependence analysis (SL, ND, RB, NR, MS), pp. 287–296.
ICFP-2010-ArnoldHKBS #matrix #specification #verification: Specifying and verifying sparse matrix codes (GA, JH, ASK, RB, MS), pp. 249–260.
OOPSLA-2010-ItzhakyGIS #induction #synthesis: A simple inductive synthesis methodology and its applications (SI, SG, NI, MS), pp. 36–46.
OOPSLA-2010-LiangTNS #abstraction #evaluation #precise: A dynamic evaluation of the precision of static heap abstractions (PL, OT, MN, MS), pp. 411–427.
SAS-2010-McCloskeyRS #array #invariant: Statically Inferring Complex Heap, Array, and Numeric Invariants (BM, TWR, MS), pp. 71–99.
CAV-2009-McMillanKS #logic: Generalizing DPLL to Richer Logics (KLM, AK, MS), pp. 462–476.
POPL-2009-GulwaniLS #framework: A combination framework for tracking partition sizes (SG, TLA, MS), pp. 239–251.
VMCAI-2009-Sagiv #analysis #thread: Thread-Modular Shape Analysis (MS), p. 3.
CAV-2008-CookGLRS #proving #termination: Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
ESOP-2008-ChawdharyCGSY #abstraction #ranking: Ranking Abstractions (AC, BC, SG, MS, HY), pp. 148–162.
ISSTA-2008-DorLLSW #enterprise #impact analysis #slicing: Customization change impact analysis for erp professionals via program slicing (ND, TLA, SL, MS, DW), pp. 97–108.
SAS-2008-ManevichLSRB #analysis #composition #concurrent: Heap Decomposition for Concurrent Shape Analysis (RM, TLA, MS, GR, JB), pp. 363–377.
CADE-2007-Lev-AmiWRS: Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.
CAV-2007-AmitRRSY #abstraction #comparison #verification: Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
CAV-2007-BallKS #abstraction: Leaping Loops in the Presence of Abstraction (TB, OK, MS), pp. 491–503.
CAV-2007-BogudlovLRS #analysis #parametricity: Revamping TVLA: Making Parametric Shape Analysis Competitive (IB, TLA, TWR, MS), pp. 221–225.
ESOP-2007-RinetzkyPRSY #analysis #composition #encapsulation #source code: Modular Shape Analysis for Dynamically Encapsulated Programs (NR, APH, GR, MS, EY), pp. 220–236.
PLDI-2007-GotsmanBCS #analysis #thread: Thread-modular shape analysis (AG, JB, BC, MS), pp. 266–277.
TACAS-2007-ManevichBCRS #analysis #composition #graph: Shape Analysis by Graph Decomposition (RM, JB, BC, GR, MS), pp. 3–18.
VMCAI-2007-Lev-AmiSIR #analysis: Constructing Specialized Shape Analyses for Uniform Change (TLA, MS, NI, TWR), pp. 215–233.
FoSSaCS-2006-YorshRSMB #linked data #logic #open data: A Logic of Reachable Patterns in Linked Data-Structures (GY, AMR, MS, AM, AB), pp. 94–110.
ISSTA-2006-YorshBS #abstraction #exclamation #proving #testing #theorem proving: Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
SAS-2006-LoginovRS #algorithm #automation #verification: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm (AL, TWR, MS), pp. 261–279.
VMCAI-2006-ArnoldMSS #abstraction #analysis: Combining Shape Analyses by Intersecting Abstractions (GA, RM, MS, RS), pp. 33–48.
PPoPP-2005-ShachamSS #information management #model checking #scalability #using: Scaling model checking of dataraces using dynamic information (OS, MS, AS), pp. 107–118.
SAS-2005-RinetzkySY #analysis #interprocedural #source code: Interprocedural Shape Analysis for Cutpoint-Free Programs (NR, MS, EY), pp. 284–302.
CAV-2017-GrossmanCIRS #equivalence #source code #verification: Verifying Equivalence of Spark Programs (SG, SC, SI, NR, MS), pp. 282–300.
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.
OOPSLA-2018-AlpernasFFRSSW #data flow #information management #using: Secure serverless computing using dynamic information flow control (KA, CF, SF, LR, MS, TS, KW), p. 26.
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-GrossmanAGMRSZ #contract #detection #effectiveness #online: Online detection of effectively callback free objects with applications to smart contracts (SG, IA, GGG, YM, NR, MS, YZ), p. 28.
POPL-2018-PadonHLPSS #first-order #liveness #logic #safety: Reducing liveness to safety in first-order logic (OP, JH, GL, AP, MS, SS), p. 33.
PLDI-2019-GershuniAGNNRRS #kernel #linux #precise #static analysis: Simple and precise static analysis of untrusted Linux kernel extensions (EG, NA, AG, NN, JAN, NR, LR, MS), pp. 1069–1084.
POPL-2020-FeldmanISS #complexity #invariant: Complexity and information in invariant inference (YMYF, NI, MS, SS), p. 29.