FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

A
abstract interpretation	Software Safety and Security and AI
Abstraction	Towards `Verifying' a Water Treatment System
Actor	Deadlock Detection for Actor-based Coroutines
actors	SDN-Actors: Modeling and Verification of SDN Programs
air traffic surveillance systems	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
algebraic effects	Modular Verification of Programs with Effects and Effect Handlers in Coq
alloy	CompoSAT: Specification-Guided Coverage for Model Finding
approximate partial order reduction	Approximate Partial Order Reduction
architecture	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
assumptions refinement	A Weakness Measure for GR(1) Formulae
auto-generated code	Verifying Auto-Generated C Code from Simulink
automatic verification	Compositional Reasoning for Shared-variable Concurrent Programs
automotive	Verifying Auto-Generated C Code from Simulink
Automotive case study	Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Autonomous automotive	Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
avionics systems	Model-Based Testing for Avionics Systems
B
Barrier Certificates	Vector Barrier Certificates and Comparison Systems
C
C code	Verifying Auto-Generated C Code from Simulink
Case study	Verifying Auto-Generated C Code from Simulink
channel composition	An Algebraic Approach for Reasoning About Information Flow
code review	Evidential and Continuous Integration of Software Verification Tools
comparison systems	Vector Barrier Certificates and Comparison Systems
Complexity	Timed Vacuity
composition	Modular Verification of Programs with Effects and Effect Handlers in Coq
compositional model checking	To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
compositional reasoning	Compositional Reasoning for Shared-variable Concurrent Programs
concurrency	Operational Semantics of a Weak Memory Model with Channel Synchronization
Concurrent datatypes	View abstraction for systems with component identities
concurrent program algebra	Encoding fairness in a synchronous concurrent program algebra
continuous systems	Vector Barrier Certificates and Comparison Systems
controller synthesis	Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Cooperative Scheduling	Deadlock Detection for Actor-based Coroutines
Coq	Modular Verification of Programs with Effects and Effect Handlers in Coq
counter-example	Producing Explanations for Rich Logics
crowds	An Algebraic Approach for Reasoning About Information Flow
Cyber-Physical system	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems Towards `Verifying' a Water Treatment System
cyber-physical systems	Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
D
Deadlock	A lightweight deadlock analysis technique of object-oriented programs
Deadlock Detection	Deadlock Detection for Actor-based Coroutines Dynamic Symbolic Verification of MPI Programs
Decentralized planning	Multi-Robot LTL Planning Under Uncertainty
Decidability	The Compound Interest in Relaxing Punctuality
declarative programming	Variant Analysis with QL
distributed concurrent systems	SDN-Actors: Modeling and Verification of SDN Programs
distributed systems	Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
Dynamic Logic	The Compound Interest in Relaxing Punctuality
Dynamic Verification	Dynamic Symbolic Verification of MPI Programs
E
Embedded systems	Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
epistemic logic	Timed Epistemic Knowledge Bases for Social Networks
evidential verification	Evidential and Continuous Integration of Software Verification Tools
explanation	Producing Explanations for Rich Logics
explanatory analysis	To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
F
fairness	Encoding fairness in a synchronous concurrent program algebra
Fault tolerance	Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
first-order logic	Formal Specification and Verification of Dynamic Parametrized Architectures
floating-point analysis	Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point optimization	Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point round-off errors	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Formal Methods	Disruptive Innovations for the Development and the Deployment of Fault-Free Software Z3 and SMT in Industrial R&D From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems CompoSAT: Specification-Guided Coverage for Model Finding The Compound Interest in Relaxing Punctuality
formal methods in practice	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
formal specification	Formal Specification and Verification of Dynamic Parametrized Architectures
formal verification	Interlocking Design Automation using Prover Trident Formal Specification and Verification of Dynamic Parametrized Architectures Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations Verifying Auto-Generated C Code from Simulink
Frama-C	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
free monad	Modular Verification of Programs with Effects and Effect Handlers in Coq
FSM	FSM Inference from Long Traces
G
g-leakage	An Algebraic Approach for Reasoning About Information Flow
Gappa	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Generalized Reactivity	A Weakness Measure for GR(1) Formulae
H
hardware verification	Modular Verification of Programs with Effects and Effect Handlers in Coq
hardware-in-the-loop	Model-Based Testing for Avionics Systems
Highly Assured Software	From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
hydraulic oil pump	Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
I
Importance Splitting	Statistical Model Checking of LLVM Code
industrial case	Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
industrial impact	20 Years of "Real" Real-Time Model Checking
inference	FSM Inference from Long Traces
information flow	Formal Specification and Verification of Dynamic Parametrized Architectures
Integrated Development Environment	QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
integrated verification	Evidential and Continuous Integration of Software Verification Tools
Integration	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
Interlocking	Interlocking Design Automation using Prover Trident
K
Knowledge based Reasoning	Timed Epistemic Knowledge Bases for Social Networks
L
lams	A lightweight deadlock analysis technique of object-oriented programs
LLVM	Statistical Model Checking of LLVM Code
logic	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
logic programming	Variant Analysis with QL
M
memory model	Operational Semantics of a Weak Memory Model with Channel Synchronization
Message Passing Interface	Dynamic Symbolic Verification of MPI Programs
Model Animation	From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
model checking	20 Years of "Real" Real-Time Model Checking SDN-Actors: Modeling and Verification of SDN Programs IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems Verifying Auto-Generated C Code from Simulink Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE View abstraction for systems with component identities Producing Explanations for Rich Logics
model finding	CompoSAT: Specification-Guided Coverage for Model Finding
Model learning	Towards `Verifying' a Water Treatment System
model-based engineering	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
model-based testing	Model-Based Testing for Avionics Systems
model-checking	Timed Vacuity
modular approach	Modular Verification of Programs with Effects and Effect Handlers in Coq
mu-calculus	Producing Explanations for Rich Logics
Multi-Robot planning	Multi-Robot LTL Planning Under Uncertainty
O
object-oriented	Object-Oriented Security Proofs
Object-oriented programs	A lightweight deadlock analysis technique of object-oriented programs
omega-languages	A Weakness Measure for GR(1) Formulae
Online Social Networks	Timed Epistemic Knowledge Bases for Social Networks
OpenFlow	SDN-Actors: Modeling and Verification of SDN Programs
operational semantics	Operational Semantics of a Weak Memory Model with Channel Synchronization A wide-spectrum language for verification of programs on weak memory models
ordinary differential equations	Vector Barrier Certificates and Comparison Systems
P
Parameterised verification problem	View abstraction for systems with component identities
parametrized systems	Formal Specification and Verification of Dynamic Parametrized Architectures
Partial models	Multi-Robot LTL Planning Under Uncertainty
partial order reduction	SDN-Actors: Modeling and Verification of SDN Programs
Predicate Abstraction	Deadlock Detection for Actor-based Coroutines
Privacy	Timed Epistemic Knowledge Bases for Social Networks
Program Analysis	Variant Analysis with QL
proofs	Object-Oriented Security Proofs
Prover Trident	Interlocking Design Automation using Prover Trident
PVS	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Q
quantifier elimination	Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Quantitative Analysis	QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
quantitative information flow	An Algebraic Approach for Reasoning About Information Flow
R
railway interlocking systems	Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
RAISE	Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
Rare Event Simulation	Statistical Model Checking of LLVM Code
reachability analysis	Approximate Partial Order Reduction
real-time logic TCTL	Timed Vacuity
refinement	Compositional Reasoning for Shared-variable Concurrent Programs
regular expressions	The Compound Interest in Relaxing Punctuality
Reinforcement Learning	Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
Reliable	Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
rely-guarantee	Compositional Reasoning for Shared-variable Concurrent Programs
Rely/guarantee concurrency	Encoding fairness in a synchronous concurrent program algebra
Requirement Analysis	From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
Requirements specification	Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Resource-aware	Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
rich logic	Producing Explanations for Rich Logics
Robustness guided falsification	Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
roundoff error	Combining Tools for Optimization and Analysis of Floating-Point Computations
S
Safety	Software Safety and Security and AI
safety critical	Disruptive Innovations for the Development and the Deployment of Fault-Free Software
safety properties	Compositional Reasoning for Shared-variable Concurrent Programs
safety verification	Approximate Partial Order Reduction Vector Barrier Certificates and Comparison Systems
SAT solver	FSM Inference from Long Traces
Security	Object-Oriented Security Proofs Variant Analysis with QL Software Safety and Security and AI Modular Verification of Programs with Effects and Effect Handlers in Coq
sensitivity analysis	Approximate Partial Order Reduction
shared-variable concurrent programs	Compositional Reasoning for Shared-variable Concurrent Programs
Sign-off	Interlocking Design Automation using Prover Trident
Simulink	Verifying Auto-Generated C Code from Simulink
Simulink-based development	Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
SMT	Z3 and SMT in Industrial R&D
SMT-based model checking	Formal Specification and Verification of Dynamic Parametrized Architectures
software development	Disruptive Innovations for the Development and the Deployment of Fault-Free Software
Software Engineering	Z3 and SMT in Industrial R&D
Software Product Lines	QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
software verification	A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm Modular Verification of Programs with Effects and Effect Handlers in Coq
software-defined networks	SDN-Actors: Modeling and Verification of SDN Programs
specification	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
state space minimisation	To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
Static program analysis	Software Safety and Security and AI
Statistical Model Checking	Statistical Model Checking of LLVM Code QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
stepwise development	Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE
Symmetry reduction	View abstraction for systems with component identities
synchronizations	A lightweight deadlock analysis technique of object-oriented programs
system architectures	Formal Specification and Verification of Dynamic Parametrized Architectures
T
theorem proving	Z3 and SMT in Industrial R&D
threads	A lightweight deadlock analysis technique of object-oriented programs
timed systems	The Compound Interest in Relaxing Punctuality
Tool paper	QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
transition system	Deadlock Detection for Actor-based Coroutines Approximate Partial Order Reduction
type system	A lightweight deadlock analysis technique of object-oriented programs
U
Uncertain planning	Multi-Robot LTL Planning Under Uncertainty
Unmanned Aircraft Systems	From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
UPPAAL	20 Years of "Real" Real-Time Model Checking
V
vacuity	Timed Vacuity
variant analysis	Variant Analysis with QL
vector Lyapunov functions	Vector Barrier Certificates and Comparison Systems
Verification	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems Towards `Verifying' a Water Treatment System
view	IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
View abstraction	View abstraction for systems with component identities
W
weak memory models	A wide-spectrum language for verification of programs on weak memory models
weakness	A Weakness Measure for GR(1) Formulae
Weighted timed automata	Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
wide-spectrum language	A wide-spectrum language for verification of programs on weak memory models

Disclaimer | Powered by EasyChair Smart Program