Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
28
views
13
references
Top references
cited by
3
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
1,972
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
NASA Formal Methods
SPEN: A Solver for Separation Logic
other
Author(s):
Constantin Enea
,
Ondřej Lengál
,
Mihaela Sighireanu
,
Tomáš Vojnar
Publication date
(Online):
April 09 2017
Publisher:
Springer International Publishing
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
ScienceOpen Research
Most cited references
13
Record
: found
Abstract
: not found
Book Chapter
: not found
Local Reasoning about Programs that Alter Data Structures
Peter O’Hearn
,
John Reynolds
,
Hongseok Yang
(2001)
0
comments
Cited
52
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
A Decidable Fragment of Separation Logic
Josh Berdine
,
Cristiano Calcagno
,
Peter O’Hearn
(2004)
0
comments
Cited
34
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Automated verification of shape, size and bag properties via user-defined predicates in separation logic
Shengchao Qin
,
Wei-Ngan Chin
,
Cristina David
…
(2012)
0
comments
Cited
31
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2017
Publication date (Online):
April 09 2017
Pages
: 302-309
DOI:
10.1007/978-3-319-57288-8_22
SO-VID:
ee20fd74-4fa3-4cd0-97f1-662fef678fe1
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 1
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data
pp. 19
Learning from Faults: Mutation Testing in Active Automata Learning
pp. 35
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption
pp. 52
Multi-timed Bisimulation for Distributed Timed Automata
pp. 68
Auto-Active Proof of Red-Black Trees in SPARK
pp. 84
Analysing Security Protocols Using Refinement in iUML-B
pp. 99
On Learning Sparse Boolean Formulae for Explaining AI Decisions
pp. 115
Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets
pp. 131
Model-Counting Approaches for Nonlinear Numerical Constraints
pp. 139
Input Space Partitioning to Enable Massively Parallel Proof
pp. 146
Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations
pp. 163
Modular Model-Checking of a Byzantine Fault-Tolerant Protocol
pp. 178
Improved Learning for Stochastic Timed Models by State-Merging Algorithms
pp. 194
Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
pp. 212
A Relational Shape Abstract Domain
pp. 230
Floating-Point Format Inference in Mixed-Precision
pp. 247
A Verification Technique for Deterministic Parallel Programs
pp. 265
Systematic Predicate Abstraction Using Variable Roles
pp. 282
specgen: A Tool for Modeling Statecharts in CSP
pp. 288
HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis
pp. 295
Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino
pp. 302
SPEN: A Solver for Separation Logic
pp. 310
From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case
pp. 327
Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function
pp. 342
Reasoning About Safety-Critical Information Flow Between Pilot and Computer
pp. 357
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
pp. 373
Verifying a Class of Certifying Distributed Programs
pp. 389
Compact Proof Witnesses
pp. 404
Qualification of a Model Checker for Avionics Software Verification
pp. 420
SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements
pp. 427
Just Formal Enough? Automated Analysis of EARS Requirements
Similar content
1,972
Clinical Nutrition University nutrition in the prevention and management of irritable bowel syndrome, constipation and diverticulosis. e-SPEN Eur E J Clin Nutr
Authors:
E CABRE
Handgrip strength and adductor pollicis muscle thickness as predictors of postoperative complications after major operations of the gastrointestinal tract e-SPEN, Eur e-J Clin Nutr
Authors:
R Bragagnolo
,
FS Caporossi
,
DB Dock-Nascimento
…
Frantz's tumour, solid pseudopapillary epithelial neoplasm (SPEN)
Authors:
Orapin Tanapanpanit
,
Samornmas Kanngurn
,
Krit Pongpirul
See all similar
Cited by
3
Effective Entailment Checking for Separation Logic with Inductive Definitions
Authors:
Jens Katelaan
,
Christoph Matheja
,
Florian Zuleger
Local Reasoning for Global Graph Properties
Authors:
Siddharth Krishna
,
Alexander J. Summers
,
Thomas Wies
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)
Authors:
Siddharth Krishna
,
Dennis Shasha
,
Thomas Wies
See all cited by