FM 2016: 21ST INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

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

A
aadl	Model-Based Design of an Energy-System Embedded Controller using Taste
Abstract domains	Recovering high-level conditions from binary programs
Abstract Interpretation	Finding Suitable Variability Abstractions for Family-Based Analysis
Abstraction	Refactoring Refinement Structures of Event-B Machines Decoupled simulating abstractions of non-linear ordinary differential equations
amortized cost	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
approximate bisimilar	Approximate Bisimulation and Discretization of Hybrid CSP
Atomicity Violation	Error Invariants for Concurrent Traces
Automata learning	Learning Moore Machines from Input-Output Traces
automotive systems	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
B
Barrier certificates	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
battery-aware scheduling	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
bifurcation analysis	A Model Checking Approach to Discrete Bifurcation Analysis
Binary code	Recovering high-level conditions from binary programs
binary x86 analysis	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
bound analysis	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
Bounded Model Checking	Equivalence Checking of a Floating-point Unit Against a High-level C Model
C
C11	Explaining Relaxed Memory Models with Program Transformations
Case-splitting	Equivalence Checking of a Floating-point Unit Against a High-level C Model
clock drifting	Automated Verification of Timed Security Protocols with Clock Drift
Co-simulation	Formalising and Validating the Interface Description in the FMI standard
Code generation	Formalising and Validating the Interface Description in the FMI standard
collision avoidance	Exploring Model Quality for ACAS X
Combinatorial testing	Formalising and Validating the Interface Description in the FMI standard
compositionality	Compositional Parameter Synthesis
Compression	An Implementation of Deflate in Coq
Concurrency	Error Invariants for Concurrent Traces Explaining Relaxed Memory Models with Program Transformations
concurrency theory	An algebra of synchronous atomic steps
Concurrent Systems	Tighter Reachability Criteria for Deadlock-Freedom Analysis
confidence interval	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
continuous systems	Decoupled simulating abstractions of non-linear ordinary differential equations
Coq	An Implementation of Deflate in Coq SpecCert: Specifying and Verifying Hardware-based Security Enforcement Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
correctness	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
cost analysis	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
Counter-example guided refinement	Counter-Example Guided Program Verification
CSP	Tighter Reachability Criteria for Deadlock-Freedom Analysis
cyber-physical systems	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
D
Darboux polynomials	Decoupled simulating abstractions of non-linear ordinary differential equations
Data Race	Error Invariants for Concurrent Traces
deadlock	Tighter Reachability Criteria for Deadlock-Freedom Analysis State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Deadlock-freedom	Tighter Reachability Criteria for Deadlock-Freedom Analysis
decoupling	Decoupled simulating abstractions of non-linear ordinary differential equations
Delay Differential Equations (DDEs)	Validated Simulation-Based Verification of Delayed Differential Dynamics
Differential-algebraic equations	From Electrical Switched Networks to Hybrid Automata
discounting	Discounted Duration Calculus
discretization	Approximate Bisimulation and Discretization of Hybrid CSP
Distributed Algorithms	Formal Verification of Multi-Paxos for Distributed Consensus
Distributed Real-Time Systems	Local Planning of Multiparty Interactions with Bounded Horizons
duration calculus	Discounted Duration Calculus
Dynamic logic	Modal Kleene Algebra Applied to Program Correctness
dynamic programming	Exploring Model Quality for ACAS X
dynamical systems	Validated Simulation-Based Verification of Delayed Differential Dynamics A Model Checking Approach to Discrete Bifurcation Analysis
E
Electrical switched networks	From Electrical Switched Networks to Hybrid Automata
embedded systems	Model-Based Design of an Energy-System Embedded Controller using Taste
energy	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Entailment checking	Automated Mutual Explicit Induction Proof in Separation Logic
entropy	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Equivalence Checking	Equivalence Checking of a Floating-point Unit Against a High-level C Model
Error Invariants	Error Invariants for Concurrent Traces
Event-B	Refactoring Refinement Structures of Event-B Machines
F
Fault Explanation	Error Invariants for Concurrent Traces
Fault Localization	Error Invariants for Concurrent Traces
Finite Model Finding	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
First-Order Logic	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Floating-point Design	Equivalence Checking of a Floating-point Unit Against a High-level C Model
formal methods	Sound and Complete Mutation-Based Program Repair Automated Verification of Timed Security Protocols with Clock Drift
Formal model	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Formal Model Driven Design	Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
formal specification	Model-Based Design of an Energy-System Embedded Controller using Taste
Formal Specification and Verification	Formal Verification of Multi-Paxos for Distributed Consensus
formal verification	An Implementation of Deflate in Coq RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions Equivalence Checking of a Floating-point Unit Against a High-level C Model A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Functional Mock-up Interface	Formalising and Validating the Interface Description in the FMI standard
G
GPU	GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
H
hardware	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Hardware RTL Model	Equivalence Checking of a Floating-point Unit Against a High-level C Model
Hazards	Error Invariants for Concurrent Traces
HCSP	Approximate Bisimulation and Discretization of Hybrid CSP
High-level structure recovery	Recovering high-level conditions from binary programs
hybrid method	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
hybrid systems	Towards Concolic Testing for Hybrid Systems From Electrical Switched Networks to Hybrid Automata A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems Decoupled simulating abstractions of non-linear ordinary differential equations Approximate Bisimulation and Discretization of Hybrid CSP
Hypervisor	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
I
Imprecise	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Incomplete	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Incomplete Model Checking	Dealing with Incompleteness in Automata-based Model Checking
Incremental Verification	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations Dealing with Incompleteness in Automata-based Model Checking
Industry experience	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Interpolation	Refactoring Refinement Structures of Event-B Machines
Interrupt	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers
invariant	Danger Invariants
invariants	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
ISA	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
K
kinetic battery model	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Kleene algebras	Modal Kleene Algebra Applied to Program Correctness
Knowledge	Local Planning of Multiparty Interactions with Bounded Horizons
L
LEON3	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Linear programming relaxation	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Linearizability	A Generic Logic for Proving Linearizability
Logic of Equality of Uninterpreted Functions	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
lower bounds	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
M
machine learning	Exploring Model Quality for ACAS X Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Mathematical Induction	Automated Mutual Explicit Induction Proof in Separation Logic
Mechanized Reasoning	Formal Verification of Multi-Paxos for Distributed Consensus
model	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
model checking	Discounted Duration Calculus A Model Checking Approach to Discrete Bifurcation Analysis GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
model-based design	Model-Based Design of an Energy-System Embedded Controller using Taste
Model-based testing	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Model-Checking	Counter-Example Guided Program Verification
models	Exploring Model Quality for ACAS X
Moore machines	Learning Moore Machines from Input-Output Traces
MPI	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Multifunction Vehicle Bus controller	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
mutation testing	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
mutual information	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
N
Non-blocking concurrent algorithms	A Generic Logic for Proving Linearizability
non-interference	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
O
on-the-fly verification of regulations	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
ordinary differential equations	Decoupled simulating abstractions of non-linear ordinary differential equations
P
parameterised verification	Automated Verification of Timed Security Protocols with Clock Drift
parametric timed automata	Compositional Parameter Synthesis
partial-order methods	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Power/ARM	Explaining Relaxed Memory Models with Program Transformations
Predicate transformers	Modal Kleene Algebra Applied to Program Correctness
Process Algebra	Tighter Reachability Criteria for Deadlock-Freedom Analysis
program equivalence	Regression Verification for unbalanced recursive functions
Program Extraction	An Implementation of Deflate in Coq
Program Families	Finding Suitable Variability Abstractions for Family-Based Analysis
program repair	Sound and Complete Mutation-Based Program Repair
program transformations	Explaining Relaxed Memory Models with Program Transformations
Program verification	Modal Kleene Algebra Applied to Program Correctness Mechanised Verification Patterns for Dafny
proof	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Proof Patterns	Mechanised Verification Patterns for Dafny
proof-rules	Regression Verification for unbalanced recursive functions
R
railway infrastructure designs	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
random testing	Towards Concolic Testing for Hybrid Systems
Reachability analysis	Tighter Reachability Criteria for Deadlock-Freedom Analysis
real-time control systems	Model-Based Design of an Energy-System Embedded Controller using Taste
Refactoring	Refactoring Refinement Structures of Event-B Machines
Refinement	Refactoring Refinement Structures of Event-B Machines
regression-verification	Regression Verification for unbalanced recursive functions
rely/guarantee concurrency	An algebra of synchronous atomic steps
renewable-energy systems	Model-Based Design of an Energy-System Embedded Controller using Taste
reversible instructions	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
RPNI	Learning Moore Machines from Input-Output Traces
rule-based modelling	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
S
Safety analysis	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Safety Properties	Counter-Example Guided Program Verification
Safety Requirement	Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
SAT and SMT solvers	Sound and Complete Mutation-Based Program Repair
SAT formula	Equivalence Checking of a Floating-point Unit Against a High-level C Model
SAT solving	Tighter Reachability Criteria for Deadlock-Freedom Analysis
satellite	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Satisfiability Modulo Theories	From Electrical Switched Networks to Hybrid Automata
sdl	Model-Based Design of an Energy-System Embedded Controller using Taste
security	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Semantically-correct static analysis	Recovering high-level conditions from binary programs
Separation Logic	A Generic Logic for Proving Linearizability Automated Mutual Explicit Induction Proof in Separation Logic
Sequentialization	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers
Simulink	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Slicing	Error Invariants for Concurrent Traces
SMT Solvers	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
software	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
solar energy	Model-Based Design of an Energy-System Embedded Controller using Taste
SPARCv8	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
state space exploration algorithms	GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
state-space reduction	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
static analysis	Danger Invariants
statistical estimation	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
statistical model checking	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Step-wise development	Dealing with Incompleteness in Automata-based Model Checking
stirling engine	Model-Based Design of an Energy-System Embedded Controller using Taste
symbolic execution	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions Towards Concolic Testing for Hybrid Systems Equivalence Checking of a Floating-point Unit Against a High-level C Model
synchronous process algebra	An algebra of synchronous atomic steps
synthesis	Compositional Parameter Synthesis Danger Invariants
system modelling	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
T
Tactic language	Mechanised Verification Patterns for Dafny
taste	Model-Based Design of an Energy-System Embedded Controller using Taste
temporal logic	Discounted Duration Calculus
testing	Exploring Model Quality for ACAS X
timed automata	Discounted Duration Calculus Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems Local Planning of Multiparty Interactions with Bounded Horizons
timed security protocol	Automated Verification of Timed Security Protocols with Clock Drift
tools	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
TSO	Explaining Relaxed Memory Models with Program Transformations
U
Untimed Software Model	Equivalence Checking of a Floating-point Unit Against a High-level C Model
UPPAAL SMC	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
upper bounds	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
V
Validated Numerical Methods	Validated Simulation-Based Verification of Delayed Differential Dynamics
Variability-Aware Static Analysis	Finding Suitable Variability Abstractions for Family-Based Analysis
VDM-SL	Formalising and Validating the Interface Description in the FMI standard
verification	Exploring Model Quality for ACAS X An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Verification by Simulation	Validated Simulation-Based Verification of Delayed Differential Dynamics
Verification of concurrent program	Counter-Example Guided Program Verification
W
weak memory models	Explaining Relaxed Memory Models with Program Transformations

Disclaimer | Powered by EasyChair Smart Program