Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
Blog
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Publishing
DrugRxiv
Drug Repurposing
Network Medicine
About
REPO4EU
Meet the team
Drug Repurposing Research Collection
Conference
My ScienceOpen
Sign in
Register
Dashboard
Search
46
views
27
references
Top references
cited by
6
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
344
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
FM 2016: Formal Methods
Automated Mutual Explicit Induction Proof in Separation Logic
other
Author(s):
Quang-Trung Ta
,
Ton Chanh Le
,
Siau-Cheng Khoo
,
Wei-Ngan Chin
Publication date
(Online):
November 08 2016
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
Network Medicine
Most cited references
27
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
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
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
Publication date (Print):
2016
Publication date (Online):
November 08 2016
Pages
: 659-676
DOI:
10.1007/978-3-319-48989-6_40
SO-VID:
6f312eb6-5e80-446b-8ec1-fbe27bd8f267
License:
http://www.springer.com/tdm
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. E1
Erratum to: Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
pp. 3
Industrial-Strength Model-Based Testing of Safety-Critical Systems
pp. 25
Counter-Example Guided Program Verification
pp. 43
Tighter Reachability Criteria for Deadlock-Freedom Analysis
pp. 60
Compositional Parameter Synthesis
pp. 69
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
pp. 85
A Model Checking Approach to Discrete Bifurcation Analysis
pp. 102
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
pp. 119
Formal Verification of Multi-Paxos for Distributed Consensus
pp. 137
Validated Simulation-Based Verification of Delayed Differential Dynamics
pp. 155
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
pp. 164
From Electrical Switched Networks to Hybrid Automata
pp. 182
Danger Invariants
pp. 199
Local Planning of Multiparty Interactions with Bounded Horizons
pp. 217
Finding Suitable Variability Abstractions for Family-Based Analysis
pp. 235
Recovering High-Level Conditions from Binary Programs
pp. 254
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
pp. 274
Exploring Model Quality for ACAS X
pp. 291
Learning Moore Machines from Input-Output Traces
pp. 310
Modal Kleene Algebra Applied to Program Correctness
pp. 326
Mechanised Verification Patterns for Dafny
pp. 344
Formalising and Validating the Interface Description in the FMI Standard
pp. 352
An Algebra of Synchronous Atomic Steps
pp. 370
Error Invariants for Concurrent Traces
pp. 388
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor
pp. 406
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
pp. 426
A Generic Logic for Proving Linearizability
pp. 444
Refactoring Refinement Structure of Event-B Machines
pp. 460
Towards Concolic Testing for Hybrid Systems
pp. 479
Explaining Relaxed Memory Models with Program Transformations
pp. 496
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement
pp. 513
Automated Verification of Timed Security Protocols with Clock Drift
pp. 531
Dealing with Incompleteness in Automata-Based Model Checking
pp. 551
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model
pp. 577
Discounted Duration Calculus
pp. 593
Sound and Complete Mutation-Based Program Repair
pp. 612
An Implementation of Deflate in Coq
pp. 628
Decoupling Abstractions of Non-linear Ordinary Differential Equations
pp. 645
Regression Verification for Unbalanced Recursive Functions
pp. 659
Automated Mutual Explicit Induction Proof in Separation Logic
pp. 677
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
pp. 694
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
pp. 702
Approximate Bisimulation and Discretization of Hybrid CSP
pp. 721
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
pp. 741
Model-Based Design of an Energy-System Embedded Controller Using Taste
pp. 748
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
pp. 757
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
pp. 764
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers
pp. 772
Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations
pp. 779
RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions
Similar content
344
Specification and proof in membership equational logic
Authors:
Adel Bouhoula
,
José Meseguer
,
Jean-Pierre Jouannaud
Display to Labeled Proofs and Back Again for Tense Logics
Authors:
Agata Ciabattoni
,
Tim S. Lyon
,
Revantha Ramanayake
…
The role of FGF-2 and BMP-2 in regulation of gene induction, cell proliferation and mineralization
Authors:
Millie Hughes-Fulford
,
Chai-Fei Li
See all similar
Cited by
6
Automating Induction for Solving Horn Clauses
Authors:
Hiroshi Unno
,
Sho Torii
,
Hiroki Sakamoto
Automated Mutual Explicit Induction Proof in Separation Logic
Authors:
Quang-Trung Ta
,
Ton Chanh Le
,
Siau-Cheng Khoo
…
Frame Inference for Inductive Entailment Proofs in Separation Logic
Authors:
Quang Loc Le
,
Jun Sun
,
Shengchao Qin
See all cited by