Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
76
views
19
references
Top references
cited by
32
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
4,843
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Scalable Shape Analysis for Systems Code
other
Author(s):
Hongseok Yang
,
Oukseh Lee
,
Josh Berdine
,
Cristiano Calcagno
,
Byron Cook
,
Dino Distefano
,
Peter O’Hearn
Publication date
(Print):
2008
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Software for SAXS correction and analysis
Most cited references
19
Record
: found
Abstract
: not found
Conference Proceedings
: not found
Abstract interpretation
Patrick Cousot
,
Radhia Cousot
(1977)
0
comments
Cited
364
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
A Local Shape Analysis Based on Separation Logic
Dino Distefano
,
Peter O’Hearn
,
Hongseok Yang
(2006)
0
comments
Cited
44
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Symbolic Execution with Separation Logic
Josh Berdine
,
Cristiano Calcagno
,
Peter O’Hearn
(2005)
0
comments
Cited
42
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Pages
: 385-398
DOI:
10.1007/978-3-540-70545-1_36
SO-VID:
3245c1ad-ac7e-45a6-8cfa-a6b49d0b874b
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
Singularity: Designing Better Software (Invited Talk)
pp. 3
Coping with Outside-the-Box Attacks
pp. 5
Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)
pp. 11
Theorem Proving for Verification (Invited Tutorial)
pp. 19
Tutorial on Separation Logic (Invited Tutorial)
pp. 22
Abstract Interpretation with Applications to Timing Validation
pp. 37
Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
pp. 52
Monitoring Atomicity in Concurrent Programs
pp. 66
Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
pp. 80
A Hybrid Type System for Lock-Freedom of Mobile Processes
pp. 94
Implied Set Closure and Its Application to Memory Consistency Verification
pp. 107
Effective Program Verification for Relaxed Memory Models
pp. 121
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
pp. 135
Automated Assume-Guarantee Reasoning by Abstraction Refinement
pp. 149
Local Proofs for Linear-Time Properties of Concurrent Programs
pp. 162
Probabilistic CEGAR
pp. 176
Computing Differential Invariants of Hybrid Systems as Fixedpoints
pp. 190
Constraint-Based Approach for Analysis of Hybrid Systems
pp. 204
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems
pp. 209
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement
pp. 214
Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems
pp. 227
Conflict-Tolerant Features
pp. 240
Ranking Automata and Games for Prioritized Requirements
pp. 254
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
pp. 268
Linear Arithmetic with Stars
pp. 281
Inferring Congruence Equations Using SAT
pp. 294
The Barcelogic SMT Solver
pp. 299
The MathSAT 4 SMT Solver
pp. 304
CSIsat: Interpolation for LA+EUF
pp. 309
Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B
pp. 314
Heap Assumptions on Demand
pp. 328
Proving Conditional Termination
pp. 341
Monotonic Abstraction for Programs with Dynamic Memory Heaps
pp. 355
Enhancing Program Verification with Lemmas
pp. 370
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
pp. 385
Scalable Shape Analysis for Systems Code
pp. 399
Thread Quantification for Concurrent Shape Analysis
pp. 414
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols
pp. 419
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis
pp. 423
Jakstab: A Static Analysis Platform for Binaries
pp. 428
THOR: A Tool for Reasoning about Shape and Arithmetic
pp. 433
Functional Verification of Power Gated Designs by Compositional Reasoning
pp. 446
A Practical Approach to Word Level Model Checking of Industrial Netlists
pp. 459
Validating High-Level Synthesis
pp. 473
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
pp. 487
Application of Formal Word-Level Analysis to Constrained Random Simulation
pp. 491
Producing Short Counterexamples Using “Crucial Events”
pp. 504
Discriminative Model Checking
pp. 517
Correcting a Space-Efficient Simulation Algorithm
pp. 530
Semi-external LTL Model Checking
pp. 543
QMC: A Model Checker for Quantum Systems
pp. 548
T(O)RMC: A Tool for (ω)-Regular Model Checking
pp. 552
Faster Than Uppaal?
Similar content
4,843
Strategies for a scalable multi-robot large scale wire arc additive manufacturing system
Authors:
Alex Arbogast
,
Andrzej Nycz
,
Mark W. Noakes
…
XGBoost: a scalable tree boosting system
Authors:
Chen
,
T CHEN
,
C GUESTRIN
…
A novel features ranking metric with application to scalable visual and bioinformatics data classification
Authors:
Sheng-Quan Zou
,
Jiancang Zeng
,
Liujuan Cao
…
See all similar
Cited by
32
Automating Separation Logic Using SMT
Authors:
Ruzica Piskac
,
Thomas Wies
,
Damien Zufferey
Automated Cyclic Entailment Proofs in Separation Logic
Authors:
James Brotherston
,
Dino Distefano
,
Rasmus Lerchedahl Petersen
SLAyer: Memory Safety for Systems-Level Code
Authors:
Josh Berdine
,
Byron Cook
,
Samin Ishtiaq
See all cited by