Scalable Shape Analysis for Systems Code
From MaRDI portal
Publication:3512506
DOI10.1007/978-3-540-70545-1_36zbMath1155.68359MaRDI 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
68N25: Theory of operating systems
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Separation logics and modalities: a survey, Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs, Unnamed Item, Automated Cyclic Entailment Proofs in Separation Logic, Separation Logic Tutorial, Precision and the Conjunction Rule in Concurrent Separation Logic, Verification of heap manipulating programs with ordered data by extended forest automata, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Programs with lists are counter automata, Verifying pointer safety for programs with unknown calls, An array content static analysis based on non-contiguous partitions, Juggrnaut: using graph grammars for abstracting unbounded heap structures, Predicate extension of symbolic memory graphs for the analysis of memory safety correctness, Ranking function synthesis for bit-vector relations, A divide-and-conquer approach for analysing overlaid data structures, Forest automata for verification of heap manipulation, Invariants Synthesis over a Combined Domain for Automated Program Verification, Counterexample Validation and Interpolation-Based Refinement for Forest Automata, Access Analysis-Based Tight Localization of Abstract Memories, A Machine-Checked Framework for Relational Separation Logic, Undecidability of Propositional Separation Logic and Its Neighbours, Region Analysis for Race Detection
Uses Software
