FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
VSTTE PROGRAM

Days: Wednesday, July 18th Thursday, July 19th

Wednesday, July 18th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 121N: Model Checking I

Model Checking I

Location: Maths LT2
09:00
A Tree-Based Approach to Data Flow Proofs (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 123N: Model Checking II

Model Checking II

Location: Maths LT2
11:00
Executable Counterexamples in Software Model Checking (abstract)
11:30
Extending VIAP to Handle Array Programs (abstract)
12:00
Lattice-Based Refinement in Bounded Model Checking (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 124N: Certification & Formalisation I

Certification & Formalisation I

Location: Maths LT2
14:00
Invited Talk, TBA (abstract)
15:00
Verified Certificate Checking for Counting Votes (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 126M: Certification & Formalisation II

Certification & Formalisation II

Location: Maths LT2
16:00
Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications (abstract)
16:30
TWAM: A Certifying Abstract Machine for Logic Programs (abstract)
17:00
A Java bytecode formalisation (abstract)
17:30
Formalising Executable Specifications of Low-Level Systems (abstract)
19:15-21:30 Workshops dinner at Magdalen College

Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).

Thursday, July 19th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 127H: Certification & Formalisation III

Certification & Formalisation III

Location: Maths LT2
09:00
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 129H: Security

Security

Location: Maths LT2
11:00
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components (abstract)
11:30
SideTrail: Verifying Time-Balancing of Cryptosystems (abstract)
12:00
Towards verification of Ethereum smart contracts: a formalization of core of Solidity (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 131H: New Applications

New Applications

Location: Maths LT2
14:00
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms (abstract)
14:30
Practical Methods for Reasoning about Java 8's Functional Programming Features (abstract)
15:00
Verification of Binarized Neural Networks via Inter-Neuron Factoring (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 133G: Off the beaten track

Off the beaten track

Location: Maths LT2
16:00
The Map Equality Domain (abstract)
16:30
Loop Detection by Logically Constrained Term Rewriting (abstract)
17:00
Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment (abstract)