NFM 2024: 16TH NASA FORMAL METHODS SYMPOSIUM

This page contains an index consisting of author-provided keywords.

A
Abstract Interpretation	Quantitative Input Usage Static Analysis
abstraction	Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
automated software design	Model Refinement
autonomous driving vehicles	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
Autonomous Navigation	SMT-Based Aircraft Conflict Detection and Elimination
B
B method	Validation of Reinforcement Learning Agents and Safety Shields with ProB
Boolean satisfiability	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
C
Capacitated Robots	SMT-Based Dynamic Multi-Robot Task Allocation
CDCL SAT solver	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
Computer Science	Structuring Formal Methods into the Undergraduate Computer Science Curriculum
Conformance Checking	Approximate Conformance Verification of Deep Neural Networks
continuous integration	Integrated Contract-based Unit and System Testing for Component-based Systems
Contract-based design	Contract-driven Runtime Adaptation
contracts	Integrated Contract-based Unit and System Testing for Component-based Systems
control barrier function	The Control Barrier Function Toolbox
control Lyapunov function	The Control Barrier Function Toolbox
control synthesis	Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
coverage analysis	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
cube-and-conquer	Structure-guided Cube-and-conquer for MaxSAT
Curriculum Development	Structuring Formal Methods into the Undergraduate Computer Science Curriculum
Cyber-Physical Systems	Towards formal verification of neural networks in cyber-physical systems SMT-Based Dynamic Multi-Robot Task Allocation Contract-driven Runtime Adaptation Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications
D
Dafny	Verification of Scapegoat Trees using Dafny
Description Logics	Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
distributed programming	Verifying a C implementation of Derecho's coordination mechanism using VST and Coq
E
Evolutionary algorithms	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
F
Formal Methods	Verification of Scapegoat Trees using Dafny SMT-Based Aircraft Conflict Detection and Elimination Towards formal verification of neural networks in cyber-physical systems Structuring Formal Methods into the Undergraduate Computer Science Curriculum
formal model	Validation of Reinforcement Learning Agents and Safety Shields with ProB
formal specification	Model Refinement
formal verification	Verifying a C implementation of Derecho's coordination mechanism using VST and Coq Real Arithmetic in TLAPM Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
function synthesis	Model Refinement
G
Gauss---Seidel method	Formalization of asymptotic convergence for Stationary Iterative Methods
Genetic algorithms	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
H
Hybrid Programs	A Formal Verification Framework for Runtime Assurance
hybrid systems	Real Arithmetic in TLAPM
I
Incremental Solving	SMT-Based Dynamic Multi-Robot Task Allocation
Inductive Invariants	Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
Industrial case study	Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
industry development	Integrated Contract-based Unit and System Testing for Component-based Systems
Initialization problem	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
inprocessing	Structure-guided Cube-and-conquer for MaxSAT
Iterative Convergence	Formalization of asymptotic convergence for Stationary Iterative Methods
J
Jacobi method	Formalization of asymptotic convergence for Stationary Iterative Methods
L
logical properties	Model Refinement
M
Markov Decision Processes	Distributional Probabilistic Model Checking
Metaheuristic	Tackling the polarity initialization problem in SAT solving using a genetic algorithm
metric	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
model-based design	Model Refinement
model-based development	Integrated Contract-based Unit and System Testing for Component-based Systems
Monitor-based verification	Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
monotonicity	Verifying a C implementation of Derecho's coordination mechanism using VST and Coq
Multi-Robot Task Allocation	SMT-Based Dynamic Multi-Robot Task Allocation
N
Neural Network Controlled Systems	Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
Neural Networks	Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems Approximate Conformance Verification of Deep Neural Networks Towards formal verification of neural networks in cyber-physical systems
O
optimization	Structure-guided Cube-and-conquer for MaxSAT
P
Plaidypvs	A Formal Verification Framework for Runtime Assurance
Planning	Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications
PLC program verification	Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
Probabilistic Model Checking	Distributional Probabilistic Model Checking
program synthesis	Model Refinement
Pure-past LTL verification	Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
PVS	A Formal Verification Framework for Runtime Assurance
Q
Quantitative Verification	Quantitative Input Usage Static Analysis
R
Reachability Analysis	Approximate Conformance Verification of Deep Neural Networks
real arithmetic	Real Arithmetic in TLAPM
refinement	Model Refinement
reinforcement learning	Validation of Reinforcement Learning Agents and Safety Shields with ProB
Requirements	Robotics: A New Mission for FRET Requirements
Risk-Aware Verification	Distributional Probabilistic Model Checking
Robotic mission specification	Robotics: A New Mission for FRET Requirements
Robotics	SMT-Based Dynamic Multi-Robot Task Allocation
Runtime adaptation	Contract-driven Runtime Adaptation
Runtime Assurance	A Formal Verification Framework for Runtime Assurance
S
safety	The Control Barrier Function Toolbox
safety shield	Validation of Reinforcement Learning Agents and Safety Shields with ProB
Satisfiability Modulo Theories	SMT-Based Dynamic Multi-Robot Task Allocation
Scapegoat Trees	Verification of Scapegoat Trees using Dafny
scenario classification	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
scenario-based testing	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems
Signal Temporal Logic	Contract-driven Runtime Adaptation Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications
SMT-based Deconfliction	SMT-Based Aircraft Conflict Detection and Elimination
Software Engineering	Structuring Formal Methods into the Undergraduate Computer Science Curriculum
Specification weakening	Contract-driven Runtime Adaptation
Static Analysis	Quantitative Input Usage Static Analysis
Stationary Iterative Methods	Formalization of asymptotic convergence for Stationary Iterative Methods
Structured natural language	Robotics: A New Mission for FRET Requirements
Structured Natural Language specification	Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
symmetry	Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
system design	Model Refinement
T
Teaching and Learning	Structuring Formal Methods into the Undergraduate Computer Science Curriculum
Temporal Conjunctive Queries	Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
temporal logic	Tree-Based Scenario Classification. A Formal Framework for Measuring Domain Coverage when Testing Autonomous Systems Robotics: A New Mission for FRET Requirements
Temporal Logics	Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
testing	Integrated Contract-based Unit and System Testing for Component-based Systems
TLA+	Real Arithmetic in TLAPM
treewidth	Structure-guided Cube-and-conquer for MaxSAT
U
Unmanned Aircraft Systems (UAS) Traffic Management	SMT-Based Aircraft Conflict Detection and Elimination
V
validation	Validation of Reinforcement Learning Agents and Safety Shields with ProB
Verification	Tackling the polarity initialization problem in SAT solving using a genetic algorithm Verification of Scapegoat Trees using Dafny Integrated Contract-based Unit and System Testing for Component-based Systems

Disclaimer | Powered by EasyChair Smart Program