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
13
views
17
references
Top references
cited by
4
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,007
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
FM 2016: Formal Methods
An Algebra of Synchronous Atomic Steps
other
Author(s):
Ian J. Hayes
,
Robert J. Colvin
,
Larissa A. Meinicke
,
Kirsten Winter
,
Andrius Velykis
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
Atomic Force Microscopy
Most cited references
17
Record
: found
Abstract
: not found
Article
: not found
Calculi for synchrony and asynchrony
Robin Milner
(1983)
0
comments
Cited
93
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Process algebra for synchronous communication
J.A. Bergstra
,
J.W. Klop
(1984)
0
comments
Cited
77
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Kleene algebra with tests
Dexter Kozen
(1997)
0
comments
Cited
64
times
– based on
0
reviews
Review now
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2016
Publication date (Online):
November 08 2016
Pages
: 352-369
DOI:
10.1007/978-3-319-48989-6_22
SO-VID:
91e5354c-8f8c-4163-b27c-85cc64464429
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
1,007
Matrix valued orthogonal polynomials related to SU\((N+1)\), their algebras of differential operators and the corresponding curves
Authors:
F. Alberto Grünbaum
,
Manuel D. De la Iglesia
Inexact iterative numerical linear algebra for neural network-based spectral estimation and rare-event prediction
Authors:
John Strahan
,
Spencer C. Guo
,
Chatipat Lorpaiboon
…
A low-power circuit for piezoelectric vibration control by synchronized switching on voltage sources
Authors:
Hui Shen
,
Jinhao Qiu
,
Hongli Ji
…
See all similar
Cited by
4
Encoding Fairness in a Synchronous Concurrent Program Algebra
Authors:
Ian Hayes
,
Larissa A. Meinicke
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models
Authors:
Robert Colvin
,
Graeme Smith
Completeness and Incompleteness of Synchronous Kleene Algebra
Authors:
Jana Wagemaker
,
Marcello M. Bonsangue
,
Tobias Kappé
…
See all cited by