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
39
views
22
references
Top references
cited by
9
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,954
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
Enhancing Program Verification with Lemmas
other
Author(s):
Huu Hai Nguyen
,
Wei-Ngan Chin
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
De Gruyter Materials Science: Energy
Most cited references
22
Record
: found
Abstract
: not found
Book
: not found
Isabelle/HOL
Tobias Nipkow
,
Markus Wenzel
,
Lawrence Paulson
(2002)
0
comments
Cited
199
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Conference Proceedings
: not found
Separation logic: a logic for shared mutable data structures
J.C. Reynolds
(2024)
0
comments
Cited
81
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
All references
Author and book information
Book Chapter
Pages
: 355-369
DOI:
10.1007/978-3-540-70545-1_34
SO-VID:
774938ca-01b7-43cf-858e-fa71f8231c70
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
2,954
BEAK LIKE SPIKELET1 is required for lateral development of lemma and palea in rice
Authors:
X Ma
,
Z. CHENG
,
F WU
…
Drinfeld's lemma for perfectoid spaces and overconvergence of multivariate \((\varphi, \Gamma)\)-modules
Authors:
Gergely Zábrádi
,
Annie Carter
,
Kiran Kedlaya
Distance holomorphic mappings and the Schwarz lemma
Authors:
Shoshichi Kobayashi
See all similar
Cited by
9
The Tree Width of Separation Logic with Recursive Definitions
Authors:
Radu Iosif
,
Adam Rogalewicz
,
Jiri Simacek
A Generic Cyclic Theorem Prover
Authors:
James Brotherston
,
Nikos Gorogiannis
,
Rasmus L Petersen
Automated Cyclic Entailment Proofs in Separation Logic
Authors:
James Brotherston
,
Dino Distefano
,
Rasmus Lerchedahl Petersen
See all cited by