IFM 2019: 15TH INTERNATIONAL CONFERENCE ON INTEGRATED FORMAL METHODS

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

A
Abstractions for execution paths	Visualization and Abstractions for Execution Paths in Model-based Software Testing
Active learning	Learning to reuse: Adaptive model learning for evolving systems
Active objects	Summary of: An Evaluation of Interaction Paradigms for Active Objects
Actor model	Summary of: Dynamic Structural Operational Semantics
alternating refinement	Relating Alternating Relations for Conformance and Refinement
API fuzzing	Fuzzing JavaScript Environment APIs with Interdependent Function Calls
Approximate Computing	Sound Probabilistic Numerical Error Analysis
Assurance Cases	Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
asynchronous methods	Summary of: An Evaluation of Interaction Paradigms for Active Objects
Attack-defense Trees	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
automation	Automated Drawing of Railway Schematics using SAT and optimization
autonomous robotic systems	Summary of: Formal Specification and Verification of Autonomous Robotic Systems
B
B method	Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
Bayesian Inference	HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-based Web Applications
Behavioural model	Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
Bisimulation Metrics	Computing Bisimilarity Metrics for Probabilistic Timed Automata
Boolean satisfiability	SIGmA: GPU Accelerated Simplification of SAT Formulas
C
CENELEC 50128	Using Ontologies in Formal Developments Targeting Certification
Certification of Safety-Critical Systems	Using Ontologies in Formal Developments Targeting Certification
code generation	A Multi-Target Code Generator for High-Level B
completeness	Axiomatic Characterization of Trace Reachability for Concurrent Objects
Component models	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
compositionality	Axiomatic Characterization of Trace Reachability for Concurrent Objects
computation tree logic	Accelerating Parameter Synthesis using Semi-Algebraic Constraints
concurrency	Summary of: An Evaluation of Interaction Paradigms for Active Objects Axiomatic Characterization of Trace Reachability for Concurrent Objects
Concurrency verification	Practical Abstractions for Automated Verification of Message Passing Concurrency
concurrent objects	Summary of: Dynamic Structural Operational Semantics
concurrent programming	Resource Sharing via Capability-Based Multiparty Session Types
Configurable Systems	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
Conformance testing	Asynchronous Testing of Synchronous Components in GALS Systems
Constraint Programming	Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
cooperative scheduling	Summary of: An Evaluation of Interaction Paradigms for Active Objects
Core calculus	Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
Creol	Summary of: Dynamic Structural Operational Semantics
D
Dafny	Dione: A protocol verification system built with Dafny for I/O Automata
Data dependence	A Program Logic For Dependence Analysis
Dataflow	Dynamic Reconfigurations in Frequency Constrained Data Flow
Decidability	Computing Bisimilarity Metrics for Probabilistic Timed Automata
Deductive verification	Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
Delta-oriented programming	Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
Deployment	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
Description Logics	Ontology-Mediated Probabilistic Model Checking
distributed	Summary of: An Evaluation of Interaction Paradigms for Active Objects
Distributed software commissioning	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
Distributed Systems	Dione: A protocol verification system built with Dafny for I/O Automata
dynamic class upgrades	Summary of: Dynamic Structural Operational Semantics
dynamic software updates	Summary of: Dynamic Structural Operational Semantics
dynamical systems	Accelerating Parameter Synthesis using Semi-Algebraic Constraints
Dynamicity	Dynamic Reconfigurations in Frequency Constrained Data Flow
E
Efficiency	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
embedded systems	Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming
experimental evaluation	Evaluation of Program Slicing in Software Verification
F
Featured transition system	Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
Floating-point	Sound Probabilistic Numerical Error Analysis
Formal Document Development	Using Ontologies in Formal Developments Targeting Certification
formal methods	Summary of: Formal Specification and Verification of Autonomous Robotic Systems A Multi-Target Code Generator for High-Level B An integrated approach to a combinatorial optimisation problem Asynchronous Testing of Synchronous Components in GALS Systems
Formal Methods in Interdisciplinary Settings	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
Formal modeling and specification	Visualization and Abstractions for Execution Paths in Model-based Software Testing
Formal specification	Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
formal specification and verification	Summary of: Formal Specification and Verification of Autonomous Robotic Systems
Formal verification	Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
Formalization and proof of properties	Dynamic Reconfigurations in Frequency Constrained Data Flow
futures	Summary of: An Evaluation of Interaction Paradigms for Active Objects
G
GALS system	Asynchronous Testing of Synchronous Components in GALS Systems
graph-based	Fuzzing JavaScript Environment APIs with Interdependent Function Calls
Graphical Security Models	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
H
high-level	A Multi-Target Code Generator for High-Level B
I
incremental SAT	Automated Drawing of Railway Schematics using SAT and optimization
Industrial case study	Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
Input/Output Automaton	Dione: A protocol verification system built with Dafny for I/O Automata
Integrated Formal Methods	Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
interaction mechanisms	Summary of: An Evaluation of Interaction Paradigms for Active Objects
interface automata	Relating Alternating Relations for Conformance and Refinement
ioco	Relating Alternating Relations for Conformance and Refinement
Isabelle/DOF	Using Ontologies in Formal Developments Targeting Certification
Isabelle/HOL	An integrated approach to a combinatorial optimisation problem Using Ontologies in Formal Developments Targeting Certification Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
J
JavaScript	Fuzzing JavaScript Environment APIs with Interdependent Function Calls
L
Liveness	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
M
Mealy machines	Learning to reuse: Adaptive model learning for evolving systems
Message passing	Practical Abstractions for Automated Verification of Message Passing Concurrency
Modal transition system	Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
Model checking	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System Asynchronous Testing of Synchronous Components in GALS Systems Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
Model of Computation	Dynamic Reconfigurations in Frequency Constrained Data Flow
Model validation	Dynamic Reconfigurations in Frequency Constrained Data Flow
Model-based software testing	Visualization and Abstractions for Execution Paths in Model-based Software Testing
Model-based Testing	HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-based Web Applications
modular SOS	Summary of: Dynamic Structural Operational Semantics
multi-GPU computing	SIGmA: GPU Accelerated Simplification of SAT Formulas
N
numerical optimization	Automated Drawing of Railway Schematics using SAT and optimization
O
object-orientation	Summary of: Dynamic Structural Operational Semantics
Operational semantics	Summary of: Dynamic Structural Operational Semantics
optimisation	An integrated approach to a combinatorial optimisation problem
P
Parallel SAT Preprocessing	SIGmA: GPU Accelerated Simplification of SAT Formulas
parameter synthesis	Accelerating Parameter Synthesis using Semi-Algebraic Constraints
Path coverage visualization	Visualization and Abstractions for Execution Paths in Model-based Software Testing
Petri nets	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
Probabilistic Analysis	Sound Probabilistic Numerical Error Analysis
Probabilistic Model Checking	Ontology-Mediated Probabilistic Model Checking
Probabilistic systems	HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-based Web Applications
Probabilistic Timed Automata	Computing Bisimilarity Metrics for Probabilistic Timed Automata
Process algebra	Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System Practical Abstractions for Automated Verification of Message Passing Concurrency
program slicing	Evaluation of Program Slicing in Software Verification
program synthesis	Axiomatic Characterization of Trace Reachability for Concurrent Objects
Program verification	A Program Logic For Dependence Analysis
Proteus	Summary of: Dynamic Structural Operational Semantics
Q
Quantitative Analysis	Ontology-Mediated Probabilistic Model Checking Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
Quantitative Security	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
R
railway signalling	Automated Drawing of Railway Schematics using SAT and optimization
Reactive system	Learning to reuse: Adaptive model learning for evolving systems
Real-time	Dynamic Reconfigurations in Frequency Constrained Data Flow
S
Safety	Integrated Model-checking for the Design of Safe and Efficient Distributed Software Commissioning
Safety-critical systems	Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
SAT Decomposition	SIGmA: GPU Accelerated Simplification of SAT Formulas
Saturation-based Theorem Prover	Interactive Visualization of Saturation Attempts in Vampire
schematic drawing	Automated Drawing of Railway Schematics using SAT and optimization
semi-algebraic sets	Accelerating Parameter Synthesis using Semi-Algebraic Constraints
semi-automatic formal verification	Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming
Separation logic	Practical Abstractions for Automated Verification of Message Passing Concurrency
Service-based Systems	HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-based Web Applications
session types	Resource Sharing via Capability-Based Multiparty Session Types
sharing	Resource Sharing via Capability-Based Multiparty Session Types
SMT	Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
SMT solvers	An integrated approach to a combinatorial optimisation problem
Software evolution	Learning to reuse: Adaptive model learning for evolving systems
Software product line analysis	Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
Software reuse	Learning to reuse: Adaptive model learning for evolving systems
software verification	Evaluation of Program Slicing in Software Verification
Statechart	Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
Static analysis	A Program Logic For Dependence Analysis
Statistical Model Checking	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
Synchronous programming	Asynchronous Testing of Synchronous Components in GALS Systems
systems	Summary of: An Evaluation of Interaction Paradigms for Active Objects
T
template-based	A Multi-Target Code Generator for High-Level B
Theorem Proving	Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
Tools for Formal Methods	Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
type safety	Summary of: Dynamic Structural Operational Semantics
U
uioco	Relating Alternating Relations for Conformance and Refinement
Uncertainty Quantification	HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-based Web Applications
Unifying Theories of Programming	Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
uniqueness types	Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming
V
Vampire	Interactive Visualization of Saturation Attempts in Vampire
Variability	Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
Visualization	Interactive Visualization of Saturation Attempts in Vampire

Disclaimer | Powered by EasyChair Smart Program