Scalable Shape Analysis for Systems Code
From MaRDI portal
Publication:3512506
DOI10.1007/978-3-540-70545-1_36zbMath1155.68359OpenAlexW1508482211MaRDI QIDQ3512506
Cristiano Calcagno, Josh Berdine, Dino Distefano, Hongseok Yang, Oukseh Lee, Byron Cook, Peter W. O'Hearn
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_36
Theory of operating systems (68N25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Verification of heap manipulating programs with ordered data by extended forest automata, Undecidability of Propositional Separation Logic and Its Neighbours, Verifying pointer safety for programs with unknown calls, Separation logics and modalities: a survey, Counterexample Validation and Interpolation-Based Refinement for Forest Automata, An algebraic glimpse at bunched implications and separation logic, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, A divide-and-conquer approach for analysing overlaid data structures, Forest automata for verification of heap manipulation, Predicate extension of symbolic memory graphs for the analysis of memory safety correctness, An array content static analysis based on non-contiguous partitions, Ranking function synthesis for bit-vector relations, Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs, Programs with lists are counter automata, Precision and the Conjunction Rule in Concurrent Separation Logic, Unnamed Item, Automated Cyclic Entailment Proofs in Separation Logic, Access Analysis-Based Tight Localization of Abstract Memories, On Temporal and Separation Logics, Juggrnaut: using graph grammars for abstracting unbounded heap structures, Region Analysis for Race Detection, A Machine-Checked Framework for Relational Separation Logic, Invariants Synthesis over a Combined Domain for Automated Program Verification, Separation Logic Tutorial
Uses Software