FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program