Josh Berdine

According to our database, Josh Berdine authored at least 33 papers between 2002 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

A General Approach to Under-Approximate Reasoning About Concurrent Programs.

Azalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn

Proceedings of the 34th International Conference on Concurrency Theory, 2023

2022

Concurrent incorrectness separation logic.

Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

Proc. ACM Program. Lang., 2022

Finding real bugs in big programs with incorrectness logic.

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

Proc. ACM Program. Lang., 2022

2020

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2015

A Forward Analysis for Recurrent Sets.

Alexey Bakhirkin, Josh Berdine, Nir Piterman

Proceedings of the Static Analysis - 22nd International Symposium, 2015

Spatial Interpolants.

Aws Albarghouthi, Josh Berdine, Byron Cook, Zachary Kincaid

Proceedings of the Programming Languages and Systems, 2015

2014

Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction.

Alexey Bakhirkin, Josh Berdine, Nir Piterman

Proceedings of the Static Analysis - 21st International Symposium, 2014

Computing All Implied Equalities via SMT-Based Partition Refinement.

Josh Berdine, Nikolaj S. Bjørner

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Resourceful Reachability as HORN-LA.

Josh Berdine, Nikolaj S. Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph M. Wintersteiger

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

2012

Verification Condition Generation and Variable Conditions in Smallfoot

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

CoRR, 2012

Diagnosing Abstraction Failure for Separation Logic-Based Analyses.

Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. Wintersteiger

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Precision and the Conjunction Rule in Concurrent Separation Logic.

Alexey Gotsman, Josh Berdine, Byron Cook

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

SLAyer: Memory Safety for Systems-Level Code.

Josh Berdine, Byron Cook, Samin Ishtiaq

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Structuring the verification of heap-manipulating programs.

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

2009

Automatic Verification of Heap Manipulation Using Separation Logic.

Josh Berdine

Proceedings of the SOFSEM 2009: Theory and Practice of Computer Science, 2009

2008

Heap Decomposition for Concurrent Shape Analysis.

Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine

Proceedings of the Static Analysis, 15th International Symposium, 2008

Diagrammatic Reasoning in Separation Logic.

M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine

Proceedings of the Diagrammatic Representation and Inference, 5th International Conference, 2008

Scalable Shape Analysis for Systems Code.

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Thread Quantification for Concurrent Shape Analysis.

Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Shape Analysis by Graph Decomposition.

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Arithmetic Strengthening for Shape Analysis.

Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook

Proceedings of the Static Analysis, 14th International Symposium, 2007

Local reasoning about storable locks.

Josh Berdine

Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2007

Variance analyses from invariance analyses.

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Thread-modular shape analysis.

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Shape Analysis for Composite Data Structures.

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Local Reasoning for Storable Locks and Threads.

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Strong Update, Disposal, and Encapsulation in Bunched Typing.

Josh Berdine, Peter W. O'Hearn

Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, 2006

Interprocedural Shape Analysis with Separated Heap Abstractions.

Alexey Gotsman, Josh Berdine, Byron Cook

Proceedings of the Static Analysis, 13th International Symposium, 2006

Automatic Termination Proofs for Programs with Shape-Shifting Heaps.

Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Smallfoot: Modular Automatic Assertion Checking with Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Symbolic Execution with Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the Programming Languages and Systems, Third Asian Symposium, 2005

2004

A Decidable Fragment of Separation Logic.

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

2002

Linear Continuation-Passing.

Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke

High. Order Symb. Comput., 2002