FM 2015: FORMAL METHODS 2015

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

A
Abstract interpretation	Narrowing operators on template abstract domains
abstraction	Abstraction of Elementary Hybrid Systems by Variable Transformation
Acceleration	Proving Safety with Trace Automata and Bounded Model Checking
Alloy	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification Static Differential Program Analysis for Software-Defined Networks
Analysis Operations	The Semantics of Cardinality-based Feature Models via Formal Languages
Android	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Android Frameworks	Using Real-Time Maude to Model Check Energy Consumption Behavior
Android security	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
architectures	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Assume-Guarantee Reasoning	Automated Circular Assume-Guarantee Reasoning
auto-active verification	A Fully Verified Container Library
automated theorem proving	Typed First-Order Logic
automated verification	Certified Reasoning with Infinity
axiomatisation	Typed First-Order Logic
B
B-method	Model-Based Problem Solving for University Timetable Validation and Improvement
BB84 quantum key distribution	QPMC: A Model Checker for Quantum Programs and Protocols
biological systems	Parameter Synthesis through Temporal Logic Specifications
biometric systems	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Bitvectors	Proving Safety with Trace Automata and Bounded Model Checking
bounded model checking	Property-Driven Fence Insertion using Reorder Bounded Model Checking Proving Safety with Trace Automata and Bounded Model Checking
C
camkes	Automated Verification of RPC Stub Code
Cardinality-based Feature Models	The Semantics of Cardinality-based Feature Models via Formal Languages
Certificates	Certificates for Parameterized Model Checking
Certification	Certificates for Parameterized Model Checking
certified decision procedure	Certified Reasoning with Infinity
Circular Assume-Guarantee Reasoning	Automated Circular Assume-Guarantee Reasoning
completeness proof	Typed First-Order Logic
component platform verification	Automated Verification of RPC Stub Code
Compositional Verification	Verifying the Safety of a Flight-Critical System Automated Circular Assume-Guarantee Reasoning
Concurrency	Verifying Opacity of a Transactional Mutex Lock Towards Formal Verification of Orchestration Computations Using the K Framework
constraint programming	Model-Based Problem Solving for University Timetable Validation and Improvement
container library	A Fully Verified Container Library
continuous systems	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
correctness criteria for shared memory	A framework for correctness criteria on weak memory models
Counterexample	Counterexamples for Expected Rewards
cryptography	QPMC: A Model Checker for Quantum Programs and Protocols
D
Data Flow Graphs	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
DCR Graphs	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Decidability	The Semantics of Cardinality-based Feature Models via Formal Languages
declarative process modelling	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Distribution Bisimulation	Probabilistic Bisimulation for Realistic Schedulers
dynamic sub processes	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
E
elementary function	Abstraction of Elementary Hybrid Systems by Variable Transformation
Energy Consumption	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
eventuality	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Expected Reward	Counterexamples for Expected Rewards
F
fence insertion	Property-Driven Fence Insertion using Reorder Bounded Model Checking
Firewall	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Floating-point	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Formal Languages	The Semantics of Cardinality-based Feature Models via Formal Languages
formal methods	Typed First-Order Logic
Formal Modeling	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Formal Semantics	Towards Formal Verification of Orchestration Computations Using the K Framework
Formal verification	Counterexamples for Expected Rewards Semantics-Preserving Simplification of Real-World Firewall Rule Sets Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Freeze Quantifier	Using Real-Time Maude to Model Check Energy Consumption Behavior
full functional correctness	A Fully Verified Container Library
G
Global Optimization	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
H
hybrid system	Abstraction of Elementary Hybrid Systems by Variable Transformation
hybrid systems	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
I
Inductive invariants	Certificates for Parameterized Model Checking
interdisciplinarity	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
invariant	Abstraction of Elementary Hybrid Systems by Variable Transformation
Isabelle	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
J
Java	A Specification Language for Static and Runtime Verification of Data and Control Properties
JML	A Specification Language for Static and Runtime Verification of Data and Control Properties
K
K Framework	Towards Formal Verification of Orchestration Computations Using the K Framework
Kerberos V	Verifying Parameterized Timed Security Protocols
KeY	A Specification Language for Static and Runtime Verification of Data and Control Properties
KIV Theorem Prover	Verifying Opacity of a Transactional Mutex Lock
L
LARVA	A Specification Language for Static and Runtime Verification of Data and Control Properties
Linear Temporal Logic	Using Real-Time Maude to Model Check Energy Consumption Behavior
linear temporal logics	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
Linearizability	A framework for correctness criteria on weak memory models
M
Markov Chain	Counterexamples for Expected Rewards
Model Checking	Verifying the Safety of a Flight-Critical System QPMC: A Model Checker for Quantum Programs and Protocols Automated Circular Assume-Guarantee Reasoning Certificates for Parameterized Model Checking
Multi-Constraint	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
N
Narrowing	Narrowing operators on template abstract domains
netfilter iptables	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Network security management	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
O
object-orientation	A Fully Verified Container Library
Opacity	Verifying Opacity of a Transactional Mutex Lock
operating system security	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
Orc	Towards Formal Verification of Orchestration Computations Using the K Framework
ordinary differential equations	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
P
parameter synthesis	Parameter Synthesis through Temporal Logic Specifications
Parameterised Protocol	Verifying Parameterized Timed Security Protocols
Parameterized systems	Certificates for Parameterized Model Checking
Permission-model	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
privacy by design	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Probabilistic Automata	Probabilistic Bisimulation for Realistic Schedulers
Probabilistic Model	Counterexamples for Expected Rewards
process-aware information systems	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
program verification	Towards Formal Verification of Orchestration Computations Using the K Framework Typed First-Order Logic
property-driven	Property-Driven Fence Insertion using Reorder Bounded Model Checking
Q
quantum computation tree logic QCTL	QPMC: A Model Checker for Quantum Programs and Protocols
quantum Markov chain	QPMC: A Model Checker for Quantum Programs and Protocols
R
reachability analysis	Parameter Synthesis through Temporal Logic Specifications
Realistic Schedulers	Probabilistic Bisimulation for Realistic Schedulers
Regular Expressions	The Semantics of Cardinality-based Feature Models via Formal Languages
reorder bounded model checking	Property-Driven Fence Insertion using Reorder Bounded Model Checking
Round-off Error Analysis	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
run-time refinement	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
runtime verification	A Specification Language for Static and Runtime Verification of Data and Control Properties Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
S
safety and liveness	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Safety verification	Verifying the Safety of a Flight-Critical System
SAT Solver	Automated Circular Assume-Guarantee Reasoning
scheduling	Model-Based Problem Solving for University Timetable Validation and Improvement
Secrecy	Verifying Parameterized Timed Security Protocols
Security Protocol Verification	Verifying Parameterized Timed Security Protocols
sel4	Automated Verification of RPC Stub Code
Semantics	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Service Orchestration	Towards Formal Verification of Orchestration Computations Using the K Framework
SMT solvers	Certificates for Parameterized Model Checking
Software Transactional Memory	Verifying Opacity of a Transactional Mutex Lock
Software Verification	Proving Safety with Trace Automata and Bounded Model Checking
software-defined networks	Static Differential Program Analysis for Software-Defined Networks
specification	Certified Reasoning with Infinity
Static Analysis	A Specification Language for Static and Runtime Verification of Data and Control Properties Narrowing operators on template abstract domains
static differential analysis	Static Differential Program Analysis for Software-Defined Networks
STL	Parameter Synthesis through Temporal Logic Specifications
Stochastic Model	Counterexamples for Expected Rewards
superdense coding	QPMC: A Model Checker for Quantum Programs and Protocols
T
Throughput	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Timed Authentication	Verifying Parameterized Timed Security Protocols
Timed Automata	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Timed Protocol	Verifying Parameterized Timed Security Protocols
timetabling	Model-Based Problem Solving for University Timetable Validation and Improvement
Trace automata	Proving Safety with Trace Automata and Bounded Model Checking
Transactional Mutex Lock	Verifying Opacity of a Transactional Mutex Lock
TSO	A framework for correctness criteria on weak memory models
Turing completeness	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
typed logic	Typed First-Order Logic
U
UPPAAL	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
V
variable transformation	Abstraction of Elementary Hybrid Systems by Variable Transformation
Verification	Verifying Opacity of a Transactional Mutex Lock Abstraction of Elementary Hybrid Systems by Variable Transformation
verified data structures	A Fully Verified Container Library
Vulnerability Analysis	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
W
Weak memory models	A framework for correctness criteria on weak memory models
Weighted Timed Automaton	Using Real-Time Maude to Model Check Energy Consumption Behavior

Disclaimer | Powered by EasyChair Smart Program