Josh Berdine

35 papers A* 9A 3B 13C 2Journal 5Unranked 3
YearRankTypeTitle / Venue / Authors
2023 B conf
A General Approach to Under-Approximate Reasoning About Concurrent Programs.
CONCUR
Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn
2022 J jnl
Concurrent incorrectness separation logic.
Proc. ACM Program. Lang.
Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2022 J jnl
Finding real bugs in big programs with incorrectness logic.
Proc. ACM Program. Lang.
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
2020 — conf
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.
CAV (2)
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard
2015 B conf
A Forward Analysis for Recurrent Sets.
SAS
Alexey Bakhirkin, Josh Berdine, Nir Piterman
2015 A conf
Spatial Interpolants.
ESOP
Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
2015 J jnl
Spatial Interpolants.
CoRR
Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid
2014 B conf
Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction.
SAS
Alexey Bakhirkin, Josh Berdine, Nir Piterman
2014 A conf
Computing All Implied Equalities via SMT-Based Partition Refinement.
IJCAR
Josh Berdine, Nikolaj S. Bjørner
2013 B conf
Resourceful Reachability as HORN-LA.
LPAR
Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger
2013 B ed.
Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings
VMCAI
Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni
2012 A* conf
Diagnosing Abstraction Failure for Separation Logic-Based Analyses.
CAV
Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger
2012 J jnl
Verification Condition Generation and Variable Conditions in Smallfoot
CoRR
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2011 B conf
Precision and the Conjunction Rule in Concurrent Separation Logic.
MFPS
Alexey Gotsman, Josh Berdine, Byron Cook
2011 A* conf
SLAyer: Memory Safety for Systems-Level Code.
CAV
Josh Berdine, Byron Cook, Samin Ishtiaq
2010 A* conf
Structuring the verification of heap-manipulating programs.
POPL
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine
2009 B conf
Automatic Verification of Heap Manipulation Using Separation Logic.
SOFSEM
Josh Berdine
2008 C conf
Diagrammatic Reasoning in Separation Logic.
Diagrams
M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine
2008 B conf
Heap Decomposition for Concurrent Shape Analysis.
SAS
Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine
2008 A* conf
Scalable Shape Analysis for Systems Code.
CAV
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
2008 A* conf
Thread Quantification for Concurrent Shape Analysis.
CAV
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv
2007 B conf
Arithmetic Strengthening for Shape Analysis.
SAS
Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
2007 B conf
Local Reasoning for Storable Locks and Threads.
APLAS
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
2007 C conf
Local reasoning about storable locks.
PPDP
Josh Berdine
2007 A conf
Shape Analysis by Graph Decomposition.
TACAS
Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv
2007 A* conf
Shape Analysis for Composite Data Structures.
CAV
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
2007 A* conf
Thread-modular shape analysis.
PLDI
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
2007 A* conf
Variance analyses from invariance analyses.
POPL
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn
2006 A* conf
Automatic Termination Proofs for Programs with Shape-Shifting Heaps.
CAV
Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn
2006 B conf
Interprocedural Shape Analysis with Separated Heap Abstractions.
SAS
Alexey Gotsman, Josh Berdine, Byron Cook
2006 B conf
Strong Update, Disposal, and Encapsulation in Bunched Typing.
MFPS
Josh Berdine, Peter W. O'Hearn
2005 — conf
Smallfoot: Modular Automatic Assertion Checking with Separation Logic.
FMCO
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2005 B conf
Symbolic Execution with Separation Logic.
APLAS
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2004 — conf
A Decidable Fragment of Separation Logic.
FSTTCS
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2002 J jnl
Linear Continuation-Passing.
High. Order Symb. Comput.
Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke