BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Sagiv:Mooly

Facilitated 2 volumes:

POPL 2011Ed
ISMM 2007Ed

Contributed to:

PLDI 20152015
POPL 20152015
PPoPP 20152015
SAS 20152015
CAV 20142014
ESOP 20142014
ISSTA 20142014
PLDI 20142014
POPL 20142014
PPoPP 20142014
CAV 20132013
OOPSLA 20132013
PLDI 20132013
TACAS 20132013
ESOP 20122012
OOPSLA 20122012
PLDI 20122012
POPL 20122012
OOPSLA 20112011
PLDI 20112011
FSE 20102010
ICFP 20102010
OOPSLA 20102010
SAS 20102010
CAV 20092009
POPL 20092009
VMCAI 20092009
CAV 20082008
ESOP 20082008
ISSTA 20082008
SAS 20082008
CADE 20072007
CAV 20072007
ESOP 20072007
PLDI 20072007
TACAS 20072007
VMCAI 20072007
FoSSaCS 20062006
ISSTA 20062006
SAS 20062006
VMCAI 20062006
PPoPP 20052005
SAS 20052005
CAV (2) 20172017
CAV (2) 20192019
OOPSLA 20172017
OOPSLA 20182018
PLDI 20162016
POPL 20162016
PLDI 20182018
POPL 20182018
PLDI 20192019
POPL 20202020

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.