IFM 2022: 17TH INTERNATIONAL CONFERENCE ON INTEGRATED FORMAL METHODS

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

A
Active Automata Learning	Learning Finite State Models from Recurrent Neural Networks
autonomous grasping	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
B
B Method	Operation Caching and State Compression for Model Checking of High-Level Models
Bitwarden	Verified Password Generation from Password Composition Policies
BPMN	Probabilistic Model Checking of BPMN Processes at Runtime
C
Clock allocation	Untangling the Graphs of Timed Automata to Decrease the Number of Clocks
code contracts	Scalable Typestate Analysis for Low-Latency Environments
concurrent updates	Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
Cooperative Verification	Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Coq	Certified Verification of Relational Properties
coverage criteria	Extending Data Flow Coverage to Test Constraint Refinements
D
data flow analysis	Extending Data Flow Coverage to Test Constraint Refinements
Data protection	A Policy Language to Capture Compliance of Data Protection Requirements
Deductive Program Verification	Formal Specification and Verification of JDK’s Identity Hash Map Implementation
E
EasyCrypt	Verified Password Generation from Password Composition Policies
Event-B	Reachability Analysis and Simulation for Hybridised Event-B Models
experimentation	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
F
Finite State Machines	Learning Finite State Models from Recurrent Neural Networks
formal methods	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
Formal Verification	Reachability Analysis and Simulation for Hybridised Event-B Models Verified Password Generation from Password Composition Policies
formalised requirements	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
G
GDPR	A Policy Language to Capture Compliance of Data Protection Requirements
H
hybrid systems	Reachability Analysis and Simulation for Hybridised Event-B Models
Hyperproperties	HyperPCTL Model Checking by Probabilistic Decomposition
I
Information exchange	Reusing Predicate Precision in Value Analysis
Interactive Theorem Proving	Verified Password Generation from Password Composition Policies
J
Jasmin	Verified Password Generation from Password Composition Policies
Java Modeling Language	Formal Specification and Verification of JDK’s Identity Hash Map Implementation
L
Labelled Transition System	Probabilistic Model Checking of BPMN Processes at Runtime
Linear system	Conservative Time Discretization: A Comparative Study
M
Model checking	Operation Caching and State Compression for Model Checking of High-Level Models
Monitoring	Probabilistic Model Checking of BPMN Processes at Runtime
N
network update problem	Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
P
Password Manager	Verified Password Generation from Password Composition Policies
PCTL	HyperPCTL Model Checking by Probabilistic Decomposition
Petri games	Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
Policy Compliance	A Policy Language to Capture Compliance of Data Protection Requirements
Policy language	A Policy Language to Capture Compliance of Data Protection Requirements
Precision reuse	Reusing Predicate Precision in Value Analysis
Privacy Policies	A Policy Language to Capture Compliance of Data Protection Requirements
probabilistic decomposition	HyperPCTL Model Checking by Probabilistic Decomposition
Probabilistic Model Checking	Probabilistic Model Checking of BPMN Processes at Runtime
R
Random Password Generator	Verified Password Generation from Password Composition Policies
Reachability	Conservative Time Discretization: A Comparative Study
reachability analysis	Reachability Analysis and Simulation for Hybridised Event-B Models
Real-world case study	Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Recurrent Neural Networks	Learning Finite State Models from Recurrent Neural Networks
Relational Verification	Certified Verification of Relational Properties
runtime verification	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
S
Security	Verified Password Generation from Password Composition Policies
simulation	Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
Simulink	Reachability Analysis and Simulation for Hybridised Event-B Models
Software model checking	Reusing Predicate Precision in Value Analysis
Software verification	Reusing Predicate Precision in Value Analysis
State-based formal methods	Operation Caching and State Compression for Model Checking of High-Level Models
static analysis	Scalable Typestate Analysis for Low-Latency Environments
synthesis	Kaki: Concurrent Update Synthesis for Regular Policies via Petri Games
T
testing	Extending Data Flow Coverage to Test Constraint Refinements
Time discretization	Conservative Time Discretization: A Comparative Study
Timed Automata	Untangling the Graphs of Timed Automata to Decrease the Number of Clocks
typestate	Scalable Typestate Analysis for Low-Latency Environments
V
Verifiable Machine Learning	Learning Finite State Models from Recurrent Neural Networks
Verification	Untangling the Graphs of Timed Automata to Decrease the Number of Clocks
Verification Condition Generation	Certified Verification of Relational Properties
Verified Compilation	Verified Password Generation from Password Composition Policies
Verified Data Structure	Formal Specification and Verification of JDK’s Identity Hash Map Implementation
Verified Hash Map	Formal Specification and Verification of JDK’s Identity Hash Map Implementation

Disclaimer | Powered by EasyChair Smart Program