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
30
views
13
references
Top references
cited by
2
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,475
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
NASA Formal Methods
Auto-Active Proof of Red-Black Trees in SPARK
other
Author(s):
Claire Dross
,
Yannick Moy
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
Active Travel Studies
Most cited references
13
Record
: found
Abstract
: not found
Book Chapter
: not found
Dafny: An Automatic Program Verifier for Functional Correctness
K. Rustan M. Leino
(2010)
0
comments
Cited
71
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Why3 — Where Programs Meet Provers
Jean-Christophe Filliâtre
,
Andrei Paskevich
(2013)
0
comments
Cited
39
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Conference Proceedings
: not found
IronFleet
Chris Hawblitzel
,
Jon L. Howell
,
Manos Kapritsos
…
(2015)
0
comments
Cited
23
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2017
Publication date (Online):
April 09 2017
Pages
: 68-83
DOI:
10.1007/978-3-319-57288-8_5
SO-VID:
cd61aa3c-da48-4ea9-8eb9-387356fb15d9
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
2,475
Microstructure and properties of nano-laminated Y3Si2C2 ceramics fabricated via in situ reaction by spark plasma sintering
Authors:
Lin-Kun Shi
,
Xiaobing Zhou
,
Jian-Qing Dai
…
Mechanical and microstructure comparison between microwave and spark plasma sintering of Al–B 4 C composite
Authors:
Ehsan Ghasali
,
Masoud Alizadeh
,
Touradj Ebadzadeh
Effect of pre-chamber enrichment on lean burn pre-chamber spark ignition combustion concept with a narrow-throat geometry
Authors:
See all similar
Cited by
2
Deductive Verification of Unmodified Linux Kernel Library Functions
Authors:
Denis Efremov
,
Mikhail Mandrykin
,
Alexey Khoroshilov
Efficient Verification of Imperative Programs Using Auto2
Authors:
Bohua Zhan
See all cited by