Linked e-resources
Details
Table of Contents
Model checking quantum Markov chains
Bridging Formal Methods and Machine Learning with Global Optimisation
Canonical Narrowing for Variant-based Conditional Rewrite Theories
Modular Analysis of Tree-Topology Models
Non-linear optimization methods for learning regular distributions
Separation of concerning things: a simpler basis for defining and programming with the C\C++ memory model
Creusot: a Foundry for the Deductive Verification of Rust Programs
Generation of a Reversible Semantics for Erlang in Maude
Program slicing techniques with support for unconditional jumps
Formal verification of the inter-core synchronization of a multi-core RTOS kernel
SMT-Based Model Checking of Industrial Simulink Models
PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification
A Formal Methodology for Verifying Side-channel Vulnerabilities in Cache Architectures
Refined Modularization for Bounded Model Checking through Precondition Generation
TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
A Proof System for Cyber-physical Systems with Shared-Variable Concurrency
Theorem proving for Maude specifications using Lean
On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
Declassification predicates for controlled information release
Trace Refinement in B and Event-B
Model Checking B Models via High-level Code Generation
On Probabilistic Extension of The Interaction Theory
Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
RoboCert: Property Specification in Robotics
Formally Verified Animation for RoboChart using Interaction Trees
Machine-checked executable semantics of Stateflow.
Bridging Formal Methods and Machine Learning with Global Optimisation
Canonical Narrowing for Variant-based Conditional Rewrite Theories
Modular Analysis of Tree-Topology Models
Non-linear optimization methods for learning regular distributions
Separation of concerning things: a simpler basis for defining and programming with the C\C++ memory model
Creusot: a Foundry for the Deductive Verification of Rust Programs
Generation of a Reversible Semantics for Erlang in Maude
Program slicing techniques with support for unconditional jumps
Formal verification of the inter-core synchronization of a multi-core RTOS kernel
SMT-Based Model Checking of Industrial Simulink Models
PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification
A Formal Methodology for Verifying Side-channel Vulnerabilities in Cache Architectures
Refined Modularization for Bounded Model Checking through Precondition Generation
TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
A Proof System for Cyber-physical Systems with Shared-Variable Concurrency
Theorem proving for Maude specifications using Lean
On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
Declassification predicates for controlled information release
Trace Refinement in B and Event-B
Model Checking B Models via High-level Code Generation
On Probabilistic Extension of The Interaction Theory
Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
RoboCert: Property Specification in Robotics
Formally Verified Animation for RoboChart using Interaction Trees
Machine-checked executable semantics of Stateflow.