Linked e-resources
Details
Table of Contents
Requirements and Architectures
Temporal Logic Framework for Performance Analysis of Architectures of Systems
On Implementing Real-time Specification Patterns Using Observers
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems
ARSENAL: Automatic Requirements Specification Extraction from Natural Language
Testing and Run-time Enforcement
Assisted Coverage Closure
Synthesizing Runtime Enforcer of Safety Properties under Burst Error
Compositional Runtime Enforcement
Improving an Industrial Test Generation Tool using SMT Solver
The comKorat Tool: Unified Combinatorial and Constraint-based Generation of Structurally Complex Tests
Theorem Proving and Proofs
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Verifying Relative Safety, Accuracy, and Termination for Program Approximations
A Proof Infrastructure for Binary Programs.-Application of Formal Methods
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
Probabilistic Formal Verification of the SATS Concept of Operation
Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application
Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft
Formal Validation and Verification Framework and Models for Model-Based and Adaptive Control Systems
Code Generation and Synthesis
Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty
Obfuscator Synthesis for Privacy and Utility
Code Generation Using A Formal Model of Reference Counting
EventB2Java: A Code Generator for Event-B
Model Checking and Verification
A Modular Way to Reason About Iteration
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis
Gray-box Learning of Serial Compositions of Mealy Machines
Hierarchical Verification of Quantum Circuits
Correctness and Certification
Semantics for Locking Specifications
From Design Contracts to Component Requirements Verification
A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control.
Temporal Logic Framework for Performance Analysis of Architectures of Systems
On Implementing Real-time Specification Patterns Using Observers
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems
ARSENAL: Automatic Requirements Specification Extraction from Natural Language
Testing and Run-time Enforcement
Assisted Coverage Closure
Synthesizing Runtime Enforcer of Safety Properties under Burst Error
Compositional Runtime Enforcement
Improving an Industrial Test Generation Tool using SMT Solver
The comKorat Tool: Unified Combinatorial and Constraint-based Generation of Structurally Complex Tests
Theorem Proving and Proofs
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Verifying Relative Safety, Accuracy, and Termination for Program Approximations
A Proof Infrastructure for Binary Programs.-Application of Formal Methods
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
Probabilistic Formal Verification of the SATS Concept of Operation
Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application
Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft
Formal Validation and Verification Framework and Models for Model-Based and Adaptive Control Systems
Code Generation and Synthesis
Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty
Obfuscator Synthesis for Privacy and Utility
Code Generation Using A Formal Model of Reference Counting
EventB2Java: A Code Generator for Event-B
Model Checking and Verification
A Modular Way to Reason About Iteration
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis
Gray-box Learning of Serial Compositions of Mealy Machines
Hierarchical Verification of Quantum Circuits
Correctness and Certification
Semantics for Locking Specifications
From Design Contracts to Component Requirements Verification
A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control.