IFM 2020: INTEGRATED FORMAL METHODS

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

A
Active Automata Learning	Grey-Box Learning of Register Automata
Active objects	Active Objects with Deterministic Behaviour
Actors	Active Objects with Deterministic Behaviour
B
B-Method	Fast and Effective Well-Definedness Checking for Formal Models
Boolean satisfiability	Reformulation of SAT into a PolynomialBox-Constrainted Optimization Problem
Bugs	Formal methods for GPGPU programming: is the demand met?
C
Clustering	Clustering-Guided SMT(LRA) Learning
Code generation	Generating SPARK from Event-B Models
complementation	Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata
compliance	Chain of events: Modular Process Models for the Law
Computational Models	Philosophers may Dine - Definitively!
Concurrency	Philosophers may Dine - Definitively!
Confluent	Active Objects with Deterministic Behaviour
Continuous-State Stochastic Systems	Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
Crash-Safety	Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
CUDA	Formal methods for GPGPU programming: is the demand met?
D
dataflow analysis	Detection of Polluting Test Objectives for Dataflow Criteria
dataflow criteria	Detection of Polluting Test Objectives for Dataflow Criteria
declarative process modelling	Chain of events: Modular Process Models for the Law
Deductive verification	A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms
Deterministic behaviour	Active Objects with Deterministic Behaviour
Domain-Specific Language	Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs
DSL	Meeduse: A Tool to Build and Run Proved DSLs
Dynamic Symbolic Execution	Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs
Dynamic Taint Analysis	Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs
E
Event-B	Generating SPARK from Event-B Models An Event-B Based Generic Framework for Hybrid Systems Formal Modelling Fast and Effective Well-Definedness Checking for Formal Models
explicit-state model checking	Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
F
Fix-point theory	Philosophers may Dine - Definitively!
fixed-point arithmetics	Tight Error Analysis in Fixed-point Arithmetics
Floating-point Arithmetic	Automatic Generation of Test Stable Floating Point Code
Formal methods	Formal methods for GPGPU programming: is the demand met? Meeduse: A Tool to Build and Run Proved DSLs
Formal specification	PALM: a technique for Process ALgebraic specification Mining
formal verification	History-based Specification and Verification of Java Collections in KeY Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata Synthesizing clock-efficient timed automata Automatic Generation of Test Stable Floating Point Code
G
generic framework	An Event-B Based Generic Framework for Hybrid Systems Formal Modelling
GPGPU	Formal methods for GPGPU programming: is the demand met?
GPU	Formal methods for GPGPU programming: is the demand met?
Grey-box	Grey-Box Learning of Register Automata
H
hybrid process model	Chain of events: Modular Process Models for the Law
hybrid systems	An Event-B Based Generic Framework for Hybrid Systems Formal Modelling
I
infeasible test objectives	Detection of Polluting Test Objectives for Dataflow Criteria
Interactive Verification	Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
Interface specification	History-based Specification and Verification of Java Collections in KeY
invariants	Algebra-based Loop Synthesis
isomorphism principle	Chain of events: Modular Process Models for the Law
J
Java Web-application Security	Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs
K
KeY	History-based Specification and Verification of Java Collections in KeY
L
law	Chain of events: Modular Process Models for the Law
Linear Temporal Logic	Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
loop synthesis	Algebra-based Loop Synthesis
M
Machine Learning	Clustering-Guided SMT(LRA) Learning
mCRL2	PALM: a technique for Process ALgebraic specification Mining
Model Driven Engineering	Meeduse: A Tool to Build and Run Proved DSLs
Model learning	Grey-Box Learning of Register Automata
Model-Free Policy Synthesis	Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
models of law	Chain of events: Modular Process Models for the Law
multi-threaded software	Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
N
non-linear arithmetic	Algebra-based Loop Synthesis
numerical error analysis	Tight Error Analysis in Fixed-point Arithmetics
numerical solvers	Reformulation of SAT into a PolynomialBox-Constrainted Optimization Problem
O
omega automata	Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata
OpenCL	Formal methods for GPGPU programming: is the demand met?
P
Petri-nets	Meeduse: A Tool to Build and Run Proved DSLs
POSIX-compliant File Systems	Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
process execution	Chain of events: Modular Process Models for the Law
Process mining	PALM: a technique for Process ALgebraic specification Mining
Process-Algebra	Philosophers may Dine - Definitively!
program optimizaton	Algebra-based Loop Synthesis
program transformation	Tight Error Analysis in Fixed-point Arithmetics
R
RALib	Grey-Box Learning of Register Automata
recurrence equations	Algebra-based Loop Synthesis
Refinement	Chain of events: Modular Process Models for the Law Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
refinement and proof	An Event-B Based Generic Framework for Hybrid Systems Formal Modelling
reformulation	Reformulation of SAT into a PolynomialBox-Constrainted Optimization Problem
Register Automata	Grey-Box Learning of Register Automata
Reinforcement Learning	Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
Rodin	Generating SPARK from Event-B Models
Round-off Errors	Automatic Generation of Test Stable Floating Point Code
S
Satisfiability Modulo Theories	Clustering-Guided SMT(LRA) Learning
Separation logic	A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms
Shallow Embedding	Philosophers may Dine - Definitively!
Software Verification	Automatic Generation of Test Stable Floating Point Code
Sorting algorithms	A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-based Sorting Algorithms
SPARK	Generating SPARK from Event-B Models
specifications	Synthesizing clock-efficient timed automata
static analysis	Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion Tight Error Analysis in Fixed-point Arithmetics Synthesizing clock-efficient timed automata Detection of Polluting Test Objectives for Dataflow Criteria
T
Tainting	Grey-Box Learning of Register Automata
TBA1	Verification with Stochastic Games: Advances and Challenges Verifying Parallel and Distributed Systems: The Observer Problem Towards Verified Stochastic Variational Inference for Probabilistic Programs
TBA2	Verification with Stochastic Games: Advances and Challenges Verifying Parallel and Distributed Systems: The Observer Problem Towards Verified Stochastic Variational Inference for Probabilistic Programs
TBA3	Verification with Stochastic Games: Advances and Challenges Verifying Parallel and Distributed Systems: The Observer Problem Towards Verified Stochastic Variational Inference for Probabilistic Programs
test coverage	Detection of Polluting Test Objectives for Dataflow Criteria
Test Stability	Automatic Generation of Test Stable Floating Point Code
Theorem Proving	Automatic Generation of Test Stable Floating Point Code Fast and Effective Well-Definedness Checking for Formal Models
timed automata	Synthesizing clock-efficient timed automata
timed scenarios	Synthesizing clock-efficient timed automata
V
Verification	Formal methods for GPGPU programming: is the demand met?
W
weak memory models	Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
Welcome1	Welcome
Welcome2	Welcome
Welcome3	Welcome
Well-definedness	Fast and Effective Well-Definedness Checking for Formal Models
Write-Back Caching	Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch

Disclaimer | Powered by EasyChair Smart Program