FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program