FM 2019: 23RD INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

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

A
Abstract Execution	Abstract Execution
Abstract Java Programs	Abstract Execution
active automata learning	L*-Based Learning of Markov Decision Processes
Approximation hardness	How Hard is Finding Shortest Counter-Example Lassos in Model Checking?
Architecture Verification	APML: An Architecture Proof Modelling Language
ARM Cortex-M	Formal Semantics Extraction from Natural Language Specifications for ARM
automata	Generic Partition Refinement and Weighted Tree Automata
Automata over infinite words	Learning Deterministic Variable Automata over Infinite Alphabets
Automatic Theorem Proving	Abstract Execution
B
Behavioral Specification Language	GOSPEL - Providing OCaml with a Formal Specification Language
Bisimulations	Compositional Verication of Concurrent Systems by Combining Bisimulations
blockchain	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Boolean network	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
Büchi automata	How Hard is Finding Shortest Counter-Example Lassos in Model Checking?
C
Canonical form for automata	Learning Deterministic Variable Automata over Infinite Alphabets
capacity	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Certification	Unification in Matching Logic
Chord	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Circus	Circus2CSP: A Tool for Model-Checking Circus Using FDR Towards a Model-Checker for Circus
coalgebra	Generic Partition Refinement and Weighted Tree Automata
Component-based modeling	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Compositional verification	Compositional Verication of Concurrent Systems by Combining Bisimulations
concolic testing	Concolic Testing Heap-Manipulating Programs
concurrency	Value-Dependent Information-Flow Security on Weak Memory Models
Concurrent data structures	Verifying Correctness of Persistent Concurrent Data Structures
Concurrent Reactive Systems	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
concurrent stochastic games	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Consistency	Local Consistency Check in Synchronous Dataflow Models
Continuous invariants	Pegasus: A Framework for Sound Continuous Invariant Generation
Control theory	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
Coq	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
correctness	On the Nature of Symbolic Execution
Counterexamples	Counterexample-Driven Synthesis for Probabilistic Program Sketches
csp	Circus2CSP: A Tool for Model-Checking Circus Using FDR Towards a Model-Checker for Circus
cyber-physical systems	Pegasus: A Framework for Sound Continuous Invariant Generation
D
Data Minimization	Gray-Box Monitoring of Hyperproperties
data structures	Concolic Testing Heap-Manipulating Programs
Database queries and updates	Reasoning Formally about Database Queries and Updates
Dataflow	Local Consistency Check in Synchronous Dataflow Models
Deductive Reasoning	Abstract Execution
Deep Neural Networks	Star-Based Reachability Analysis of Deep Neural Networks
derivative-free numerical optimization	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Deterministic Variable Automata	Learning Deterministic Variable Automata over Infinite Alphabets
differential dynamic logic	An Axiomatic Approach to Liveness for Differential Equations
differential equations	An Axiomatic Approach to Liveness for Differential Equations
discrete event simulation	Synthesis of Railway Signaling Layout from Local Capacity Specifications
distributed protocol	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
Domain-specific language	Reasoning Formally about Database Queries and Updates
Durable linearizability	Verifying Correctness of Persistent Concurrent Data Structures
Dynamic Symbolic Execution	Formal Semantics Extraction from Natural Language Specifications for ARM
E
embedding	Embedding High-Level Formal Specifications into Applications
Events	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
F
FACTum	APML: An Architecture Proof Modelling Language
FDR	Circus2CSP: A Tool for Model-Checking Circus Using FDR Towards a Model-Checker for Circus
finite-precision	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
floating-point programs	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Formal methods	Embedding High-Level Formal Specifications into Applications Gray-Box Monitoring of Hyperproperties Reasoning Formally about Database Queries and Updates
formal verification	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Frama-C	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
G
game theory	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Gene regulatory network	Controlling Large Boolean Networks with Temporary and Permanent Perturbations
geo-fencing	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Guarded logic	Reasoning Formally about Database Queries and Updates
H
heap-manipulating programs	Concolic Testing Heap-Manipulating Programs
high-level data races	Static Analysis for Detecting High-Level Races in RTOS Kernels
Hybrid Systems	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Hyperproperties	Gray-Box Monitoring of Hyperproperties
I
incremental SAT	Synthesis of Railway Signaling Layout from Local Capacity Specifications
information-flow security	Value-Dependent Information-Flow Security on Weak Memory Models
interactive	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Interactive Theorem Proving	APML: An Architecture Proof Modelling Language Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
interrupt-driven programs	Static Analysis for Detecting High-Level Races in RTOS Kernels
invariant generation	Pegasus: A Framework for Sound Continuous Invariant Generation
IoT Malware	Formal Semantics Extraction from Natural Language Specifications for ARM
Isabelle	APML: An Architecture Proof Modelling Language
Isabelle/HOL	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
K
Kalman filters	Quantitative Verification of Numerical Stability for Kalman Filters
L
L^*	Learning Deterministic Variable Automata over Infinite Alphabets
Language Integration	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Learning automata	Learning Deterministic Variable Automata over Infinite Alphabets
Linear-Temporal Logic	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
liveness	An Axiomatic Approach to Liveness for Differential Equations
liveness proof	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
M
markov chain	Generic Partition Refinement and Weighted Tree Automata
Markov Chains	Counterexample-Driven Synthesis for Probabilistic Program Sketches
Markov decision processes	L*-Based Learning of Markov Decision Processes
Matching Logic	Unification in Matching Logic
Model checking	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games Counterexample-Driven Synthesis for Probabilistic Program Sketches Learning Deterministic Variable Automata over Infinite Alphabets How Hard is Finding Shortest Counter-Example Lassos in Model Checking? Compositional Verication of Concurrent Systems by Combining Bisimulations
model inference	L*-Based Learning of Markov Decision Processes
model-checking	Circus2CSP: A Tool for Model-Checking Circus Using FDR Towards a Model-Checker for Circus
Modular Verification	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Monitoring	Gray-Box Monitoring of Hyperproperties
N
Nash equilibria	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Natural Language Processing	Formal Semantics Extraction from Natural Language Specifications for ARM
non-quantitative analysis	SOA and the Button Problem
Non-volatile memory	Verifying Correctness of Persistent Concurrent Data Structures
O
object-orientation	On the Nature of Symbolic Execution
OCaml	GOSPEL - Providing OCaml with a Formal Specification Language
Omega-automata	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
on-the-fly synthesis	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Operating Systems Verification	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
ordinary differential equations	Pegasus: A Framework for Sound Continuous Invariant Generation
P
Parameter adaptation and subsumption	Abstraction and Subsumption in Modular Verification of C Programs
parameterized verification	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
partition refinement	Generic Partition Refinement and Weighted Tree Automata
Persistence	Verifying Correctness of Persistent Concurrent Data Structures
point-in-polygon algorithm	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
ProB	Embedding High-Level Formal Specifications into Applications
Probabilistic Model Checking	Quantitative Verification of Numerical Stability for Kalman Filters From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Probabilistic Programming	Counterexample-Driven Synthesis for Probabilistic Program Sketches
probabilistic verification	Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games
Program Sketches	Counterexample-Driven Synthesis for Probabilistic Program Sketches
Program verification	Abstraction and Subsumption in Modular Verification of C Programs GOSPEL - Providing OCaml with a Formal Specification Language
programming language design	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
Prototype Verification System	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
Q
Quantitative verification	Quantitative Verification of Numerical Stability for Kalman Filters
R
railway signaling	Synthesis of Railway Signaling Layout from Local Capacity Specifications
Reachability Analysis	Star-Based Reachability Analysis of Deep Neural Networks
Reactive synthesis	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
refactoring	SOA and the Button Problem
Refactoring Verification	Abstract Execution
refinement	Circus2CSP: A Tool for Model-Checking Circus Using FDR Towards a Model-Checker for Circus Verifying Correctness of Persistent Concurrent Data Structures
Rely-guarantee	A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems
Robustness of Neural Networks	Star-Based Reachability Analysis of Deep Neural Networks
roundoff error	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
RTOS kernel	Static Analysis for Detecting High-Level Races in RTOS Kernels
run-time execution	Embedding High-Level Formal Specifications into Applications
Runtime Verification	Gray-Box Monitoring of Hyperproperties
S
Safety Verification	Star-Based Reachability Analysis of Deep Neural Networks
Semantics Extraction	Formal Semantics Extraction from Natural Language Specifications for ARM
separation logic	Concolic Testing Heap-Manipulating Programs GOSPEL - Providing OCaml with a Formal Specification Language
service-oriented architecture	SOA and the Button Problem
smart contract verification	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain
SMT oracle	Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions
Specification languages	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
specification-based testing	Concolic Testing Heap-Manipulating Programs
stabilization proof	Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
static analysis	Static Analysis for Detecting High-Level Races in RTOS Kernels
Symbolic Execution	On the Nature of Symbolic Execution Abstract Execution
Symbolic fixed-point algorithms	GR(1)*: GR(1) Specifications Extended with Existential Guarantees
Synchronous dataflow	Local Consistency Check in Synchronous Dataflow Models
Syntactic unification	Unification in Matching Logic
synthesis	Synthesis of Railway Signaling Layout from Local Capacity Specifications
T
Time-Critical Systems	Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
tool	Circus2CSP: A Tool for Model-Checking Circus Using FDR
transition system	On the Nature of Symbolic Execution
transition systems	Generic Partition Refinement and Weighted Tree Automata
U
Unambiguous Büchi automata	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Unification	Unification in Matching Logic
unstable tests	Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
V
value-dependent security	Value-Dependent Information-Flow Security on Weak Memory Models
Verification	Learning Deterministic Variable Automata over Infinite Alphabets Verifying Correctness of Persistent Concurrent Data Structures
Verified Software Toolchain	Abstraction and Subsumption in Modular Verification of C Programs
Very-weak alternating automata	From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
W
weak memory models	Value-Dependent Information-Flow Security on Weak Memory Models
Weakest preconditions	Reasoning Formally about Database Queries and Updates
weighted tree automata	Generic Partition Refinement and Weighted Tree Automata

Disclaimer | Powered by EasyChair Smart Program