FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

A
Active Objects	Detecting Deadlocks in Formal System Models with Condition Synchronization
Android Applications	Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
B
Backward exploration ·	Backward reachability analysis for timed automata with data variables
C
classical B	Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
compositional analysis of software systems	Using SMT engine to generate Symbolic Automata
Compositional verification	A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Condition Synchronization	Detecting Deadlocks in Formal System Models with Condition Synchronization
Consistency Analysis	Analyzing Consistency of Formal Requirements
contract-based verification	Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Coq	Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
critical software assurance	Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Critical Systems	Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems
Cyclic proofs	An Entailment Checker for Separation Logic with Inductive Definitions
D
Deadlock Analysis	Detecting Deadlocks in Formal System Models with Condition Synchronization
Dependency	Detecting Deadlocks in Formal System Models with Condition Synchronization
F
Formal Methods	Analyzing Consistency of Formal Requirements Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
formal proof	Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
formal verification	Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems
I
ic3	A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
inductive definitions	An Entailment Checker for Separation Logic with Inductive Definitions
infinite descent	An Entailment Checker for Separation Logic with Inductive Definitions
Interlocking	A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Internet of Things	Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems
M
memory isolation	Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
model checking	Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
N
networks of synchronized automata	Using SMT engine to generate Symbolic Automata
nuxmv	A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
O
Ocra	A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
P
protokernel	Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
R
reachability analysis	Backward reachability analysis for timed automata with data variables
Requirements Engineering	Analyzing Consistency of Formal Requirements
Rule-Based Programming	Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
S
Security Management	Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
separation logic	An Entailment Checker for Separation Logic with Inductive Definitions
SMT Solver	Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
software formal verification	Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Software-Defined Networking	Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
symbolic behavioral semantics	Using SMT engine to generate Symbolic Automata
T
Timed automata	Backward reachability analysis for timed automata with data variables
V
Verification	Analyzing Consistency of Formal Requirements
W
Weakest precondition	Backward reachability analysis for timed automata with data variables

Disclaimer | Powered by EasyChair Smart Program