Trace Semantics for C++11 Memory Model
The C and C++ languages introduced the relaxed-memory concurrency into the language specification for efficiency purposes in 2011. Trace semantics can provide the mathematical foundation for the proposed C++11 memory model, and there is a lack of ...
SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics
Parameter identifiability is an important aspect of parameter estimation of dynamic system modelling. Several methods exist to determine identifiability of parameter sets using the model definition and analysis of experimental data. There is also the ...
A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems
A calculus for the specification and verification of distributed concurrent interactive real-time systems is introduced. Systems are specified by their interface behavior formalized by interface predicates and interface assertions. System designs in terms ...
Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs
As more end-user applications depend on Internet of Things (IoT) technology, it is essential the networking protocols underpinning these applications are reliable. Using Formal Methods to reason about protocol specifications is an established technique, ...