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
58
views
27
references
Top references
cited by
13
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
6,440
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
Thread Quantification for Concurrent Shape Analysis
other
Author(s):
J. Berdine
,
T. Lev-Ami
,
R. Manevich
,
G. Ramalingam
,
M. Sagiv
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
Core Readings in Statistical Mediation Analysis
Most cited references
27
Record
: found
Abstract
: not found
Article
: not found
Linearizability: a correctness condition for concurrent objects
Maurice P. Herlihy
,
Jeannette Wing
(1990)
0
comments
Cited
273
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Parametric shape analysis via 3-valued logic
Mooly Sagiv
,
Thomas Reps
,
Reinhard Wilhelm
(2002)
0
comments
Cited
107
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Verifying properties of parallel programs: an axiomatic approach
Susan Owicki
,
David Gries
(1976)
0
comments
Cited
54
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Pages
: 399-413
DOI:
10.1007/978-3-540-70545-1_37
SO-VID:
4fef3ae0-fd8b-4cca-937f-ba27fc6b858f
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
6,440
Thread, read, rewind, repeat: towards using nanopores for protein sequencing
Authors:
Aleksei Aksimentiev
Microfluidic thread-based electrode system to detect glucose and acetylthiocholine.
Authors:
Michelle Gaines
,
Maria José González-Guerrero
,
Kathryn M. Uchida
…
Subcortical lesions after transient thread occlusion in the rat: T2-weighted magnetic resonance imaging findings without corresponding sensorimotor deficits.
Authors:
Susanne Wegener
,
Mathias Hoehn
,
Korinna Kandal
…
See all similar
Cited by
13
Scalable Shape Analysis for Systems Code
Authors:
Hongseok Yang
,
Oukseh Lee
,
Josh Berdine
…
Automatically Proving Linearizability
Authors:
Viktor Vafeiadis
Shape-Value Abstraction for Verifying Linearizability
Authors:
Viktor Vafeiadis
See all cited by