BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Denmark
1 × Korea
1 × Poland
1 × Portugal
1 × United Kingdom
2 × France
2 × Germany
2 × Spain
5 × USA
Collaborated with:
B.Cook D.Distefano P.W.O'Hearn A.Bakhirkin N.Piterman M.Sagiv R.Manevich S.Ishtiaq A.Gotsman N.Bjørner T.Lev-Ami G.Ramalingam A.Nanevski V.Vafeiadis H.Yang C.Calcagno A.Albarghouthi Z.Kincaid A.Cox C.M.Wintersteiger S.Magill E.M.Clarke S.Sagiv G.Ramalingam A.Chawdhary O.Lee T.Wies
Talks about:
analysi (10) shape (9) heap (4) abstract (3) analys (3) decomposit (2) structur (2) approxim (2) program (2) concurr (2)

Person: Josh Berdine

DBLP DBLP: Berdine:Josh

Facilitated 1 volumes:

VMCAI 2013Ed

Contributed to:

ESOP 20152015
SAS 20152015
IJCAR 20142014
SAS 20142014
CAV 20122012
CAV 20112011
POPL 20102010
CAV 20082008
SAS 20082008
CAV 20072007
PLDI 20072007
POPL 20072007
PPDP 20072007
SAS 20072007
TACAS 20072007
CAV 20062006
SAS 20062006

Wrote 18 papers:

Spatial Interpolants (AA, JB, BC, ZK), pp. 634–660.
SAS-2015-BakhirkinBP #analysis #set
A Forward Analysis for Recurrent Sets (AB, JB, NP), pp. 293–311.
IJCAR-2014-BerdineB #refinement #smt
Computing All Implied Equalities via SMT-Based Partition Refinement (JB, NB), pp. 168–183.
SAS-2014-BakhirkinBP #abstraction #analysis #approximate
Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction (AB, JB, NP), pp. 34–50.
CAV-2012-BerdineCIW #abstraction #analysis
Diagnosing Abstraction Failure for Separation Logic-Based Analyses (JB, AC, SI, CMW), pp. 155–173.
CAV-2011-BerdineCI #memory management #named #safety
SLAyer: Memory Safety for Systems-Level Code (JB, BC, SI), pp. 178–183.
POPL-2010-NanevskiVB #source code #verification
Structuring the verification of heap-manipulating programs (AN, VV, JB), pp. 261–274.
CAV-2008-BerdineLMRS #analysis #concurrent #quantifier #thread
Thread Quantification for Concurrent Shape Analysis (JB, TLA, RM, GR, SS), pp. 399–413.
CAV-2008-YangLBCCDO #analysis #scalability
Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.
SAS-2008-ManevichLSRB #analysis #composition #concurrent
Heap Decomposition for Concurrent Shape Analysis (RM, TLA, MS, GR, JB), pp. 363–377.
CAV-2007-BerdineCCDOWY #analysis #data type
Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
PLDI-2007-GotsmanBCS #analysis #thread
Thread-modular shape analysis (AG, JB, BC, MS), pp. 266–277.
POPL-2007-BerdineCCDO #analysis
Variance analyses from invariance analyses (JB, AC, BC, DD, PWO), pp. 211–224.
PPDP-2007-Berdine #reasoning
Local reasoning about storable locks (JB), p. 153.
SAS-2007-MagillBCC #analysis
Arithmetic Strengthening for Shape Analysis (SM, JB, EMC, BC), pp. 419–436.
TACAS-2007-ManevichBCRS #analysis #composition #graph
Shape Analysis by Graph Decomposition (RM, JB, BC, GR, MS), pp. 3–18.
CAV-2006-BerdineCDO #automation #proving #source code #termination
Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
SAS-2006-GotsmanBC #abstraction #analysis #interprocedural
Interprocedural Shape Analysis with Separated Heap Abstractions (AG, JB, BC), pp. 240–260.

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.