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 124N: Model Checking I
Model Checking I
Chair:
Location: Maths LT2
| 09:00 | A Tree-Based Approach to Data Flow Proofs (abstract)   |
10:30-11:00Coffee Break
11:00-12:30 Session 126N: Model Checking II
Model Checking II
Chair:
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 127N: Certification & Formalisation I
Certification & Formalisation I
Chair:
Location: Maths LT2
| 14:00 | Verified Software: Theories, Tools, and Engineering (Invited Talk) (abstract) |
| 15:00 | Verified Certificate Checking for Counting Votes (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 129M: Certification & Formalisation II
Certification & Formalisation II
Chair:
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).
Location: Magdalen College
Thursday, July 19th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 130H: Certification & Formalisation III
Certification & Formalisation III
Chair:
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 132H: Security
Security
Chair:
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 134H: New Applications
New Applications
Chair:
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 136G: Off the beaten track
Off the beaten track
Chair:
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) |