FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
PROGRAM

Days: Sunday, July 1st Monday, July 2nd Tuesday, July 3rd Wednesday, July 4th Thursday, July 5th Friday, July 6th Saturday, July 7th Sunday, July 8th Monday, July 9th Tuesday, July 10th Wednesday, July 11th Thursday, July 12th Friday, July 13th Saturday, July 14th Sunday, July 15th Monday, July 16th Tuesday, July 17th Wednesday, July 18th Thursday, July 19th

Sunday, July 1st

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 1 (FoPSS)
09:00
Computational learning theory I (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 2 (FoPSS)
11:00
Computational learning theory II (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 3 (FoPSS)
14:00
Statistical learning theory I (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 4 (FoPSS)
16:00
Statistical learning theory II (abstract)
Monday, July 2nd

View this program: with abstractssession overviewtalk overview

10:30-11:00Coffee Break
12:30-14:00Lunch Break
15:30-16:00Coffee Break
Tuesday, July 3rd

View this program: with abstractssession overviewtalk overview

10:30-11:00Coffee Break
12:30-14:00Lunch Break
Wednesday, July 4th

View this program: with abstractssession overviewtalk overview

10:30-11:00Coffee Break
12:30-14:00Lunch Break
14:00-15:30 Session 13 (FoPSS)
14:00
Verification of machine learning programs I (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 14 (FoPSS)
16:00
Verification of machine learning programs II (abstract)
Thursday, July 5th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 15 (FoPSS)
09:00
Learning and epistemic modal logic I (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 16 (FoPSS)
11:00
Learning and epistemic modal logic II (abstract)
12:30-14:00Lunch Break
15:30-16:00Coffee Break
Friday, July 6th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 19 (FoPSS)
09:00
Inductive logic programming and deep learning I (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 20 (FoPSS)
11:00
Inductive logic programming and deep learning II (abstract)
12:30-14:00Lunch Break
15:30-16:00Coffee Break
Saturday, July 7th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 23A (CL&C)
09:00
Sheaf models of classical logic extended by independence relations (abstract)
10:00
Towards a Dualized Sequent Calculus with Canonicity (abstract)
09:00-10:30 Session 23B (Domains13)
Location: Maths LT1
09:00
Invited Talk: Looking Backward; Looking Forward (abstract)
10:00
A Brouwerian proof of the Fan Theorem (abstract)
09:00-10:30 Session 23D: Invited talk: Emily Riehl (HDRA)
Location: Blavatnik LT2
09:00
Homotopy coherent adjunctions and other structures (abstract)
10:00
Merge-bicategories: towards semi-strictification of higher categories (abstract)
09:00-10:00 Session 23E: Invited talk: Naoki Kobayashi (HOR)
09:00
On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification (abstract)
09:00-10:30 Session 23F: Invited Talk and Higher Dimensional Rewriting (IWC)
09:00
Confluence in Constraint Handling Rules: An overview from early, fundamental results to recent extensions including state invariants and conf. modulo equivalence. (abstract)
10:00
Coherence modulo relations (abstract)
09:00-10:30 Session 23G: Type Theory and Proof Assistants (LFMTP)
Location: Maths LT2
09:00
Invited talk: Cubical Computational Type Theory and RedPRL (abstract)
10:00
Sharing a library between proof assistants: reaching out to the HOL family (abstract)
09:00-10:30 Session 23H: Amiga (LOLA)
09:00
Asynchronous games fifteen years later (abstract)
09:30
Algebraic Theories and Control Effects, Back and Forth (abstract)
09:00-10:30 Session 23I (Linearity/TLLA)
09:00
Substructural Calculi with Dependent Types (abstract)
09:20
On the Lambek Calculus with an Exchange Modality (abstract)
09:55
The Bang Calculus and the Two Girard's Translations (abstract)
09:00-10:30 Session 23J: Invited and Contributed (NLCS)
09:00
Is compositionality all it's cracked up to be? (abstract)
10:00
Anti-Unification and Natural Language Processing (abstract)
09:00-10:30 Session 23L: Tuning solvers and applications (POS)
Location: Maths L5
09:00
Tuning Parallel SAT Solvers (abstract)
09:30
CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances (abstract)
10:00
Stedman and Erin Triples encoded as a SAT Problem (abstract)
09:00-10:30 Session 23N: switch (TYDI)
Location: Maths Boardroom
09:00
An introduction to deep inference (abstract)
10:00
Deep-Inference Intersection Types (abstract)
09:00-10:30 Session 23P: Invited Talk, and orders and sets of E-unifiers (UNIF)
09:00
Handling substitutions via duality (abstract)
10:00
Unification based on generalized embedding (abstract)
09:30-10:30 Session 24A (HoTT/UF)
Location: Blavatnik LT1
09:30
Axiomatizing Cubical Sets Models of Univalent Foundations (abstract)
09:30-10:30 Session 24B: Invited Talk (TERMGRAPH)
09:30
Critical Pairs in Graph Transformation Systems (abstract)
10:00-10:30 Session 25 (HOR)
10:00
Combinatorics of explicit substitutions (extended abstract) (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 26A (CL&C)
11:00
Fast cut-elimination using proof terms: an empirical study (abstract)
11:45
Validating Back-links of FOL-ID Cyclic Pre-proofs (abstract)
11:00-12:30 Session 26B (Domains13)
Chair:
Location: Maths LT1
11:00
Invited Talk: A Brief History of Denotational Semantics (abstract)
11:30
First-order differential programming (abstract)
12:00
Games and domains (abstract)
11:00-12:30 Session 26C (GS)
Location: Maths LT3
11:00
Some reflections on algorithmic game semantics (abstract)
11:30
Strategies as sheaves on plays (abstract)
11:00-12:30 Session 26D (HDRA)
Location: Blavatnik LT2
11:00
The equivalence between opetopic sets and many-to-one polygraphs (abstract)
11:30
Minimal models for monomial algebras (abstract)
12:00
Termination in linear (2,2)-categories with braidings and duals (abstract)
11:00-12:00 Session 26E: Invited talk: Pierre Vial (HOR)
11:00
Some applications of quantitative types inside and outside type theory (abstract)
11:00-12:30 Session 26F (HoTT/UF)
Location: Blavatnik LT1
11:00
Internalizing Presheaf Semantics: Charting the Design Space (abstract)
11:30
Cubical Assemblies and the Independence of the Propositional Resizing Axiom (abstract)
12:00
Dependent Right Adjoint Types (abstract)
11:00-12:30 Session 26G: Algebraic Structures and Coherence (IWC)
11:00
Coherence of monoids by insertions (abstract)
11:30
Critical pairs for Gray categories (abstract)
12:00
The diamond lemma for free modules (abstract)
11:00-12:40 Session 26H: Verification and Testing (LFMTP)
Location: Maths LT2
11:00
Invited talk: Why and How Does K work? The Logical Infrastructure Behind It (abstract)
12:00
Computation-as-deduction in Abella: work in progress (abstract)
12:20
Property-Based Testing of Abstract Machines: an Experience Report (abstract)
11:00-12:30 Session 26I: Bellmac (LOLA)
11:00
A more precise, more correct stack and register model for CompCert (abstract)
11:30
Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic (abstract)
12:00
A graph-rewriting perspective of the beta-law (abstract)
11:00-12:35 Session 26J (Linearity/TLLA)
11:00
Termination of lambda-calculus linearization methods (abstract)
12:00
Taking Linear Logic Apart (abstract)
11:00-12:30 Session 26K: Contributed papers (NLCS)
Chair:
11:00
Propositional Attitude Operators in Homotopy Type Theory (abstract)
11:30
Propositional Forms of Judgemental Interpretations (abstract)
12:00
Paychecks, Presupposition, and Dependent Types (abstract)
11:00-12:30 Session 26L: Contributed talks (PARIS)
Location: Maths L4
11:00
Local Validity for Circular Proofs in Linear Logic with Fixed Points (abstract)
11:45
Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (abstract)
11:00-12:30 Session 26M: Pseudo-Boolean and Proofs (POS)
Location: Maths L5
11:00
Two flavors of DRAT (abstract)
11:30
Competitive Sorter-based Encoding of PB-Constraints into SAT (abstract)
12:00
Divide and Conquer: Towards Faster Pseudo-Boolean Solving (abstract)
11:00-12:30 Session 26P: Frameworks (TERMGRAPH)
11:00
Drags: an algebraic framework for graph rewriting (abstract)
11:30
A framework for rewriting families of string diagrams (abstract)
12:00
On quasi ordinal diagram systems (abstract)
11:00-12:30 Session 26Q: promotion (TYDI)
Location: Maths Boardroom
11:00
Truely Concurrent Processes in the Calculus of Structures (abstract)
11:30
Sequentialising nested systems (abstract)
12:00
Nested sequents for modal logics and beyond (abstract)
11:00-12:30 Session 26R: Unification, protocol analysis, and logics (UNIF)
11:00
Knowledge Problems in Equational Extensions of Subterm Convergent Theories (abstract)
11:30
Bounded ACh Unification (abstract)
12:00
About the unification type of topological logics over Euclidean spaces (abstract)
12:00-12:30 Session 27 (HOR)
12:00
Orthogonality and sequentiality in substructural Linear HRSs (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 28A (CL&C)
14:00
On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains (abstract)
14:45
Herbrand's Theorem as Higher-Order Recursion (abstract)
14:00-15:30 Session 28B (Domains13)
Location: Maths LT1
14:00
Invited Talk: Scott Domains for Denotational Semantics and Program Extraction (abstract)
14:40
Robust computability notions for types arising in classical analysis (abstract)
15:05
T^\omega-representations of compact sets through dyadic subbases (abstract)
14:00-15:30 Session 28C (GS)
Location: Maths LT3
14:00
Game semantics: from call-by-push-value and CPS to coalgebra (abstract)
14:30
Incomplete information and uniformity in game semantics (abstract)
15:00
Asynchronous games fifteen years later (abstract)
14:00-15:30 Session 28F: Term Rewriting (IWC)
14:00
Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (abstract)
14:30
Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (abstract)
15:00
Certified Ordered Completion (abstract)
14:00-15:30 Session 28G: Formalization (LFMTP)
Location: Maths LT2
14:00
Formalization in Constructive Type Theory of the Standardization Theorem (abstract)
14:30
Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (abstract)
15:00
What Does This Notation Mean Anyway? BNF-style notation as it is actually used (abstract)
14:00-15:30 Session 28H (Linearity/TLLA)
14:00
The structure of non decomposable connectives of linear logic (abstract)
14:20
On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (abstract)
14:55
From Linear Logic to Cyclic Sharing (abstract)
14:00-15:30 Session 28I: Contributed papers (NLCS)
Chair:
14:00
Speakers in vats: simulating model-theoretic alignment with distributional semantics (abstract)
15:00
Graph Knowledge Representations for SICK (abstract)
14:00-15:30 Session 28J: Contributed talks (PARIS)
Location: Maths L4
14:00
Useless Explicit Induction Reasoning (abstract)
14:45
Towards the Automatic Construction of Schematic Proofs (abstract)
14:00-15:30 Session 28K (PC)
Location: Maths L6
14:00
Space Proof Complexity beyond Resolution (abstract)
15:00
Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (abstract)
14:00-15:30 Session 28L: Determinacy, compositionality (SR)
Chair:
14:00
Compositional Game Theory (abstract)
14:40
Concurrent games and semi-random determinacy (abstract)
14:00-15:30 Session 28M: Invited Talk, and Semantics (TERMGRAPH)
14:00
Modeling terms by graphs with structure constraints (two illustrations) (abstract)
15:00
Semantics-Preserving DPO-Based Term Graph Rewriting (abstract)
14:00-15:30 Session 28N: Medial (TYDI)
Location: Maths Boardroom
14:00
Two Unifying Structural Principles (abstract)
15:00
Deep Inference, Herbrand's Theorem and Expansion Proofs (abstract)
14:00-15:30 Session 28P: Invited Talk, and Unification Modulo (UNIF)
14:00
Compressed Term Unification: Results, uses, open problems, and hopes (abstract)
15:00
ACUI Unification modulo Ground Theories (abstract)
14:30-15:30 Session 29A: Commodore (LOLA)
14:30
Invited talk: Semantic Equivalence Checking for HHVM Bytecode (abstract)
14:30-15:30 Session 29B: MAXSAT & local search (POS)
Location: Maths L5
14:30
Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving (abstract)
15:00
MLIC: A MaxSAT-Based framework for learning interpretable classification rules (abstract)
15:00-15:30 Session 30A (HDRA)
Location: Blavatnik LT2
15:00
Towards a fully formalized definition of syllepsis in weak higher categories (abstract)
15:00-15:30 Session 30B (HOR)
15:00
Refining Properties of Filter Models: Sensibility, Approximability and Reducibility (abstract)
15:00-15:30 Session 30C (HoTT/UF)
Location: Blavatnik LT1
15:00
Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 31A (CL&C)
16:00
Admissible tools in the kitchen of intuitionistic logic (abstract)
16:30
The “duality of computation” from a fibrational perspective (abstract)
17:00
A Denotational Model of the Typed Lambda-Mu Calculus (abstract)
17:30
Some ideas on cut-elimination for cyclic arithmetic proofs (abstract)
16:00-16:50 Session 31B (Domains13)
Location: Maths LT1
16:00
Higher-dimensional categories: recursion on extensivity (abstract)
16:25
A logical view of complex analytic maps (abstract)
16:00-18:00 Session 31C (GS)
Chair:
Location: Maths LT3
16:00
Games and the Lambda Cube (abstract)
16:30
Games, Geometry of Interaction, Reversible Computations, Lambda Calculus (abstract)
17:00
Characterizing observational equivalence for PCF terms within richer languages (abstract)
16:00-18:00 Session 31D (HDRA)
Location: Blavatnik LT2
16:00
Minimal Bacus FP is Turing Complete (abstract)
16:30
String data structures for Chinese monoids (abstract)
17:00
Generalizations of the associative operad and convergent rewrite systems (abstract)
17:30
Normal forms for planar connected string diagrams (abstract)
16:00-17:00 Session 31E (HOR)
16:00
Normalization and Taylor expansion of lambda-terms (abstract)
16:30
The next 700 (type-theoretical) denotational models ? (abstract)
16:00-18:00 Session 31F (HoTT/UF)
Location: Blavatnik LT1
16:00
Univalent Foundations and the Constructive View of Theories (abstract)
16:30
Algebraic models of dependent type theory (abstract)
17:00
First-order homotopical logic and Grothendieck fibrations (abstract)
16:00-18:00 Session 31H: Implementation (LFMTP)
Location: Maths LT2
16:00
Invited talk: A fresh view of call-by-need (abstract)
17:00
Abstract Representation of Binders in OCaml using the Bindlib Library (abstract)
17:30
Functional programming with λ-tree syntax: a progress report (abstract)
16:00-18:00 Session 31I: DECsystem (LOLA)
16:00
Denotational Event structure for relaxed memory (abstract)
16:30
A resource modality for RAII (abstract)
17:00
Experimenting with graded monads: certified grading-based program transformations (abstract)
17:30
Heaps denote finitely partitioned trees (abstract)
16:00-18:10 Session 31J (Linearity/TLLA)
16:00
Applying linear logic semantics to probabilistic programming (abstract)
17:00
Proof nets, coends and the Yoneda isomorphism (abstract)
17:35
Quantum programming made easy (abstract)
16:00-18:00 Session 31K: Contributed talks (NLCS)
16:00
Automated Reasoning from Polarized Parse Trees (abstract)
16:30
Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus. (abstract)
17:00
Automatic test suite generation for PMCFG grammars (abstract)
17:30
OpenWordNet-PT: Taking Stock (abstract)
16:00-18:00 Session 31L: Invited talk + contributed talk (PARIS)
Location: Maths L4
16:00
The size-change principle and circular proofs: checking totality of (co)recursive definitions (abstract)
17:15
What makes guarded types tick? (abstract)
16:00-18:10 Session 31M (PC)
Location: Maths L6
16:00
On OBBD Proofs (abstract)
17:00
Resolution and the binary encoding of combinatorial principles (abstract)
17:20
Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (abstract)
17:40
Proof systems for #SAT based on restricted circuits (abstract)
16:00-18:00 Session 31N: SAT pragmatics (POS)
Location: Maths L5
16:00
A Problem Meta-Data Library for Research in SAT (abstract)
16:30
The Effect of Scrambling CNFs (abstract)
17:00
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (abstract)
17:30
On the use of solvers with docker technology (abstract)
17:45
Questions and Answers (abstract)
16:00-18:00 Session 31P: Multiple-player games (SR)
16:00
Verification of Multi-agent Systems with Imperfect Information and Public Actions (abstract)
16:40
Local Equilibria in Logic-Based Multi-Player Games (abstract)
17:20
Beyond admissibility: Dominance between chains of strategies (abstract)
16:00-18:00 Session 31Q: Applications (TERMGRAPH)
16:00
SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract (abstract)
16:30
A Port-graph Model for Finance (abstract)
17:00
Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting (abstract)
17:30
Programming by Term Rewriting (abstract)
16:00-18:00 Session 31R: Contraction (TYDI)
Location: Maths Boardroom
16:00
Some incoherent musings on deep inference and combinatorial proofs (abstract)
17:00
Proof complexity of deep inference: a survey (abstract)
16:00-18:10 Session 31S: Nominal Unification and Formalisations (UNIF)
16:00
Proximity-Based Generalization (abstract)
16:30
Towards Generalization Methods for Purely Idempotent Equational Theories (abstract)
17:00
Rewriting with Generalized Nominal Unification (abstract)
17:30
Formalization of First-Order Syntactic Unification (abstract)
17:50
Efficiency of a good but not linear nominal unification algorithm (abstract)
18:10-18:40 Session 33: UNIF 2018 Wrap Up (UNIF)

Discussions about UNIF 2018 issues and future of UNIF

19:00-21:00 UNIF Dinner (UNIF)

This is a dinner in a restaurant to be defined different from the FLOC dinner at Balliot College.

19:00-21:00 LFMTP Dinner (LFMTP)

This is a dinner in a restaurant to be defined different from the FLOC dinner at Balliot College.

To register, please send a mail to lfmtp18@easychair.org before July 1st.

19:45-22:00 Workshops dinner at Balliol College (FLoC)

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).

Location: Balliol College
Sunday, July 8th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 34A (COALG)
09:00
The Method of Coalgebra: Exercises in Coinduction (abstract)
09:45
Coalgebra meets Convexity in Probabilistic Systems (abstract)
09:00-10:30 Session 34B (Coq)
Location: Maths LT2
09:00
Verifying Distributed Systems (abstract)
10:00
Procrastination, A proof engineering technique (abstract)
09:00-10:00 Session 34C: DCM/ITRS joint invited talk (DCM and ITRS)
09:00
Quantitative types: from Foundations to Applications (abstract)
09:00-10:30 Session 34D (Domains13)
Location: Maths LT1
09:00
Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences (abstract)
09:40
Diffeological Spaces and Semantics for Differential Programming (abstract)
10:05
Domain Theory for Intensional Computation (abstract)
09:00-10:30 Session 34E: Invited talk & IoT security (FCS)
09:00
A Formal Approach to Cyber-Physical Attacks (abstract)
10:00
LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems (abstract)
09:00-10:30 Session 34F (GS)
Location: Maths LT3
09:00
The Geometry of Parallelism: Probabilistic and Quantum Effects (abstract)
09:30
The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (abstract)
10:00
Coalgebras and Higher-Order Computation: a GoI Approach (abstract)
09:00-10:30 Session 34G: Opening and Keynote (GraMSec)
09:00
Opening remarks and introductions (abstract)
09:10
Intrusion Tolerance in Complex Cyber Systems (abstract)
10:10
Disclosure Analysis of SQL Workflows (abstract)
09:00-10:30 Session 34I (LMW)
Location: Maths Boardroom
09:00
How to get the most out of a conference like FLOC? (abstract)
09:30
Asking questions to yourself and others (abstract)
09:00-10:30 Session 34J (Linearity/TLLA)
09:00
Towards a Functional Language for Species of Structures (abstract)
09:20
How to count linear and affine closed lambda terms? (abstract)
09:55
Entropy and Complexity Lower Bounds (abstract)
09:00-10:30 Session 34K (MSFP)
09:00
Polynomial models of type theory (abstract)
10:00
Some No-Go Theorems for Distributive Laws (extended abstract) (abstract)
09:00-10:30 Session 34L: Joint QBF / Proof Complexity session (PC and QBF)
Location: Maths L5
09:00
Lower Bound Techniques for QBF Proof Systems (abstract)
10:00
Towards the Semantics of QBF Clauses (abstract)
09:00-10:30 Session 34N (WiL)
Location: Blavatnik LT2
09:00
Logic and Software Engineering: Are We Nearly There Yet? (abstract)
10:00
First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation (abstract)
10:15
A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) (abstract)
09:30-10:30 Session 36A (HoTT/UF)
Location: Blavatnik LT1
09:30
Injective types and searchable types in univalent mathematics (abstract)
10:00-10:30 Session 37 (DCM)
10:00
Models of Computation that Conserve Data (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 38A (COALG)
Chair:
11:00
Coalgebra and Automated Reasoning (abstract)
11:45
Coalgebraic Tools for Randomness-Conserving Protocols (abstract)
11:00-12:30 Session 38B (Coq)
Location: Maths LT2
11:00
Classical Analysis with Coq (abstract)
11:30
What is the Foreign Function Interface of the Coq Programming Language? (abstract)
12:00
Preliminary Report on the Yalla Library (abstract)
11:00-12:30 Session 38C (DCM)
Chair:
11:00
A syntactic model of mutation and aliasing (abstract)
11:30
Pointing to Private Names (abstract)
12:00
A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms (abstract)
11:00-12:30 Session 38D (Domains13)
Location: Maths LT1
11:00
Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming (abstract)
11:40
Abstractness of Continuation Semantics for Asynchronous Concurrency (abstract)
12:05
Algebra semantics of recursive computation types (abstract)
11:00-12:30 Session 38E: Formal Modelling & Analysis (FCS)
11:00
An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control (abstract)
11:30
Proving physical proximity using symbolic models (abstract)
12:00
Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols (abstract)
11:00-12:30 Session 38F (GS)
Location: Maths LT3
11:00
Making parallel-or deterministic again: intentional full abstraction for por (abstract)
11:30
Generalised Species of Plays (abstract)
12:00
Probabilistic strategies (abstract)
11:00-12:30 Session 38G: Technical Papers (GraMSec)
11:00
A state machine system for insider threat detection (abstract)
11:45
Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures (abstract)
11:00-12:30 Session 38H (HoTT/UF)
Location: Blavatnik LT1
11:00
A Yoneda lemma-formulation of the univalence axiom (abstract)
11:30
Robust Notions of Contextual Fibrancy (abstract)
12:00
Cohesive Covering Theory (abstract)
11:00-12:30 Session 38J (ITRS)
11:00
Natural Deduction and Normalization Proofs for the Intersection Type Discipline (abstract)
11:30
Strong normalization of simple types through uniform intersection types. (abstract)
12:00
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (abstract)
11:00-12:30 Session 38K (Linearity/TLLA)
11:00
Infinitary Proof Theory: the Multiplicative Additive Case (abstract)
12:00
Models of Linear Logic based on the Schwartz epsilon product (abstract)
11:00-12:30 Session 38L (MSFP)
11:00
Formalizing Constructive Quantifier Elimination in Agda (abstract)
11:45
Relating Idioms, Arrows and Monads from Monoidal Adjunctions (abstract)
11:00-12:30 Session 38M: Contributed talks (PARIS)
Location: Maths L4
11:00
LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (abstract)
11:45
Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI) (abstract)
11:00-12:30 Session 38N: Joint QBF / Proof Complexity session (PC and QBF)
Location: Maths L5
11:00
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs (abstract)
11:30
Short Proofs in QBF Expansion (abstract)
11:50
The Symmetry Rule for Quantified Boolean Formulas (abstract)
12:10
Discussion (abstract)
11:00-12:30 Session 38Q (WPTE)
11:00
Automating the Diagram Method to Prove Correctness of Program Transformations (abstract)
11:30
Optimizing Space of Parallel Processes (abstract)
12:00
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems (abstract)
11:00-12:40 Session 38R (WiL)
Location: Blavatnik LT2
11:00
On Expanding Standard Notions of Constructivity (abstract)
11:15
Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis (abstract)
11:30
A semantical view of sequent based systems (abstract)
11:45
Decomposing labelled proof theory for intuitionistic modal logic (abstract)
12:00
About the unification type of topological logics over Euclidean spaces (abstract)
11:30-12:30 Session 39 (LMW)
Location: Maths Boardroom
11:30
Can Logic Make Us Better People? (abstract)
12:00
Research as a collaborative effort (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 40A (COALG)
14:00
Coalgebras and Kleisli Maps for Probability (abstract)
14:45
Coalgebraic Logics: From Branching Time to Linear Time (abstract)
14:00-15:30 Session 40B (Coq)
Location: Maths LT2
14:00
A Coq mechanised formal semantics for real life SQL queries : Formally reconciling SQL and (extended) relational algebra. (abstract)
15:00
Discussion with the Coq development team (abstract)
14:00-15:30 Session 40C (DCM)
14:00
On Higher-Order Probabilistic Computation. (abstract)
15:00
Towards a Formal System for Topological Quantum Computation (abstract)
14:00-15:05 Session 40D (Domains13)
Location: Maths LT1
14:00
Invited Talk: Topology and Domain Theory Interfaces (abstract)
14:40
A Domain-theoretic Skorohod’s Theorem (abstract)
14:00-15:30 Session 40E: Cryptography (FCS)
Chair:
14:00
A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler (abstract)
14:30
Homomorphisms and Minimality for Enrich-by-Need Security Analysis (abstract)
15:00
A Homotopical Approach to Cryptography (abstract)
14:00-15:30 Session 40F (GS)
Location: Maths LT3
14:00
How to denotational an operational semantics (abstract)
14:30
What's in a game? (abstract)
15:00
Game Semantics 25 years on (abstract)
14:00-15:30 Session 40G: Technical Papers (GraMSec)
14:00
Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins (abstract)
14:45
Deciding the Non-Emptiness of Attack trees (abstract)
14:00-15:30 Session 40H (HoTT/UF)
Location: Blavatnik LT1
14:00
Cubical Computational Type Theory (abstract)
14:30
The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (abstract)
15:00
Ordered Cubes (abstract)
14:00-15:30 Session 40I: Member Talk, Discussion (IFIP WG 1.6)
14:00
Informal Report on FSCD (abstract)
14:30
Discussion on Reviewing Culture in TCS (abstract)
15:15
Discussion on IFIP (abstract)
14:00-15:30 Session 40J (ITRS)
Chair:
14:00
Intersection Types for Unboundedness Problems (ITRS invited talk) (abstract)
15:00
Gradual Intersection Types (abstract)
14:00-15:30 Session 40K (LMW)
Location: Maths Boardroom
14:00
Relational verification of probabilistic programs (abstract)
14:30
Constrained Horn clauses as a basis of automatic program verification: the higher-order case (abstract)
15:00
Rewriting and Applications (abstract)
14:00-15:30 Session 40L (Linearity/TLLA)
14:00
Generalized generalized species of structure and resource modalities (abstract)
14:20
Benchmarking Linear Logic Translations (abstract)
14:55
Coherent interaction graphs: a nondeterministic geometry of interaction for MLL (abstract)
14:00-15:30 Session 40M (MSFP)
14:00
Ornamentation put into practice in ML (abstract)
15:00
Profunctor Optics and the Yoneda Lemma (abstract)
14:00-15:30 Session 40P (QBF)
Chair:
Location: Maths L5
14:00
Preprocessing for (D)QBF (abstract)
14:20
Initial study on the effect of different QBF solvers and preprocessors on link-information sensitive QBF encodings for Abstract Dialectical Frameworks (abstract)
14:40
Tractability results for structured quantified CNF-formulas via knowledge compilation (abstract)
15:00
A Grounder From Second-Order Logic To QBF (abstract)
15:20
PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution) (abstract)
15:25
Chess Solving and Composing (QBFEval18 Contribution) (abstract)
14:00-15:30 Session 40Q: Two-player games (SR)
14:00
Infinite-Duration Richman Bidding Games (abstract)
14:40
Solving Parity Games: Explicit vs Symbolic (abstract)
14:00-15:30 Session 40R (WPTE)
14:00
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (abstract)
14:30
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions (abstract)
15:00
Verification of Ada Programs with AdaHorn (abstract)
14:00-15:30 Session 40S (WiL)
Location: Blavatnik LT2
14:00
POPLMark Reloaded: Mechanizing Logical Relations Proofs (abstract)
15:00
Towards a Playground for Logicians (abstract)
15:15
Non-well-founded proof system for Transitive Closure Logic (abstract)
14:30-15:30 Session 41 (PC)
Location: Maths L6
14:30
Complexity of expander-based reasoning and the power of monotone proofs (abstract)
15:00
Towards theories for positive polynomial time and monotone proofs with extension (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 42A (COALG)
16:00
Martingale-Based Methods for Reachability Probabilities: Excitements and Afterthoughts about Coalgebras (abstract)
16:45
Coalgebra Dreams (abstract)
16:00-18:00 Session 42B (Coq)
Location: Maths LT2
16:00
ComplCoq: Rewrite Hint Construction with Completion Procedures (abstract)
16:30
Towards a formalization of the guard condition (abstract)
17:00
Teaching Your Rooster to Crow in C (abstract)
17:30
Proof Construction by Tactic Learning (abstract)
16:00-17:15 Session 42D (Domains13)
Location: Maths LT1
16:00
Frames and frame relations (abstract)
16:25
Extending Stone Duality to Relations (abstract)
16:50
Applications of entailments: de Groot duality (abstract)
16:00-18:00 Session 42E (GS)
Location: Maths LT3
16:00
Continuous probability distributions in concurrent games (abstract)
16:30
A definable game semantics for the linear quantum lambda-calculus (abstract)
17:00
Resource-Tracking Concurrent Games (abstract)
17:30
Automata Theory and Game Semantics (abstract)
16:00-18:00 Session 42F: Technical Papers and Closing Remarks (GraMSec)
Chair:
16:00
The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (abstract)
16:45
On Linear Logic, Functional Programming, and Attack Trees (abstract)
17:30
Closing remarks and discussions (abstract)
16:00-18:00 Session 42G (HoTT/UF)
Location: Blavatnik LT1
16:00
(Truncated) Simplicial Models of Type Theory (abstract)
16:30
Towards the syntax and semantics of higher dimensional type theory (abstract)
16:00-16:30 Session 42I (ITRS)
16:00
Intersection Subtyping with Constructors (abstract)
16:00-18:00 Session 42K (Linearity/TLLA)
16:00
A shared memory semantics for session types (abstract)
17:00
A semantic conjecture on second-order MLL and its complexity consequences (work in progress) (abstract)
17:20
Formalization of Automated Trading Systems in a Concurrent Linear Framework (abstract)
16:00-17:30 Session 42L (MSFP)
16:00
Backward induction for repeated games (abstract)
16:45
Everybody's Got To Be Somewhere (abstract)
16:00-17:30 Session 42M: Contributed talks (PARIS)
Location: Maths L4
16:00
Transitive Closure Logic: Infinitary and Cyclic Proof Systems (abstract)
16:45
On the Logical Complexity of Cyclic Arithmetic (abstract)
16:00-17:50 Session 42N (PC)
Location: Maths L6
16:00
A Comparison of Algebraic and Semi-Algebraic Proof Systems (abstract)
17:00
Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials (abstract)
17:30
On Dual-Rail Based MaxSAT Solving (abstract)
16:00-18:00 Session 42P (QBF)
Location: Maths L5
16:00
Understanding and Extending Incremental Determinization for 2QBF (abstract)
16:20
Portfolio-Based Algorithm Selection for Circuit QBFs (abstract)
16:40
DepQBF (QBFEval'18 Contribution) (abstract)
16:45
RAReQS, QFUN, QESTO (QBFEval'18 Contribution) (abstract)
16:50
Qute (QBFEval'18 Contribution) (abstract)
16:55
QBFEval 2018 (abstract)
17:20
Discussion (abstract)
16:00-17:00 Session 42R (WiL)
Location: Blavatnik LT2
16:00
On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (abstract)
16:15
Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (abstract)
16:30
Towards a Logical Framework for Latent Variable Modelling (abstract)
16:30-17:30 Session 43 (DCM and ITRS)
16:30
Polyadic approximations and intersection types (ITRS/DCM joint invited talk) (abstract)
17:00-18:00 Session 44: Priorities for Diversity in Logic in Computer Science (round table discussion) (WiL)

Round table panel discussion, where attendees will be joined by leading figures in the FLoC community to discuss "Priorities for Diversity in Logic for Computer Science".

Location: Blavatnik LT2
18:30-20:30 Women in Logic reception (WiL)

Women in Logic reception and buffet supper at Wadham College (contact Ursula.Martin@maths.ox.ac.uk for more details).

Location: Wadham College
Monday, July 9th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 46: FLoC Plenary Lecture: Peter O'Hearn (FLoC)
Location: Maths LT1
09:00
Continuous Reasoning: Scaling the Impact of Formal Methods (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 47A: Security protocols I (CSF)
Location: Maths LT2
11:00
An extensive formal analysis of multi-factor authentication protocols (abstract)
11:30
Composition Theorems for CryptoVerif and Application to TLS 1.3 (abstract)
12:00
A Cryptographic Look at Multi-Party Channels (abstract)
11:00-12:30 Session 47B: Linear Logic (FSCD)
11:00
Proof nets for bi-intuitionistic linear logic (abstract)
11:30
Unique perfect matchings and proof nets (abstract)
12:00
Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories (abstract)
11:00-12:00 Session 47C: ITP Invited Talk: John Harrison (ITP)
Location: Blavatnik LT1
11:00
Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification (abstract)
11:00-12:40 Session 47D (LICS)
Location: Maths LT1
11:00
Definable decompositions for graphs of bounded linear cliquewidth (abstract)
11:20
Parameterized circuit complexity of model-checking on sparse structures (abstract)
11:40
Sequential Relational Decomposition (abstract)
12:00
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (abstract)
12:20
Regular and First Order List Functions (abstract)
11:00-12:40 Session 47E (LICS)
Location: Maths LT3
11:00
A theory of linear typings as flows on 3-valent graphs (abstract)
11:20
Cellular Cohomology in Homotopy Type Theory (abstract)
11:40
Free Higher Groups in Homotopy Type Theory (abstract)
12:00
Higher Groups in Homotopy Type Theory (abstract)
12:20
Strong Sums in Focused Logic (abstract)
11:00-12:15 Session 47F: SAT Invited Talk: Christoph Scholl (SAT)
11:00
Welcome to SAT 2018 (abstract)
11:05
Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (abstract)
12:00-12:30 Session 48 (ITP)
Location: Blavatnik LT1
12:00
Efficient Mendler-Style Lambda-Encodings in Cedille (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 49A: CSF Invited Talk: Srini Devadas (CSF)
Location: Maths LT2
14:00
Sanctum: Towards an Open-Source, Formally Verified Secure Processor (abstract)
14:00-15:30 Session 49C (ITP)
Location: Blavatnik LT1
14:00
Formalizing Implicative Algebras in Coq (abstract)
14:30
Software Tool Support for Modular Reasoning in Modal Logics of Actions (abstract)
15:00
The Coinductive Formulation of Common Knowledge (abstract)
14:00-15:40 Session 49D (LICS)
Location: Maths LT1
14:00
A modal mu perspective on solving parity games in quasipolynomial time. (abstract)
14:20
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (abstract)
14:40
Rational Synthesis Under Imperfect Information (abstract)
15:00
Playing with Repetitions in Data Words Using Energy Games (abstract)
15:20
Compositional game theory (abstract)
14:00-15:40 Session 49E (LICS)
Location: Maths LT3
14:00
Concurrency and Probability: Removing Confusion, Compositionally (abstract)
14:20
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (abstract)
14:40
Eager Functions as Processes (abstract)
15:00
Quasi-Open Bisimilarity with Mismatch is Intuitionistic (abstract)
15:20
Causal Computational Complexity of Distributed Processes (abstract)
14:00-15:30 Session 49F: MaxSAT (SAT)
14:00
Approximately Propagation Complete and Conflict Propagating Constraint Encodings (abstract)
14:30
Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (abstract)
15:00
Solving MaxSAT with Bit-Vector Optimization (abstract)
15:00-15:30 Session 50A: Attack trees (CSF)
Location: Maths LT2
15:00
Guided design of attack trees: a system-based approach (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 51A: CSF 5 minutes talks (CSF)

Short talks by attendees. 

The 5-minute talk schedule is available here.

This is a fun session in which you can describe work in progress, crazy-sounding ideas, interesting questions and challenges, research proposals, or anything else within reason! You can use 2-3 slides, or you can just speak without slides.

Chair:
Location: Maths LT2
16:00-18:00 Session 51B: Corrado Böhm Memorial (FSCD)
16:00
ALGORAND A Truly Distributed Ledger (abstract)
17:00
Corrado Böhm: the white magician in programming and its semantics (abstract)
16:00-18:00 Session 51C (ITP)
Location: Blavatnik LT1
16:00
Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (abstract)
16:30
Boosting the Reuse of Formal Specifications (abstract)
17:00
Formalization of a Polymorphic Subtyping Algorithm (abstract)
17:30
A Formal Equational Theory for Call-by-Push-Value (abstract)
16:00-18:00 Session 51D (LICS)
Location: Maths LT1
16:00
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (abstract)
16:20
A Simple and Optimal Complementation Algorithm for Büchi Automata (abstract)
16:40
The State Complexity of Alternating Automata (abstract)
17:00
Automaton-Based Criteria for Membership in CTL (abstract)
17:20
Separability by piecewise testable languages and downward closures beyond subwords (abstract)
17:40
Regular Transducer Expressions for Regular Transformations over infinite words (abstract)
16:00-18:00 Session 51E (LICS)
Location: Maths LT3
16:00
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (abstract)
16:20
An algebraic theory of Markov processes (abstract)
16:40
Boolean-Valued Semantics for Stochastic Lambda-Calculus (abstract)
17:00
Sound up-to techniques and Complete abstract domains (abstract)
17:20
Every λ-Term is Meaningful for the Infinitary Relational Model (abstract)
17:40
Probabilistic Böhm Trees and Probabilistic Separation (abstract)
16:00-18:00 Session 51F: CDCL (SAT)
16:00
Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (abstract)
16:30
Machine Learning-based Restart Policy for CDCL SAT Solvers (abstract)
17:00
Chronological Backtracking (abstract)
17:30
Centrality-Based Improvements to CDCL Heuristics (abstract)
19:00-21:30 FLoC reception at Ashmolean Museum (FLoC)

FLoC reception at Ashmolean Museum. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).

Tuesday, July 10th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 52A: Cryptographic primitives (CSF)
Location: Maths LT2
09:00
Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (abstract)
09:30
Formal Security Proof of CMAC and its Variants (abstract)
10:00
Backdoored Hash Functions: Immunizing HMAC and HKDF (abstract)
09:00-10:30 Session 52B: Types (FSCD)
09:00
Call-by-name Gradual Type Theory (abstract)
09:30
The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (abstract)
10:00
Internal Universes in Models of Homotopy Type Theory (abstract)
09:00-10:00 Session 52C: ITP Invited Talk: Dan Grayson (ITP)
Location: Blavatnik LT1
09:00
Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics (abstract)
09:00-10:30 Session 52E: Model Counting (SAT)
09:00
Fast Sampling of Perfectly Uniform Satisfying Assignments (abstract)
09:30
Fast and Flexible Probabilistic Model Counting (abstract)
10:00
Exploiting Treewidth for Projected Model Counting and its Limits (abstract)
10:00-10:30 Session 53A (ITP)
Location: Blavatnik LT1
10:00
CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math” (abstract)
10:00-10:40 Session 53B (LICS)
Location: Maths LT1
10:00
Polynomial Invariants for Affine Programs (abstract)
10:20
An answer to the Gamma question (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 54A: Secure computation (CSF)
Location: Maths LT2
11:00
Computer-aided proofs for multiparty computation with active security (abstract)
11:30
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (abstract)
12:00
Symbolic security of garbled circuits (abstract)
11:00-12:30 Session 54B: Types (FSCD)
11:00
A Unifying Framework for Type Inhabitation (abstract)
11:30
Cumulative Inductive Types in Coq (abstract)
12:00
Index-Stratified Types (abstract)
11:00-12:30 Session 54C (ITP)
Location: Blavatnik LT1
11:00
A Formalization of the LLL Basis Reduction Algorithm (abstract)
11:30
A Formally Verified Solver for Homogeneous Linear Diophantine Equations (abstract)
12:00
A Coq Tactic for Equality Learning in Linear Arithmetic (abstract)
11:00-12:40 Session 54D (LICS)
Location: Maths LT1
11:00
On the number of types in sparse graphs (abstract)
11:20
Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (abstract)
11:40
Tree depth, quantifier elimination, and quantifier rank (abstract)
12:00
Wreath Products of Distributive Forest Algebras (abstract)
12:20
MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (abstract)
11:00-12:40 Session 54E (LICS)
Location: Maths LT3
11:00
Impredicative Encodings of (Higher) Inductive Types (abstract)
11:20
Guarded Computational Type Theory (abstract)
11:40
Work Analysis with Resource-Aware Session Types (abstract)
12:00
A General Framework for Relational Parametricity (abstract)
12:20
Classical realizability as a classifier for nondeterminism (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 55A: Knowledge and hyperproperties (CSF)
Location: Maths LT2
14:00
The Complexity of Monitoring Hyperproperties (abstract)
14:30
Knowledge-based Security of Dynamic Secrets for Reactive Programs (abstract)
15:00
Assuming you know: epistemic semantics of relational annotations for expressive flow policies (abstract)
14:00-15:00 Session 55B: FSCD Invited talk: Valeria Vignudelli (FSCD)
14:00
Proof techniques for program equivalence in probabilistic higher-order languages (abstract)
14:00-15:30 Session 55C (ITP)
Location: Blavatnik LT1
14:00
Backwards and Forwards with Separation Logic (abstract)
14:30
Reification by Parametricity (abstract)
15:00
A Coq Formalisation of SQL’S Execution Engines (abstract)
14:00-15:20 Session 55D (LICS)
Location: Maths LT1
14:00
A van Benthem Theorem for Fuzzy Modal Logic (abstract)
14:20
Riesz Modal Logic with Threshold Operators (abstract)
14:40
Logics for Word Transductions with Synthesis (abstract)
15:00
Type-two polynomial-time and restricted lookahead. (abstract)
14:00-15:20 Session 55E (LICS)
Chair:
Location: Maths LT3
14:00
LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (abstract)
14:20
A Logical Account for Linear Partial Differential Equations (abstract)
14:40
Unification nets: canonical proof net quantifiers (abstract)
15:00
Around Classical and Intuitionistic Linear Logics (abstract)
14:00-15:30 Session 55F: QBF I (SAT)
Chair:
14:00
Circuit-based Search Space Pruning in QBF (abstract)
14:30
Symmetries for QBF (abstract)
15:00
Local Soundness for QBF Calculi (abstract)
15:30-16:00Coffee Break
15:40-16:40 Session 57A: Complexity (FSCD)
15:40
Counting Environments and Closures (abstract)
16:10
Term rewriting characterisation of LOGSPACE for finite and infinite data (abstract)
15:40-16:40 Session 57B (LICS)
Location: Maths LT1
15:40
Distribution-based objectives for Markov Decision Processes (abstract)
16:00
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (abstract)
16:20
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (abstract)
15:40-16:40 Session 57C (LICS)
Location: Maths LT3
15:40
What's in a game? A theory of game models (abstract)
16:00
An Asynchronous Soundness Theorem for Concurrent Separation Logic (abstract)
16:20
The concurrent game semantics of Probabilistic PCF (abstract)
16:00-17:00 Session 58B (ITP)
Location: Blavatnik LT1
16:00
An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (abstract)
16:30
Towards Certified Meta-Programming with Typed Template-Coq (abstract)
16:00-17:00 Session 58C: QBF II (SAT)
16:00
QBF as an Alternative to Courcelle's Theorem (abstract)
16:30
Polynomial-Time Validation of QCDCL Certificates (abstract)
17:00-18:30 Session 59: FLoC Public Lecture: Stuart Russell (FLoC)

Doors open at 4:30 pm; please be seated by 4:50 pm (attendance is free of charge and all are welcome; please register).

17:00
Unifying Logic and Probability: the BLOG Language (abstract)
Wednesday, July 11th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 60B: Information flow (CSF)
Location: Maths LT2
09:00
A Permission-Dependent Type System for Secure Information Flow Analysis (abstract)
09:30
Types for Information Flow Control: Labeling Granularity and Semantic Models (abstract)
10:00
Inductive Invariants for Noninterference in Multi-agent Workflows (abstract)
09:00-10:30 Session 60C: Lambda Calculus (FSCD)
09:00
On repetitive right application of B-terms (abstract)
09:30
Homogeneity without Loss of Generality (abstract)
10:00
Strict Ideal Completions of the Lambda Calculus (abstract)
09:00-10:30 Session 60D (ITP)
Location: Blavatnik LT1
09:00
Program Verification in the Presence of Cached Address Translation (abstract)
09:30
Physical Addressing on Real Hardware in Isabelle/HOL (abstract)
10:00
Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (abstract)
09:00-10:30 Session 60F: Theory (SAT)
09:00
Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT (abstract)
09:30
In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (abstract)
10:00
Cops-Robber games and the resolution of Tseitin formulas (abstract)
09:00-10:00 Session 60G: SC^2 Invited speaker (SCSC)
09:00
Hard Combinatorial Problems: A Challenge for Satisfiability (abstract)
10:00-10:40 Session 61 (LICS)
Location: Maths LT1
10:00
A sequent calculus with dependent types for classical arithmetic (abstract)
10:20
On Higher Inductive Types in Cubical Type Theory (abstract)
10:05-10:30 Session 62: Extended Abstracts (SCSC)
10:05
EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (abstract)
10:30-11:00Coffee Break
10:50-12:30 Session 63A: Formal Synthesis (ADHS)
10:50
Optimal Symbolic Controllers Determinization for BDD storage. (abstract)
11:15
Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games (abstract)
11:40
Compositional Abstraction-based Synthesis for Cascade Discrete-Time Control Systems (abstract)
12:05
Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings (abstract)
10:50-12:30 Session 63B: Switched Systems 1 (ADHS)
10:50
Language constrained stabilization of discrete- time switched linear systems: an LMI approach (abstract)
11:15
A switched system approach to optimize mixing of fluids (abstract)
11:40
Stability of switched systems on non-uniform time domains with non commuting matrices (abstract)
12:05
On invariance and reachability on semialgebraic sets for linear dynamics (abstract)
11:00-12:00 Session 64A: CSF Invited Talk: Catuscia Palamidessi (CSF)
Location: Maths LT2
11:00
Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility (abstract)
11:00-12:30 Session 64B: Rewriting (FSCD)
11:00
Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (abstract)
11:30
Completion for Logically Constrained Rewriting (abstract)
12:00
Completeness of Tree Automata Completion (abstract)
11:00-12:30 Session 64C (ITP)
Location: Blavatnik LT1
11:00
Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (abstract)
11:30
HOL Light QE (abstract)
12:00
Tactics and Certificates in Meta Dedukti (abstract)
11:00-12:40 Session 64D (LICS)
Chair:
Location: Maths LT1
11:00
Weighted model counting beyond two-variable logic (abstract)
11:20
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (abstract)
11:40
Unary negation fragment with equivalence relations has the finite model property (abstract)
12:00
Satisfiability in multi-valued circuits (abstract)
12:20
Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (abstract)
11:00-12:40 Session 64E (LICS)
Location: Maths LT3
11:00
Dialectica models of type theory (abstract)
11:20
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (abstract)
11:40
A Fixpoint Logic and Dependent Effects for Temporal Property Verification (abstract)
12:00
Computability Beyond Church-Turing via Choice Sequences (abstract)
12:20
The Syntax and Semantics of Quantitative Type Theory (abstract)
11:00-12:40 Session 64G: Extended Abstracts: Symbolic Computation (SCSC)
11:00
EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (abstract)
11:25
EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square (abstract)
11:50
EA: SMT-like Queries in Maple (abstract)
12:15
EA: Techniques for Natural-style Proofs in Elementary Analysis (abstract)
12:00-12:30 Session 65A: Privacy (CSF)
Location: Maths LT2
12:00
Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (abstract)
12:30-14:00Lunch Break
14:00-15:40 Session 66B: Applications 1 (ADHS)
14:00
Benchmarks for Cyber-Physical Systems: A Modular Model Library for Building Automation Systems (abstract)
14:25
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation (abstract)
14:50
A controlled sewer system should be treated as a sampled data system with events (abstract)
15:15
Mission Planning for Multiple Vehicles with Temporal Specifications using UxAS (abstract)
14:00-15:40 Session 66C: Stochastic systems 1 (ADHS)
14:00
Temporal Logic Control of General Markov Decision Processes by Approximate Policy Refinement (abstract)
14:25
Interacting Particle System-Based Estimation of Reach Probability for a Generalized Stochastic Hybrid System (abstract)
14:50
Statistical Verification of PCTL Using Stratified Samples (abstract)
15:15
Approximate Abstractions of Markov Chains with Interval Decision Processes (abstract)
14:00-15:30 Session 66D: Research papers: CAD (SCSC)
14:00
RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics (abstract)
14:30
RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple (abstract)
15:00
RP: Evaluation of Equational Constraints for CAD in SMT Solving (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 67A: Electronic voting (CSF)
Chair:
Location: Maths LT2
16:00
Alethea: A Provably Secure Random Sample Voting Protocol (abstract)
16:30
Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (abstract)
16:00-17:00 Session 67B: FSCD Invited talk: Grigore Rosu (FSCD)
16:00
Formal Design, Implementation and Verification of Blockchain Languages (abstract)
16:00-18:00 Session 67C (ITP)
Location: Blavatnik LT1
16:00
Towards Formal Foundations for Game Theory (Short Paper) (abstract)
16:20
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (abstract)
16:40
Towards Verified Handwritten Calculational Proofs (Short Paper) (abstract)
17:00
Formalizing Ring Theory in PVS (Short Paper) (abstract)
17:20
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (abstract)
16:00-17:00 Session 67E: MUS (SAT)
16:00
Minimal unsatisfiability and minimal strongly connected digraphs (abstract)
16:30
Finding all Minimal Safe Inductive Sets (abstract)
16:00-17:30 Session 67F: Research papers (SCSC)
16:00
RP: Refutation of Products of Linear Polynomials (abstract)
16:30
RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification (abstract)
17:00
RP: Unknot Recognition Through Quantifier Elimination (abstract)
16:10-17:25 Session 68A: Verification (ADHS)
16:10
Sufficient Conditions for Temporal Logic Specifications in Hybrid Dynamical Systems (abstract)
16:35
Falsification of Temporal Logic Requirements Using Gradient Based Local Search in Space and Time (abstract)
17:00
Higher-Dimensional Timed Automata (abstract)
16:10-17:25 Session 68B: Stability (ADHS)
16:10
Compositional Analysis of Hybrid Systems Defined Over Finite Alphabets (abstract)
16:35
Razumikhin-type Theorems on Practical Stability of Dynamic Equations on Time Scales (abstract)
17:00
Switch induced instabilities for stable power system DAE models (abstract)
17:00-18:30 Session 69B: LICS Award Session & Martin Hofmann Memorial (LICS)
Chair:
Location: Maths LT1
17:00
LICS Awards: The Kleene Award and the Test of Time Award (abstract)
17:45
Remembering Martin Hofmann (abstract)
19:00-21:30 FLoC banquet at Examination Schools (FLoC)

FLoC banquet at Examination Schools. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).

Thursday, July 12th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 70A: Invited talk: Calin Belta (ADHS)
09:00
Formal Synthesis of Control Strategies for Dynamical Systems (abstract)
09:00-10:30 Session 70C (ITP)
Location: Blavatnik LT1
09:00
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (abstract)
09:30
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (abstract)
10:00
Verification of PCP-Related Computational Reductions in Coq (abstract)
09:00-10:40 Session 70D (LICS)
Location: Maths LT1
09:00
Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (abstract)
09:20
Logical paradoxes in quantum computation (abstract)
09:40
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (abstract)
10:00
Two complete axiomatisations of pure-state qubit quantum computing (abstract)
10:20
Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (abstract)
09:00-10:40 Session 70E (LICS)
Location: Maths LT3
09:00
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (abstract)
09:20
A Generalized Modality for Recursion (abstract)
09:40
A functional interpretation with state (abstract)
10:00
The Geometry of Computation-Graph Abstraction (abstract)
10:20
Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (abstract)
09:00-10:30 Session 70F (SMT)
09:00
Invited talk: Automating Separation Logics using SMT (abstract)
10:00
Revisiting Enumerative Instantiation (abstract)
09:30-10:30 Session 71: Side channels (CSF)
09:30
Symbolic Side-Channel Analysis for Probabilistic Programs (abstract)
10:00
Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (abstract)
10:30-11:00Coffee Break
10:50-12:30 Session 73A: Reachability and safety analysis (ADHS)
10:50
Reachability Analysis for One Dimensional Linear Parabolic Equation (abstract)
11:15
On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems (abstract)
11:40
T-Barrier Certificates: A Continuous Analogy to K-Induction (abstract)
12:05
Learning and Verification of Feedback Control Systems Using Feedforward Neural Networks (abstract)
10:50-12:30 Session 73B: Observation and Estimation (ADHS)
10:50
Optimization-Based Design of Bounded-Error Estimators Robust to Missing Data (abstract)
11:15
Observability of Linear Hybrid Systems with Unknown Inputs and Discrete Dynamics Modeled by Petri Nets (abstract)
11:40
On Approximate Predictability of Metric Systems (abstract)
12:05
Input Design for Nonlinear Model Discrimination Via Affine Abstraction (abstract)
11:00-12:30 Session 74A: Security protocols II (CSF)
Chair:
11:00
A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (abstract)
11:30
Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (abstract)
12:00
A Typing Result for Stateful Protocols (abstract)
11:00-12:30 Session 74B: Unification (FSCD)
11:00
Fixed-Point Constraints for Nominal Equational Unification (abstract)
11:30
Higher-Order Equational Pattern Anti-Unification (abstract)
12:00
Nominal Unification with Atom and Context Variables (abstract)
11:00-12:30 Session 74C (ITP)
Location: Blavatnik LT1
11:00
Verified Memoization and Dynamic Programming (abstract)
11:30
Fast Machine Words in Isabelle/HOL (abstract)
12:00
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms (abstract)
11:00-12:00 Session 74D: LICS Invited Talk: Val Tannen (LICS)
Chair:
Location: Maths LT1
11:00
Provenance Analysis for First-order Model Checking (abstract)
11:00-12:00 Session 74E: SMT (SAT)
11:00
Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (abstract)
11:30
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (abstract)
12:00-12:40 Session 75A (LICS)
Chair:
Location: Maths LT1
12:00
On computability and tractability for infinite sets (abstract)
12:20
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (abstract)
12:30-14:00Lunch Break
14:00-15:40 Session 76A: Optimal and model predictive control (ADHS)
14:00
Occupation Measure Methods for Modelling and Analysis of Biological Hybrid Systems (abstract)
14:25
Safety Control, a Quantitative Approach (abstract)
14:50
Computing Controlled Invariant Sets for Hybrid Systems with Applications to Model-Predictive Control (abstract)
15:15
Data-Driven Switched Affine Modeling for Model Predictive Control (abstract)
14:00-15:40 Session 76B: Networked systems (ADHS)
14:00
Network-Aware Design of State-Feedback Controllers for Linear Wireless Networked Control Systems (abstract)
14:25
Space-Time Budget Allocation for Marketing Over Social Networks (abstract)
14:50
Tracking Control via Variable-gain Integrator and Lookahead Simulation: Application to Leader-follower Multiagent Networks (abstract)
15:15
Hybrid System Modeling of Multi-Agent Coverage Problems with Energy Depletion and Repletion (abstract)
14:00-15:00 Session 76C: FSCD General Meeting (FSCD)

AGENDA of FSCD18 General Meeting

  1. Welcome by Steering Committee Chair, Luke Ong
  2. Report of FSCD18 PC Chair, Helene Kirchner
  3. Report of FSCD18 Conference Chair, Paula Severi
  4. Progress Report of FSCD19 - PC Chair: Herman Geuvers - Conference Chair: Jakob Rehof
  5. Election of two Steering Committee members
  6. Proposal to host FSCD20 (colocating with IJCAR2020) in Paris: Stefano Guerrini and Giulio Manzonetto
  7. AOB
  8. Handover to new SC Chair (2018-2021), Delia Kesner.
Chair:
14:00-15:40 Session 76E (LICS)
Location: Maths LT1
14:00
Computable decision making on the reals and other spaces via partiality and nondeterminism (abstract)
14:20
A Theory of Register Monitors (abstract)
14:40
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (abstract)
15:00
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (abstract)
15:20
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (abstract)
14:00-15:40 Session 76F (LICS)
Chair:
Location: Maths LT3
14:00
Probabilistic stable functions on discrete cones are power series. (abstract)
14:20
Allegories: decidability and graph homomorphisms (abstract)
14:40
Syntax and Semantics for Operations with Scopes (abstract)
15:00
Rewriting with Frobenius (abstract)
15:20
Ribbon tensorial logic (abstract)
14:00-15:30 Session 76G: Tools & Applications II (SAT)
14:00
ALIAS: A Modular Tool for Finding Backdoors for SAT (abstract)
14:30
PySAT: A Python Toolkit for Prototyping with SAT Oracles (abstract)
15:00
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (abstract)
14:00-15:30 Session 76H (SMT)
14:00
Invited talk: Verifying Learners and Learning Verifiers (abstract)
15:00
Puli - A Problem-Specific OMT Solver (abstract)
15:00-15:30 Session 77B (ITP)
Location: Blavatnik LT1
15:00
ProofWatch: Watchlist Guidance for Large Theories in E (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 78B (ITP)
Location: Blavatnik LT1
16:00
Verified Tail Bounds for Randomized Programs (abstract)
16:30
Verified Analysis of Random Binary Tree Structures (abstract)
16:00-17:30 Session 78E (SMT)
16:00
SMT-based Compile-time Verification of Safety Properties for Smart Contracts (abstract)
16:30
SMT Solving Modulo Tableau and Rewriting Theories (abstract)
17:00
Rewrites for SMT Solvers using Syntax-Guided Enumeration (abstract)
16:10-17:25 Session 79A: Applications 2 (ADHS)
16:10
Multi-Energy Scheduling Using a Hybrid Systems Approach (abstract)
16:35
Hierarchical Model Predictive Control for Building Energy Management of Hybrid Systems (abstract)
17:00
Verifying nonlinear analog and mixed-signal circuits with inputs (abstract)
16:10-17:25 Session 79B: Switched systems 2 (ADHS)
16:10
Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (abstract)
16:35
Symbolic Models for Incrementally Stable Switched Systems with Aperiodic Time Sampling (abstract)
17:00
Control Synthesis for Stochastic Switched Systems Using the Tamed Euler Method (abstract)
16:30-17:30 Session 80: Confluence (FSCD)
16:30
Decreasing diagrams with two labels are complete for confluence of countable systems (abstract)
17:00
Confluence of Prefix-Constrained Rewrite Systems (abstract)
17:00-17:45 Session 81B: Alonzo Church Award Session (LICS)
Location: Maths LT1
17:00
The 2018 Alonzo Church Award for Outstanding Contributions to Logic and Computation (abstract)
17:15
Constraints, Graphs, Algebra, Logic, and Complexity (abstract)
19:45-21:30 ADHS Banquet at Balliol College (ADHS)

The ADHS18 banquet will be at Balliol College, Oxford. Drinks reception from 7:45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).

Location: Balliol College
Friday, July 13th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 83A: Invited talk: Erika Abraham (ADHS)
09:00
Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems (abstract)
09:00-10:30 Session 83B: Program Verification (ADSL)
09:00
Resource semantics: substructural logic as a modelling technology (keynote) (abstract)
09:50
Automating the Flow Framework (abstract)
09:00-10:30 Session 83C: CAV Tutorial: Shaz Qadeer (part 1) (CAV)
Location: Maths LT3
09:00
Proving a concurrent program correct by demonstrating it does nothing (abstract)
09:00-10:30 Session 83D (FRIDA)
09:00
Building verified distributed systems with IVy (abstract)
09:30
The latest gossip on BFT consensus (abstract)
10:00
Formal Verification of Internet of Things Protocols (abstract)
09:00-10:30 Session 83E (HCVS)
09:00
Horn Clauses and Beyond for Relational and Temporal Program Verification (abstract)
10:00
Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (abstract)
09:00-10:30 Session 83F (LSB)
09:00
Pathway Logic: Symbolic executable models for reasoning about cellular processes (abstract)
09:00-10:30 Session 83G (LearnAut)
09:00
Algorithms for Weighted and Probabilistic Context-Free Grammars and Convex Optimization (abstract)
10:00
Learning Graph Weighted Models on Pictures (abstract)
09:00-10:30 Session 83H: Markov decision processes 1 (MoRe)
09:00
Conditioning and quantiles in Markovian models (abstract)
10:00
Multiple Objectives and Cost Bounds in MDP (abstract)
09:00-10:30 Session 83I: Applications (RCRA)
09:00
Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. (abstract)
09:22
Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (abstract)
09:44
Greedy Randomized Search for Scalable Compilation of Quantum Circuits (abstract)
10:06
Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (abstract)
09:00-10:30 Session 83J (SMT)
09:00
Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic (abstract)
10:00
Higher-Order SMT Solving (abstract)
09:00-10:30 Session 83K: Machine learning and logic (SoMLMFM)
Location: Maths LT1
09:00
Machine learning and logic: Fast and slow thinking (abstract)
09:30
Provably beneficial artificial intelligence (abstract)
10:00
Towards Robust and Explainable Artificial Intelligence (abstract)
09:00-10:30 Session 83L (Tetrapod)
Location: Maths L6
09:00
Modularity in Software Synthesis (abstract)
09:45
Modularity in Mathematical Computation (abstract)
09:00-10:30 Session 83M: UITP 1: Invited talk (UITP)
09:00
Designing Globular: formal proofs as geometrical objects (Invited Talk) (abstract)
10:00
Interfacing with a Prover using Focusing and Logic Programming (abstract)
09:00-10:30 Session 83N (VDMW)
Location: Blavatnik LT2
09:00
Model checking and its applications (abstract)
09:45
Computation and inference (abstract)
09:00-10:30 Session 83Q (rv4rise)
09:00
Hardware-based runtime verification with Tessla (abstract)
09:45
Real-time Stream Processing with RTLola (abstract)
09:30-10:30 Session 84A: Isabelle 1 (Isabelle)
Location: Blavatnik LT1
09:30
A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (abstract)
10:00
Lazy Algebraic Types in Isabelle/HOL (abstract)
10:30-11:00Coffee Break
10:50-12:05 Session 85: Stochastic systems 2 (ADHS)
10:50
Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach (abstract)
11:15
Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations (abstract)
11:40
Concentration of Measure for Chance-Constrained Optimization (abstract)
11:00-12:30 Session 86A: Proof Theory (ADSL)
11:00
Cyclic Theorem Prover for Separation Logic by Magic Wand (abstract)
11:30
Labelled Cyclic Proofs for Separation Logic (abstract)
12:00
A Complete Proof System for Basic Symbolic Heaps with Permissions (abstract)
11:00-12:30 Session 86B: CAV Tutorial: Shaz Qadeer (part 2) (CAV)
Location: Maths LT3
11:00
Proving a concurrent program correct by demonstrating it does nothing (continued) (abstract)
11:00-12:30 Session 86C (FRIDA)
11:00
Specifying Non-Atomic Methods of Concurrent Objects (abstract)
11:30
Peregrine - A Tool for Population Protocols (abstract)
12:00
From Asynchronous Message-Passing Models To Rounds (abstract)
11:00-12:30 Session 86D (HCVS)
11:00
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (abstract)
11:30
A simple functional presentation and an inductive correctness proof of the Horn algorithm (abstract)
12:00
Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (abstract)
11:00-12:30 Session 86E: Isabelle 2 (Isabelle)
Location: Blavatnik LT1
11:00
Formal Verification of Bounds for the LLL Basis Reduction Algorithm (abstract)
11:30
Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (abstract)
12:00
Further Scaling of Isabelle Technology (abstract)
11:00-12:30 Session 86F: LCC: Contributed Talks (LCC)
Location: Maths L5
11:00
Traversal-invariant definability and Logarithmic-space computation (abstract)
11:15
A recursion-theoretic characterisation of the positive polynomial-time functions (abstract)
11:30
Feasibly constructive proofs of succinct weak circuit lower bounds (abstract)
11:45
Computability over locally finite structures from algebra (abstract)
12:00
A General Equational Framework for Static Profiling of Parametric Resource Usage (abstract)
12:15
Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (abstract)
11:00-12:30 Session 86G (LSB)
11:00
Counterfactual resimulation for causal analysis of rule-based models (abstract)
11:45
Bio-curation and rule-based modelling of protein interaction networks in KAMI (abstract)
11:00-12:30 Session 86H (LearnAut)
11:00
Methods for learning weighted finite automata and their use in reinforcement learning (abstract)
12:00
Learning Tree Distributions by Hidden Markov Models (abstract)
11:00-12:30 Session 86I: Games and synthesis (MoRe)
11:00
Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives (abstract)
11:30
Parameterized complexity of games with monotonically ordered omega-regular objectives (abstract)
12:00
Comfort and Energy Optimization for Floor Heating Systems (abstract)
11:00-12:30 Session 86J: Logic (RCRA)
11:00
Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (abstract)
11:22
Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (abstract)
11:44
Algebraic Crossover Operators for Permutations (abstract)
12:06
An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (abstract)
11:00-12:30 Session 86K (SMT)
11:00
Centralizing Equality Reasoning in MCSAT (abstract)
11:30
Proofs in conflict-driven theory combination (abstract)
12:00
Selfless Interpolation for Infinite-State Model Checking (abstract)
11:00-12:30 Session 86L: Ethical and fair AI (SoMLMFM)
Location: Maths LT1
11:00
Ethically Aligned AI Systems (abstract)
11:30
Deep Learning Methods for Large Scale Theorem Proving (abstract)
12:00
AI2: AI Safety and Robustness with Abstract Interpretation (abstract)
11:00-12:30 Session 86M (Tetrapod)
Location: Maths L6
11:00
Modularity in Proof Assistants (abstract)
11:45
Discussion 1 (abstract)
11:00-12:30 Session 86N: UITP 2 (UITP)
11:00
Partial Regularization of First-Order Resolution Proofs (abstract)
11:30
Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned (abstract)
12:00
Automated Theorem Proving in a Chat Environment (abstract)
11:00-12:30 Session 86P (VDMW)
Location: Blavatnik LT2
11:00
Verification of infinite-state systems using decidable logic (abstract)
11:45
Should I join a startup? (abstract)
11:00-12:00 Session 86Q: Invited Talk (Vampire)
11:00
Counterexample-Guided Quantifier Instantiation in Logical Theories (abstract)
11:00-12:30 Session 86R (rv4rise)
11:00
Systematic analysis and improvement of CNNs. (abstract)
11:45
Formalizing Requirements for Cyber-Physical Systems: Real-World Experiences and Challenges (abstract)
12:30-14:00Lunch Break
14:00-15:15 Session 87A: Control Synthesis (ADHS)
14:00
Algorithm for Bernstein Polynomial Control Design (abstract)
14:25
Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters (abstract)
14:50
An Interval-Based Sliding Horizon Motion Planning Method (abstract)
14:00-15:50 Session 87B: Weak Memory and Complexity (ADSL)
14:00
Weak memory made easy by separation logic (keynote) (abstract)
14:50
On the Complexity of Pointer Arithmetic in Separation Logic (abstract)
15:20
The Complexity of Prenex Separation Logic with One Selector (abstract)
14:00-15:30 Session 87C: CAV Tutorial: Matteo Maffei (CAV)
Location: Maths LT3
14:00
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts (abstract)
14:00-15:30 Session 87D (FRIDA)
14:00
Specifying and Verifying Concurrent Objects (abstract)
14:30
Making Parallel Snapshot Isolation Serializable (abstract)
15:00
Parameterized Reachability for All Flavors of Threshold Automata (abstract)
14:00-15:30 Session 87E (HCVS)
14:00
Tree dimension in verification of constrained Horn clauses (abstract)
15:00
Declarative Parameterized Verification of Topology-sensitive Distributed Protocols (abstract)
14:00-15:30 Session 87F: LCC: Martin Hofmann Memorial Session (LCC)
Location: Maths L5
14:00
Characterizing Complexity Classes in Presence of Higher-Order Functions — How Martin Hofmann Contributed to Shaping ICC (abstract)
15:00
Static Prediction of Heap Space Usage for First-Order Functional Programs -- A Retrospective on my First Paper with Martin Hofmann (abstract)
14:00-15:30 Session 87G (LSB)
Chair:
14:00
A logical framework for systems biology and biomedicine (abstract)
14:45
Introducing iota, a logic for biological modelling (abstract)
14:00-15:30 Session 87H (LearnAut)
14:00
Weak and Strong learning of Probabilistic Context-Free Grammars: theoretical and empirical perspectives (abstract)
15:00
Decision problems for Clark-congruential languages (abstract)
14:00-15:30 Session 87I: Timed and hybrid systems (MoRe)
14:00
A journey through negatively-weighted timed games: undecidability, decidability, approximability (abstract)
15:00
Stochastic o-minimal hybrid systems (abstract)
14:00-15:30 Session 87J: Constraint Satisfiability (RCRA)
14:00
Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns (abstract)
14:22
Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems (abstract)
14:44
Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited (abstract)
15:06
On the Configuration of SAT Formulae (abstract)
14:00-15:30 Session 87K (SMT)
14:00
Discovering Universally Quantified Solutions for Constrained Horn Clauses (abstract)
14:30
What is the Point of an SMT-LIB Problem? (abstract)
15:00
SMT-COMP 2018 Report (abstract)
14:00-15:30 Session 87L: Applications of AI (SoMLMFM)
Location: Maths LT1
14:00
The realities of applied AI (abstract)
14:30
Safe reinforcement learning via formal methods (abstract)
15:00
Programming from examples: PL meets ML (abstract)
14:00-15:30 Session 87M (Tetrapod)
Location: Maths L6
14:00
Modularity in Proof Checking (abstract)
14:45
Modularity in Large Proofs (abstract)
14:00-15:30 Session 87P (VDMW)
Location: Blavatnik LT2
14:00
How to get a paper accepted? (abstract)
14:30
How to attend a conference? (abstract)
15:00
Hands-on: Elevator pitch (abstract)
14:00-15:30 Session 87Q: Contributed Talks (Vampire)
14:00
Towards Word Sense Disambiguation by Reasoning (abstract)
14:30
Testing ATP folklore: a statistical analysis of Vampire proofs. (abstract)
15:00
Foundations of SPECTRE (abstract)
14:00-15:30 Session 87R (rv4rise)
14:00
Signal classification using temporal logic (abstract)
14:45
First order temporal properties of continuous signals (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 88A (FRIDA)
16:00
Stateless model-checking under the data-centric view (abstract)
16:30
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction (abstract)
16:00-18:00 Session 88C: Isabelle 4 (Isabelle)
Location: Blavatnik LT1
16:00
Substitutionless First-Order Logic: A Formal Soundness Proof (abstract)
16:15
The remote_build Tool (abstract)
16:30
PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (abstract)
17:00
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (abstract)
16:00-18:00 Session 88D: LCC: Martin Hofmann Memorial Session (LCC)
Location: Maths L5
16:00
My Journey through Observational Equivalence Research with Martin Hofmann (abstract)
16:30
Memories of Martin (abstract)
16:00-18:00 Session 88E (LSB)
Chair:
16:00
A logic modelling workflow for systems pharmacology (abstract)
16:00-17:30 Session 88F (LearnAut)
16:00
The Learnability of Symbolic Automata (abstract)
16:30
Toward Learning Boolean Functions from Positive Examples (abstract)
17:00
Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches (abstract)
16:00-18:00 Session 88G: Markov decision processes 2 (MoRe)
16:00
Multi-Scenario Uncertainty in Markov Decision Processes (abstract)
16:30
Safe and Optimal Scheduling of Hard and Soft Tasks (abstract)
17:00
Logically-Constrained Reinforcement Learning (abstract)
16:00-16:40 Session 88I: Explainable machine learning (SoMLMFM)
Location: Maths LT1
16:00
Influence-directed explanations for machine learning systems (abstract)
16:20
Safety verification for deep neural networks with provable guarantees (abstract)
16:00-17:00 Session 88K (VDMW)
Chair:
Location: Blavatnik LT2
16:00
Learning from failure (abstract)
16:00-17:30 Session 88L: Contributed Talks (Vampire)
16:00
Experimenting with Theory Instantiation in Vampire (abstract)
16:30
Giving AVATAR Quantifiers to Play With (abstract)
17:00
Developments in Higher-order Theorem proving within Vampire (abstract)
16:00-18:00 Session 88M (rv4rise)
16:00
Using the F1/10 Autonomous Racing Platform for Runtime Verification Research (abstract)
16:10-18:00 Session 89: Small Models and SL-COMP (ADSL)
Chair:
16:10
Sloth: Separation Logic and Theories via Small Models (abstract)
16:40
Presentation of Results from SL-COMP 2018 (abstract)
16:30-18:00 Session 90: Talks in memoriam Mike Gordon (CAV)
Location: Maths LT3
16:30
Proof Scripting from HOL to Goaled (abstract)
17:00
HOL Developed and HOL Used: Interconnected Stories of Real-World Applications (abstract)
17:30
From Processor Verification Upwards (abstract)
16:40-18:00 Session 91: Panel Session & Summary (SoMLMFM)

Panel session preceded by an introductory talk.

Location: Maths LT1
16:40
What Just Happened in AI (abstract)
17:00
Panel session (abstract)
19:00-21:30 Workshops dinner at Keble College (FLoC)

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

Location: Keble College
Saturday, July 14th

View this program: with abstractssession overviewtalk overview

10:00-10:30 Session 94A: Program verification (F-IDE)
10:00
Lightweight Interactive Proving inside an Automatic Program Verifier (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 95A: Model Checking (CAV)
Location: Maths LT1
11:00
Propositional Dynamic Logic for Higher-Order Functional Programs (abstract)
11:15
Syntax-Guided Termination Analysis (abstract)
11:30
Model Checking Quantitative Hyperproperties (abstract)
11:45
Exploiting Synchrony and Symmetry in Relational Verification (abstract)
12:00
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (abstract)
12:15
Eager Abstraction for Symbolic Model Checking (abstract)
11:00-12:30 Session 95B: DS-FM invited talk: Sylvain Conchon (DS-FM)
Location: Blavatnik LT1
11:00
Cubicle: a model checker for parameterized array-based transition systems (abstract)
11:45
Heuristic-Based GR(1) Assumptions Refinement (abstract)
11:00-12:30 Session 95C: User interfaces for formal tools (F-IDE)
11:00
User Support for the Combinator Logic Synthesizer Framework (abstract)
11:30
AsmetaF: a flattener for the ASMETA framework (abstract)
12:00
Improving the Visualization of Alloy Instances (abstract)
11:00-12:30 Session 95D: Ally Skills (FLoC)

"Allies" are people who support a group who are commonly the subject of discrimination or prejudice, but who are not members of that group. The Ally Skills session teaches simple everyday ways for allies to use their privilege and influence to support people who are targets of systemic oppression in their workplaces and communities. This includes women of all races, people of color, people with disabilities, LGBTQ folks, parents, caregivers of all sorts, and people of different ages.

The format of the session will be some introductory material, followed by group-based discussion of several scenarios. All are welcome, hope to see you there!

Any questions, please contact Stephen Chong <chong@seas.harvard.edu> and Alexandra Silva <alexandra.silva@ucl.ac.uk>.

Location: Blavatnik LT2
11:00-12:30 Session 95E: Foundations I (ICLP)
11:00
Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (abstract)
11:30
Shared aggregate sets in answer set programming (abstract)
12:00
Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs (abstract)
11:00-12:30 Session 95F: SMT 1 (IJCAR)
Location: Maths LT2
11:00
Efficient Interpolation for the Theory of Arrays (abstract)
11:30
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (abstract)
12:00
A Generic Framework for Implicate Generation Modulo Theories (abstract)
11:00-12:30 Session 95G: Overture: Tools and Applications (Overture)

The session contains two papers focuses on tool support for VDM in Overture and two papers on applications.

Chair:
11:00
Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (abstract)
11:20
ViennaVM: a Virtual Machine for VDM-SL development (abstract)
11:40
Multi-modelling of Cooperative Swarms (abstract)
12:00
Design Space Exploration for Secure Building Control (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 96A: CAV Invited Talk: Eran Yahav (CAV)
Location: Maths LT1
14:00
From Programs to interpretable Deep Models, and Back (abstract)
14:00-15:30 Session 96B (DS-FM)
Location: Blavatnik LT1
14:00
Analysis and Verification of Message Passing based Parallel Programs (abstract)
14:30
Formal verification of neural networks (abstract)
15:00
Consistency Checking of Functional Requirements (abstract)
14:00-15:30 Session 96D: Foundations II (ICLP)
14:00
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (abstract)
14:30
First-order answer set programming as constructive proof search (abstract)
15:00
Solving Horn Clauses on Inductive Data Types Without Induction (abstract)
14:00-15:30 Session 96E: SAT Extensions & Applications (IJCAR)
Location: Maths LT2
14:00
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (abstract)
14:30
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (abstract)
15:00
A New Probabilistic Algorithm for Approximate Model Counting (abstract)
14:50-15:30 Session 97: Overture: Perspectives and Methods (Overture)

This session focuses on methodology and prespectives on the use of the Overture tools in practice.

14:50
Transforming an industrial case study from VDM++ to VDM-SL (abstract)
15:10
Integrating VDM-SL into the continuous delivery pipelines of cloud-based software (abstract)
15:00-15:30 Session 98A: Polyhedra (CAV)
Location: Maths LT1
15:00
Fast Numerical Program Analysis with Reinforcement Learning (abstract)
15:15
A Direct Encoding for NNC Polyhedra (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 99A: Synthesis (CAV)
Location: Maths LT1
16:00
What’s hard about Boolean Functional Synthesis? (abstract)
16:15
Synthesis Modulo Theories (abstract)
16:30
Synthesizing Reactive Systems from Hyperproperties (abstract)
16:45
Reactive Control Improvisation (abstract)
17:00
Constraint-Based Synthesis of Coupling Proofs (abstract)
17:15
Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (abstract)
17:30
Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (abstract)
17:45
Syntax Guided Synthesis with Quantitative Syntactic Objectives (abstract)
16:00-16:30 Session 99B (DS-FM)
Location: Blavatnik LT1
16:00
A Formal Study of MANET Routing Protocols (abstract)
16:00-18:00 Session 99C: Integrating formal verification results (F-IDE)
16:00
Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents (abstract)
16:30
A Notebook Format for the Holistic Design of Embedded Systems (abstract)
17:00
The CLEAR Way To Transparent Formal Methods (abstract)
17:30
Integrating user design and formal models within PVSio-Web (abstract)
16:00-18:00 Session 99D: Formal Methods in Industry (FLoC)
Location: Maths LT3
16:00
Amazon’s Automated Reasoning Group: Combining Amazon’s 14 foundational principles with the Strachey philosophy (abstract)
16:30
Formal Reasoning and the Hacker Way (abstract)
17:00
Business Perspective on Software Analysis (abstract)
16:00-17:00 Session 99F: Tools and Rewriting (IJCAR)
Location: Maths LT2
16:00
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (abstract)
16:30
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (abstract)
16:45
Efficient Model Construction for Horn Logic with VLog: System Description (abstract)
16:00-18:00 Session 99G: Overture: the Workshop part (Overture)

This session will be used to host a structured brainstorm on the future of Overture, from the perspective of the notation and semantics, tool support, applications, community building and exploitation.

16:00
The Overture Strategic Research Agenda (abstract)
17:00-18:00 Session 100A: ASP Extensions (ICLP)
17:00
Constraint Answer Set Programming without Grounding (abstract)
17:30
Translating LPOD and CR-Prolog2 into Standard Answer Set Programs (abstract)
17:00-18:00 Session 100B: Awards (IJCAR)
  • Presentation of the IJCAR 2018 Best Paper Award
  • Presentation of the 2018 Woodie Bledsoe Student Travel Awards
  • Presentation of the Herbrand Award for Distinguished Contributions to Automated Reasoning to Bruno Buchberger
    • Presentation by the awardee: Automated Mathematical Invention: Would Gröbner Need a PhD Student Today?
Location: Maths LT2
19:00-21:30 FLoC reception at Oxford Town Hall (FLoC)

FLoC reception at Oxford Town Hall. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).

Sunday, July 15th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 101B (FM)
Location: Maths LT2
09:00
Deadlock Detection for Actor-based Coroutines (abstract)
09:30
An Algebraic Approach for Reasoning About Information Flow (abstract)
10:00
Towards `Verifying' a Water Treatment System (abstract)
09:00-10:00 Session 101C: ICLP Invited Talk: Elvira Albert (ICLP)
Chair:
09:00
Avoiding redundancies in the exploration of concurrent programs (abstract)
09:00-10:30 Session 101D: Logics and Calculi (IJCAR)
Location: Blavatnik LT1
09:00
A Resolution-Based Calculus for Preferential Logics (abstract)
09:30
Enumerating Justifications using Resolution (abstract)
10:00
A Tableaux Calculus for Reducing Proof Size (abstract)
09:00-10:30 Session 101E: SAT (IJCAR)
Location: Blavatnik LT2
09:00
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (abstract)
09:30
Extended Resolution Simulates DRAT (abstract)
10:00
A SAT-Based Approach to Learn Explainable Decision Sets (abstract)
09:10-10:00 Session 102: CAV Award (CAV)

The CAV 2018 Award is given to: SAT-based and Bounded Model Checking

  • Armin Biere
  • Alessandro Cimatti
  • Edmund M. Clarke
  • Daniel Kroening
  • Flavio Lerda
  • Yunshan Zhu

Bounded Model Checking has revolutionized the way model checking is used and perceived. It has increased the capabilities of model checkers by orders of magnitude, turning them into a standard tool for hardware verification and a very important component of the toolkit available for software verification. BMC changed the focus of model checking from full verification to bug-finding.  The BMC problem is defined as follows: Given a bound k, is there an erroneous computation of the system of length k?  This problem is transformed to a Boolean formula that is satisfiable if and only if the system includes a computation of length k, which violates the specification. Focusing on the bounded problem enabled the authors to exploit the progress that was made in SAT solving around the same time, and simultaneously to bootstrap the tremendous progress in satisfiability solving that we have seen since. While early implementation of BMC focused on hardware, CBMC has demonstrated how it can be applied to realistic programs written in C. The ability to apply verification directly to C programs gave an enormous boost to a very large spectrum of applications in hardware and software industry and in academic research. The application areas include error explanation and localization, concurrent programs, equivalence checking, cyber-physical systems and control systems, test vector generation, worst-case execution time, security, and many other practical applications.

Location: Maths LT1
10:00-10:30 Session 103A: Learning (CAV)
Location: Maths LT1
10:00
Learning Abstractions for Program Synthesis (abstract)
10:15
The Learnability of Symbolic Automata (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 104A: Runtime Verification, Hybrid and Timed Systems (CAV)
Location: Maths LT1
11:00
Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (abstract)
11:15
Spacetime Interpolants (abstract)
11:30
Monitoring Weak Consistency (abstract)
11:45
Monitoring CTMCs By Multi-Clock Timed Automata (abstract)
12:00
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (abstract)
12:15
A Counting Semantics for Monitoring LTL Specifications over Finite Traces (abstract)
11:00-12:00 Session 104B: FM Invited Talk: Annabelle McIver (FM)
Location: Maths LT2
11:00
Privacy in Text Processing: An information flow perspective (abstract)
11:00-12:30 Session 104C: Implementation I (ICLP)
11:00
Top-down and Bottom-up Evaluation Procedurally Integrated (abstract)
11:30
Certified Graph View Maintenance with Regular Datalog (abstract)
12:00
An iterative approach to precondition inference using constrained Horn clauses (abstract)
11:00-12:30 Session 104D: Formal Proofs (IJCAR)
Location: Blavatnik LT1
11:00
Constructive Decision via Redundancy-free Proof-Search (abstract)
11:30
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (abstract)
12:00
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (abstract)
11:00-12:30 Session 104E: SMT 2 (IJCAR)
Location: Blavatnik LT2
11:00
Exploring Approximations for Floating-Point Arithmetic using UppSAT (abstract)
11:30
Datatypes with Shared Selectors (abstract)
12:00
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 106A: Tools (CAV)
Chair:
Location: Maths LT1
14:00
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (abstract)
14:15
Strix: Explicit Reactive Synthesis Strikes Back! (abstract)
14:30
BTOR2, BtorMC and Boolector 3.0 (abstract)
14:45
Nagini: A Static Verifier for Python (abstract)
15:00
Peregrine: A Tool for the Analysis of Population Protocols (abstract)
15:15
ADAC: Automated Design of Approximate Circuits (abstract)
14:00-15:30 Session 106C: Learning and Reasoning (ICLP)
14:00
Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (abstract)
14:30
Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (abstract)
15:00
A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (abstract)
14:00-15:00 Session 106D: IJCAR Invited Talk: Martin Giese (IJCAR)
Location: Blavatnik LT1
14:00
Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 108A: Probabilistic Systems (CAV)
Location: Maths LT1
16:00
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (abstract)
16:15
Sound Value Iteration (abstract)
16:30
Safety-Aware Apprenticeship Learning (abstract)
16:45
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (abstract)
16:00-18:00 Session 108B (FM)
Location: Maths LT2
16:00
Producing Explanations for Rich Logics (abstract)
16:30
The Compound Interest in Relaxing Punctuality (abstract)
17:00
IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (abstract)
17:30
Timed Epistemic Knowledge Bases for Social Networks (abstract)
16:00-18:00 Session 108C: Technical Communications I (ICLP)
16:00
Cumulative Scoring-based Induction of Default Theories (abstract)
16:15
Epistemic Logic Programs with World View Constraints (abstract)
16:30
SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (abstract)
16:45
Introspecting Preferences In Answer Set Programming (abstract)
17:00
Application of Logic-Based Methods to Machine Component Design (abstract)
17:15
Improving Candidate Quality of Probabilistic Logic Models (abstract)
17:30
Natural Language Generation From Ontologies: Application Paper (abstract)
17:45
MASP-Reduce: a proposal for distributed computation of stable models (abstract)
16:00-18:00 Session 108D: Logics, Frameworks and Proofs (IJCAR)
Location: Blavatnik LT1
16:00
From Syntactic Proofs to Combinatorial Proofs (abstract)
16:30
A Logical Framework with Commutative and Non-Commutative Subexponentials (abstract)
17:00
Uniform Substitution for Differential Game Logic (abstract)
17:30
Theories as Types (abstract)
16:00-18:00 Session 108E: Verification (IJCAR)
Location: Blavatnik LT2
16:00
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (abstract)
16:30
A FOOLish Encoding of the Next State Relations of Imperative Programs (abstract)
17:00
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (abstract)
17:30
A Why3 framework for reflection proofs and its application to GMP's algorithms (abstract)
Monday, July 16th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 110A: Tools (CAV)
Location: Maths LT1
09:00
Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (abstract)
09:15
MaxSMT-Based Type Inference for Python 3 (abstract)
09:30
The JKind Model Checker (abstract)
09:45
The DEEPSEC prover (abstract)
10:00
SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (abstract)
10:15
StringFuzz: A Fuzzer for String Solvers (abstract)
09:00-10:30 Session 110C: Language and Reasoning (ICLP)
Location: Blavatnik LT2
09:00
An ASP Methodology for Understanding Narratives about Stereotypical Activities (abstract)
09:30
Specifying and Verbalising Answer Set Programs in Controlled Natural Language (abstract)
10:00
Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (abstract)
09:00-10:30 Session 110D: Decidability & Complexity (IJCAR)
Location: Maths LT2
09:00
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (abstract)
09:30
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (abstract)
10:00
Focussing, MALL and the polynomial hierarchy (abstract)
10:00-10:30 Session 111 (FM)
Location: Blavatnik LT1
10:00
Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 112B (FM)
Chair:
Location: Blavatnik LT1
11:00
Encoding fairness in a synchronous concurrent program algebra (abstract)
11:30
A wide-spectrum language for verification of programs on weak memory models (abstract)
12:00
Operational Semantics of a Weak Memory Model with Channel Synchronization (abstract)
11:00-12:30 Session 112C (FM)
11:00
Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (abstract)
11:30
Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (abstract)
12:00
Verifying Auto-Generated C Code from Simulink (abstract)
11:00-12:30 Session 112E: Superposition (IJCAR)
Location: Maths LT2
11:00
Superposition with Datatypes and Codatatypes (abstract)
11:30
Superposition for Lambda-Free Higher-Order Logic (abstract)
12:00
Efficient encodings of first-order Horn formulas in equational logic (abstract)
12:00-12:30 Session 114: Static Analysis (CAV)
Location: Maths LT1
12:00
Permission Inference for Array Programs (abstract)
12:15
Program Analysis is Harder than Verification: A Computability Perspective (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 115: FLoC Plenary Lecture: Byron Cook (FLoC)
Location: Maths LT1
14:00
Formal Reasoning about the Security of Amazon Web Services (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 116A: Oxford Union Debate: Ethics & Morality of Robotics (FLoC)

Public debate on "Ethics & Morality of Robotics" with panelists specializing in ethics, law, computer science, data security and privacy:

  • Prof Matthias Scheutz, Dr Sandra Wachter, Prof Jeannette Wing, Prof Francesca Rossi, Prof Luciano Floridi & Prof Ben Kuipers

See http://www.floc2018.org/public-debate/ for further details and to register.

Location: Oxford Union
16:00-18:00 Session 116B (FM)
Location: Blavatnik LT1
16:00
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (abstract)
16:30
Modular Verification of Programs with Effects and Effect Handlers in Coq (abstract)
17:00
Combining Tools for Optimization and Analysis of Floating-Point Computations (abstract)
17:30
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (abstract)
16:00-18:00 Session 116C (FM)
16:00
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (abstract)
16:30
Multi-Robot LTL Planning Under Uncertainty (abstract)
17:00
Vector Barrier Certificates and Comparison Systems (abstract)
17:30
Timed Vacuity (abstract)
19:00-21:30 FLoC banquet at Ashmolean Museum (FLoC)

FLoC banquet at Ashmolean Museum. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).

Tuesday, July 17th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 118A: Theory and Security (CAV)
Location: Maths LT1
09:00
Automata vs Linear-Programming Discounted-Sum Inclusion (abstract)
09:15
Model checking indistinguishability of randomized security protocols (abstract)
09:30
Lazy Self-Composition for Security Verification (abstract)
09:45
SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (abstract)
10:00
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (abstract)
10:15
Attracting Tangles to Solve Parity Games (abstract)
09:00-10:30 Session 118B (FM)
Location: Blavatnik LT1
09:00
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (abstract)
09:30
Dynamic Symbolic Verification of MPI Programs (abstract)
10:00
To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation (abstract)
09:00-10:30 Session 118C: FM I-Day (FM)
09:00
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (abstract)
09:30
Interlocking Design Automation using Prover Trident (abstract)
10:00
Model-Based Testing for Avionics Systems (abstract)
09:00-10:00 Session 118E: IJCAR Invited Talk: Erika Abraham (IJCAR)
Location: Maths LT2
09:00
Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics (abstract)
10:00-10:30 Session 119: SMT 3 (IJCAR)
Location: Maths LT2
10:00
A Separation Logic with Data: Small Models and Automation (abstract)
10:30-11:00Coffee Break
11:00-12:15 Session 120A: SAT, SMT and Decision Procedures (CAV)
Location: Maths LT1
11:00
Delta-Decision Procedures for Exists-Forall Problems over the Reals (abstract)
11:15
Solving Quantified Bit-Vectors using Invertibility Conditions (abstract)
11:30
Understanding and Extending Incremental Determinization for 2QBF (abstract)
11:45
The Proof Complexity of SMT Solvers (abstract)
12:00
Model Generation for Quantified Formulas: A Taint-Based Approach (abstract)
11:00-12:30 Session 120C: Applications (ICLP)
Location: Blavatnik LT2
11:00
Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming (abstract)
11:30
Experimenting with robotic intra-logistics domains (abstract)
12:00
Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (abstract)
11:00-12:30 Session 120D: AR Miscellanea (IJCAR)
Location: Maths LT2
11:00
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (abstract)
11:30
Automated Reasoning about Key Sets (abstract)
12:00
An abstraction-refinement framework for reasoning with large theories (abstract)
12:00-12:30 Session 121 (FM)
Location: Blavatnik LT1
12:00
View abstraction for systems with component identities (abstract)
12:30-14:00Lunch Break
14:00-15:15 Session 122A: Concurrency (CAV)
Location: Maths LT1
14:00
Partial Order Aware Concurrency Sampling (abstract)
14:15
Reasoning About TSO Programs Using Reduction and Abstraction (abstract)
14:30
Quasi-Optimal Partial Order Reduction (abstract)
14:45
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (abstract)
15:00
Constrained Dynamic Partial Order Reduction (abstract)
14:00-15:30 Session 122B (FM)
Location: Blavatnik LT1
14:00
Compositional Reasoning for Shared-variable Concurrent Programs (abstract)
14:30
Statistical Model Checking of LLVM Code (abstract)
15:00
A lightweight deadlock analysis technique of object-oriented programs (abstract)
14:00-15:30 Session 122C: FM I-Day (FM)
14:00
Software Safety and Security and AI (abstract)
14:30
Variant Analysis with QL (abstract)
15:00
Object-Oriented Security Proofs (abstract)
14:00-15:30 Session 122D: Probabilistic and Constraint LP (ICLP)
Chair:
Location: Blavatnik LT2
14:00
Shape Neutral Analysis of Graph-based Data-structures (abstract)
14:30
A Probabilistic Extension of Action Language BC+ (abstract)
15:00
Constraint-Based Inference in Probabilistic Logic Programs (abstract)
14:00-15:30 Session 122E: System Descriptions (IJCAR)
Chair:
Location: Maths LT2
14:00
The Higher-Order Prover Leo-III (abstract)
14:15
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (abstract)
14:30
Cubicle-W: Parameterized Model Checking on Weak Memory (abstract)
14:45
MaedMax: A Maximal Ordered Completion Tool (abstract)
15:00
Cops and CoCoWeb: Infrastructure for Confluence Tools (abstract)
15:15
FORT 2.0 (abstract)
15:30-16:00Coffee Break
16:00-17:45 Session 123A: CPS, Hardware, Industrial Applications (CAV)
Location: Maths LT1
16:00
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (abstract)
16:15
Continuous formal verification of Amazon s2n (abstract)
16:30
Symbolic Liveness Analysis of Real-World Software (abstract)
16:45
Model Checking Boot Code from AWS Data Centers (abstract)
17:00
Android Stack Systems (abstract)
17:15
Formally Verified Montgomery Multiplication (abstract)
17:30
Inner and Outer Approximating Flowpipes for Delay Differential Equations (abstract)
16:00-18:00 Session 123B (FM)
Location: Blavatnik LT1
16:00
CompoSAT: Specification-Guided Coverage for Model Finding (abstract)
16:30
Approximate Partial Order Reduction (abstract)
17:00
SDN-Actors: Modeling and Verification of SDN Programs (abstract)
17:30
Formal Specification and Verification of Dynamic Parametrized Architectures (abstract)
16:00-17:30 Session 123C: FM I-Day (FM)
16:00
Z3 and SMT in Industrial R&D (abstract)
16:30
Evidential and Continuous Integration of Software Verification Tools (abstract)
17:00
Disruptive Innovations for the Development and the Deployment of Fault-Free Software (abstract)
16:00-16:30 Session 123D: Doctoral Consortium teaser talks (ICLP)

The session hosts 3 minutes summaries by each Doctoral Consortium Ph.D. student who will give the longer presentation during the ICLP-DC on 18th of July.

Chair:
Location: Blavatnik LT2
16:30-18:00 Session 124: Technical Communications II (ICLP)
Location: Blavatnik LT2
16:30
Towards Static Performance Guarantees for Programs with Run-time Checks (abstract)
16:45
Towards Incremental and Modular Context-sensitive Analysis (abstract)
17:00
Learning Commonsense Knowledge through Interactive Dialogue (abstract)
17:15
A New Proof-theoretical Linear Semantics for CHR (abstract)
17:30
CHRvis: Syntax and Semantics (abstract)
17:45
Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability (abstract)
Wednesday, July 18th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 125A: ARQNL Invited Talk: Larry Moss (ARQNL)
09:00
Automated Reasoning In Natural Language: Current Directions (abstract)
09:00-10:30 Session 125B (ASPOCP)
09:00
Invited Talk: Optimization Problems in Answer Set Programming (abstract)
10:00
anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report) (abstract)
09:00-10:30 Session 125C: Invited talk: Michael Tautschnig (AVOCS)

Formal Methods at Amazon Web Services

09:00
Formal Methods at Amazon Web Services (abstract)
09:00-10:30 Session 125D (ICLP-DC)
Chair:
Location: Maths L6
09:00
Proof-relevant resolution for elaboration of programming languages (abstract)
09:30
Explaining Actual Causation via Reasoning about Actions and Change (abstract)
10:00
Probabalistic Action Language pBC+ (abstract)
09:00-10:30 Session 125E: Logic and Practice of Programming (LPOP)
09:00
Opening and introduction (abstract)
09:10
Invited Talk: Practical uses of Logic, Formal Methods, B and ProB (abstract)
09:50
Invited Talk: On the Development of Industrial Applications with ASP (abstract)
09:00-10:30 Session 125F: Practical MSO Model Checking 1 (LaSh)
09:00
Monadic Second-Order Model Checking with Fly-Automata (abstract)
10:05
Lazy Automata Techniques for WS1S (abstract)
09:00-10:30 Session 125G (MLP)
Location: Blavatnik LT1
09:00
Opening and demos (abstract)
09:45
Bimodal Software Engineering (abstract)
09:00-10:30 Session 125H: Industrial Session (NSV)
09:00
Needs in formal methods for the validation of naval systems (abstract)
09:45
Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering (abstract)
09:00-10:30 Session 125I: Parallel graph algorithms (PLR)

On parallel algorithms working with graphs.

Chair:
09:00
Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications (abstract)
09:45
MASP-Reduce: a proposal for distributed computation of stable models (abstract)
09:00-10:30 Session 125J (REFINE)
Location: Blavatnik LT2
09:00
Automated verification of linearizability (abstract)
10:00
Correctness of Concurrent Objects under Weak Memory Models (abstract)
09:00-10:30 Session 125K (SYNT)
Location: Maths LT3
09:00
Synthesizing safe AI-based controllers for cyber-physical systems (abstract)
09:45
Meta-Interpretive Learning of Logic Programs (abstract)
09:00-10:30 Session 125L (TLA)
Location: Maths Boardroom
09:00
TLA+ in Engineering Systems: Quinceañera (abstract)
10:00
Modeling Virtual Machines and Interrupts in TLA+ & PlusCal (abstract)
09:00-10:30 Session 125M (ThEdu)
09:00
Students' Proof Assistant (SPA) (abstract)
09:30
Natural Deduction Assistant (NaDeA) (abstract)
10:00
Rating of Geometric Automated Theorem Provers (abstract)
09:00-10:30 Session 125N: Model Checking I (VSTTE)

Model Checking I

Location: Maths LT2
09:00
Contract-based Compositional Verification of Infinite-State Reactive Systems (abstract)
10:00
A Tree-Based Approach to Data Flow Proofs (abstract)
09:00-10:30 Session 125P: Invited Speaker; Distributed Systems I (VaVAS)

Invited Speaker

Contributed Talks: Distributed Systems I

Location: Maths LT1
09:00
Formal Synthesis of Control Strategies for Dynamical Systems (abstract)
10:00
Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) (abstract)
09:00-10:30 Session 125Q: Invited talk (WST)
09:00
Termination Checking and Invariant Synthesis for Affine Programs (abstract)
10:00-10:30 Session 126: ARQNL Regular Papers 1 (ARQNL)
10:00
Evidence Extraction from Parameterised Boolean Equation Systems (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 127A: ARQNL Regular Papers 2 (ARQNL)
11:00
Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms (abstract)
11:30
An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (abstract)
12:00
Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (abstract)
11:00-12:30 Session 127B (ASPOCP)
11:00
A Survey of Advances in Epistemic Logic Program Solvers (abstract)
11:30
selp: A Single-Shot Epistemic Logic Program Solver (abstract)
12:00
Partial Evaluation of Logic Programs in Vector Spaces (abstract)
11:00-12:30 Session 127C: AVoCS Regular papers 1 (AVOCS)

Automated verification

11:00
Detecting Deadlocks in Formal System Models with Condition Synchronization (abstract)
11:30
Backward reachability analysis for timed automata with data variables (abstract)
12:00
An Entailment Checker for Separation Logic with Inductive Definitions (abstract)
11:00-12:30 Session 127D (ICLP-DC)
Chair:
Location: Maths L6
11:00
The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (abstract)
11:30
Natural Language Generation From Ontologies (abstract)
12:00
Knowledge Authoring and Question Answering via Controlled Natural Language (abstract)
11:00-12:30 Session 127E: Security Policies as Challenge Problems (LPOP)
Chair:
11:00
Introduction: Role-Based Access Control as a Programming Challenge (abstract)
11:10
Security Policies in Constraint Handling Rules (abstract)
11:20
LPOP2018 XSB Position Paper (abstract)
11:30
Role-Based Access Control via JASP (abstract)
11:40
The RBAC challenge in the Knowledge Base Paradigm (abstract)
11:50
Role-Based Access Control via LogicBlox (abstract)
12:00
Logic-based Methods for Software Engineers and Business People (abstract)
12:10
Easier Rules and Constraints for Programming (abstract)
12:20
Questions about RBAC challenge solutions (abstract)
11:00-12:30 Session 127F: Practical MSO Model Checking 2 (LaSh)
11:00
Courcelle’s Theorem – A Game-Theoretic Approach (abstract)
12:05
A Derivative-Based Decision Procedure for WS1S (abstract)
11:00-12:30 Session 127G (MLP)
Location: Blavatnik LT1
11:00
Static Analysis for Developer Efficiency with Infer (abstract)
11:45
Learning to Type (abstract)
11:00-12:30 Session 127H: Formal specification and verification (NSV)
11:00
Compositional Taylor Model Based Validated Integration (abstract)
11:30
Automatic Generation and Formal Verification of an Interior Point Algorithm (abstract)
12:00
Towards Enumerative Invariant Synthesis in SMT Solvers (abstract)
11:00-12:30 Session 127I: Verifying parallel programs (PLR)

Techniques to verify parallel programs.

 

Chair:
11:00
Permission Inference for Array Programs (abstract)
11:45
RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL (abstract)
11:00-12:30 Session 127J (REFINE)
Location: Blavatnik LT2
11:00
Challenges of specifying concurrent program components (abstract)
11:30
Programming Without Refinement (abstract)
12:00
Ordering strict partial orders to model behavioural refinement (abstract)
11:00-12:30 Session 127K (SYNT)
Location: Maths LT3
11:00
Reactive Synthesis from LTL Specification with Spot (abstract)
11:18
On the Expressiveness of HyperLTL Synthesis (abstract)
11:36
Maximum Realizability for Linear Temporal Logic Specifications (abstract)
11:54
Warm-Starting Fixed-Point Based Control Synthesis (abstract)
12:12
Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (abstract)
11:00-12:30 Session 127L (TLA)
Location: Maths Boardroom
11:00
An Animation Module for TLA+ (abstract)
11:45
BMCMT – Bounded Model Checking of TLA+ Specifications with SMT (abstract)
11:00-12:30 Session 127M (ThEdu)
11:00
Lucas Interpretation from Programmers’ Perspective (abstract)
11:30
GeoCoq: formalized foundations of geometry (abstract)
11:00-12:30 Session 127N: Model Checking II (VSTTE)

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)
11:00-12:30 Session 127P: Distributed Systems II (VaVAS)

Contributed Talks: Distributed Systems II

Location: Maths LT1
11:00
Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking (abstract)
11:30
Policing Functions for Machine Learning Systems (abstract)
12:00
Social Consequence Engines (Abstract) (abstract)
11:00-12:30 Session 127Q: Program termination and orderings (I) (WST)
11:00
Procedure-Modular Termination Analysis (abstract)
11:30
GPO: A Path Ordering for Graphs (abstract)
12:00
Objective and Subjective Specifications (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 128B (ASPOCP)
14:00
Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (abstract)
14:30
Datalog for Static Analysis Involving Logical Formulae (abstract)
15:00
Syntactic Conditions for Antichain Property in Consistency Restoring Prolog (abstract)
14:00-15:30 Session 128C: Invited talk: Michael Emmi (AVOCS)

Automatic Verification of Concurrent Objects

14:00
Automatic Verification of Concurrent Objects (abstract)
14:00-15:30 Session 128D (ICLP-DC)
Chair:
Location: Maths L6
14:00
Scalable Robotic Intra-Logistics with Answer Set Programming (abstract)
14:30
Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (abstract)
15:00
Speeding Up Lazy-Grounding Answer Set Solving (abstract)
14:00-15:30 Session 128E: Challenge Solutions and Constraint Solving (LPOP)
14:00
Panel: Practice of Modeling and Programming (abstract)
14:30
Invited Talk: A Modeling Language Based on Semantic Typing (abstract)
15:10
A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (abstract)
15:20
Confluence Analysis of Cognitive Models with Constraint Handling Rules (abstract)
14:00-15:30 Session 128F: Frameworks (LaSh)
14:00
Declarative Dynamic Programming with Inverse Coupled Rewrite Systems (abstract)
15:00
A Logic of Information Flows (abstract)
14:00-15:30 Session 128G (MLP)
Location: Blavatnik LT1
14:00
Neural Meta Program Synthesis (abstract)
14:45
Learning to Analyze Programs at Scale (abstract)
14:00-15:30 Session 128H: Hybrid systems verification (NSV)
14:00
Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation (abstract)
14:30
Parallel reachability analysis of hybrid systems in XSpeed (abstract)
15:00
The Policy Iterations Algorithm is Actually a Newton Method (abstract)
14:00-15:30 Session 128I: Parallel SAT solving (PLR)

Parallel approaches to perform SAT solving.

Chair:
14:00
Tuning Parallel SAT Solvers (abstract)
14:45
GPU Accelerated SAT solving (abstract)
14:00-15:30 Session 128J (REFINE)
Location: Blavatnik LT2
14:00
A more relaxed way to make concrete: uses of heuristic search to discover implementations (abstract)
14:00-15:30 Session 128K (SYNT)
Location: Maths LT3
14:00
Scalable Synthesis with Symbolic Syntax Graphs (abstract)
14:18
On Inductive Verification and Synthesis (abstract)
14:36
Programming by example: efficient, but not “helpful” (abstract)
14:54
Minimal Synthesis of String To String Functions From Examples (abstract)
14:00-15:30 Session 128L (TLA)
Location: Maths Boardroom
14:00
Applying TLA+ in a Safety-Critical Railway Project (abstract)
14:30
State Space Explosion or: How To Fight An Uphill Battle (abstract)
14:00-15:30 Session 128M (ThEdu)
14:00
Towards intuitive reasoning in axiomatic geometry (abstract)
14:30
Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable (abstract)
14:00-15:30 Session 128N: Certification & Formalisation I (VSTTE)

Certification & Formalisation I

Location: Maths LT2
14:00
Verified Software: Theories, Tools, ... and Engineering (abstract)
15:00
Verified Certificate Checking for Counting Votes (abstract)
14:00-15:30 Session 128P: Invited Speaker; Autonomy (VaVAS)

Invited Speaker

Contributed Talks: Autonomy

Location: Maths LT1
14:00
Trust me I am autonomous (abstract)
15:00
Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (abstract)
14:00-15:30 Session 128Q: Program termination and orderings (II) (WST)
14:00
Comparing on Strings: Semantic Kachinuki Order (abstract)
14:30
Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions (abstract)
15:00
Well-founded models in proofs of termination (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 130A: ARQNL Presentation only & System demos (ARQNL)
16:00
Formalization of a Paraconsistent Infinite-Valued Logic (abstract)
16:30
System Demonstration: The Higher-Order Prover Leo-III (abstract)
16:00-18:00 Session 130B: AVoCS Regular Papers 2 (AVOCS)
16:00
Analyzing Consistency of Formal Requirements (abstract)
16:30
Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (abstract)
17:00
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (abstract)
16:00-18:00 Session 130C (ICLP-DC)
Chair:
Location: Maths L6
16:00
Model Revision of Logical Regulatory Networks using Logic-based Tools (abstract)
16:00-18:00 Session 130D: Logic and Constraints in Applications (LPOP)
16:00
Invited Talk: The Young Software Engineer’s Guide to Using Formal Methods (abstract)
16:40
How to upgrade ASP for true dynamic modelling and solving? (abstract)
16:50
A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks (abstract)
17:00
A software system should be declarative except where it interacts with the real world (abstract)
17:10
Questions about logic and constraints in real-world applications (abstract)
17:20
Panel: Future of Programming with Logic and Knowledge (abstract)
17:50
Closing (abstract)
16:00-18:00 Session 130E: Modelling and Solving (LaSh)
16:00
ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What? (abstract)
16:25
Automated Constraint Modelling with Conjure (abstract)
16:50
Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (abstract)
17:15
Decidable Linear Tree Constraints (abstract)
16:00-18:00 Session 130F (MLP)
Location: Blavatnik LT1
16:00
DeepBugs: A Learning Approach to Name-based Bug Detection (abstract)
16:45
Measuring software development productivity: a machine learning approach (abstract)
17:15
Answering Cloze-style Software Questions Using Stack Overflow (abstract)
16:00-18:00 Session 130H: Parallel parity game solving (PLR)

On parallel algorithms to solve parity games.

 

Chair:
16:00
Using work-stealing to parallelize symbolic algorithms and parity game solvers (abstract)
16:45
An Efficient Zielonka's Algorithm for Parallel Parity Games (abstract)
16:00-18:00 Session 130I (REFINE)
Chair:
Location: Blavatnik LT2
16:00
Refining Santa: An Excercise in Efficient Synchronization (abstract)
16:30
a Theory of Lazy Imperative Timing (abstract)
16:00-18:00 Session 130J (SYNT)
Location: Maths LT3
16:00
Towards correct-by-construction controller synthesis for self-driving cars (abstract)
16:45
Competition Report: SYNTCOMP (abstract)
17:00
Competition Report: SyGuS-COMP (abstract)
17:15
Probabilistic and Interpretable Models of Code (abstract)
16:00-18:00 Session 130K (TLA)
Location: Maths Boardroom
16:00
Invariants in Distributed Algorithms (abstract)
16:45
Proving properties of a minimal covering algorithm (abstract)
16:00-18:00 Session 130L (ThEdu)

ThEdu Business Meeting

16:00
ThEdu'18 business meeting (abstract)
16:00-18:00 Session 130M: Certification & Formalisation II (VSTTE)

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)
16:00-18:00 Session 130N: Autonomous Vehicles (VaVAS)

Contributed Talks: Autonomous Vehicles

Location: Maths LT1
16:00
Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (abstract)
16:30
Towards a verifiable decision making framework for self-driving vehicles (abstract)
17:00
Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (abstract)
16:00-18:00 Session 130P: Termination Competition (report and short talks) (WST)

TERMCOMP 2018 - Report

Presentation of tool papers:

  • M. Brockschmidt, S. Dollase, F. Emrich, F. Frohn, C. Fuhs, J. Giesl, M. Hark, J. Hensel, D. Korzeniewski, M. Naaf, T. Ströder. AProVE at the Termination Competition 2018
  • Florian Messner and Christian Sternagel. TermComp 2018 Participant: TTT2
  • Dieter Hofbauer. MultumNonMulta at TermComp 2018
  • Raúl Gutiérrez and Salvador Lucas. MU-TERM at the 2018 Termination Competition
  • Jesús J. Doménech and Samir Genaim. iRankFinder
19:15-21:30 Workshops dinner at Magdalen College (FLoC)

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 overview

09:00-10:30 Session 131A: Invited talk: Antoine Miné (AVOCS)

Experiences with thread-modular static analysis of concurrent embedded systems

09:00
Experiences with thread-modular static analysis of concurrent embedded systems by abstract interpretation (abstract)
09:00-10:30 Session 131B (EICNCL)
09:00
Title TBA - Invited talk (abstract)
10:00
Effective Translations between Display and Labelled Proofs for Tense Logics (abstract)
09:00-10:30 Session 131C (MLP)
Location: Blavatnik LT1
09:00
Why is Software Natural? and how can Naturalness be exploited? (abstract)
09:45
Program Synthesis as High-Level Machine Learning (abstract)
09:00-10:30 Session 131D: Welcome and Invited Talk (PAAR)
Location: Maths LT3
09:00
The CakeML Verified Compiler and Toolchain (abstract)
10:00
Dynamic Strategy Priority: Empower the strong and abandon the weak (abstract)
09:00-10:30 Session 131E: Welcome & invited talk I (PRUV)
09:00
Welcome to PRUV (abstract)
09:10
Quantitative Logic Reasoning -- Combining logical reasoning with probabilities and counting (invited talk) (abstract)
09:00-10:30 Session 131F: Opening and First Presentation Round (ReMOTE)
09:00
Welcome and Introduction (abstract)
09:15
Understanding Ethical Reasoning (abstract)
09:45
Human morality, robots’ moral competence, and the deepest kind of trust (abstract)
10:15
Elements of a Model of Trust in Technology (abstract)
09:00-10:00 Session 131G: Invited talk: A. Turberfield (VEMDP)
Chair:
Location: Maths L6
09:00
Controlling Assembly and Function of DNA Nanostructures and Molecular Machinery (abstract)
09:00-10:30 Session 131H: Certification & Formalisation III (VSTTE)

Certification & Formalisation III

Location: Maths LT2
09:00
Synthesis of Surveillance Strategies for Mobile Sensors (abstract)
10:00
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars (abstract)
09:00-10:30 Session 131I: Invited Speaker; Robotics (VaVAS)

Invited Speaker

Contributed Talks: Robotics I

Location: Maths LT1
09:00
Reproducibility in Robotics - The Big 5 Issues (abstract)
10:00
RoboTool: Modelling and Verification with RoboChart (abstract)
10:00-10:30 Session 132 (VEMDP)
Chair:
Location: Maths L6
10:00
Computing properties of stable configurations of thermodynamic binding networks (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 133A: AVoCS Regular Papers 3 (AVOCS)
11:00
Using SMT engine to generate Symbolic Automata (abstract)
11:30
Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (abstract)
12:00
A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (abstract)
11:00-12:30 Session 133B: Modal logics (EICNCL)
11:00
Toward intuitionistic non-normal modal logic and its calculi (abstract)
11:30
Proof theory for quantified monotone modal logics (abstract)
12:00
Sequent Calculi for Logic that Includes an Infinite Number of Modalities (abstract)
11:00-12:30 Session 133C (MLP)

Deep Learning for Code

Location: Blavatnik LT1
11:00
code2vec: Learning Distributed Representations of Code (abstract)
11:45
Understanding & Generating Source Code with Graph Neural Networks (abstract)
11:00-12:30 Session 133D: Automated Reasoning I (PAAR)
Location: Maths LT3
11:00
A Verified Simple Prover for First-Order Logic (abstract)
11:30
Proof Search Optimizations for Non-clausal Connection Calculi (abstract)
12:00
TFX: The TPTP Extended Typed First-order Form (abstract)
11:00-12:30 Session 133E: PRUV regular papers (PRUV)

PRUV regular papers

11:00
Measuring Disagreement among Knowledge Bases (abstract)
11:30
Evidential Group Decision Making Model with Belief-Based Preferences (abstract)
12:00
A new logic for jointly representing hard and soft constraints (abstract)
11:00-12:30 Session 133F: Second Presentation Round (ReMOTE)
11:00
How to Free Yourself from the Curse of Bad Equilibria (abstract)
11:30
Specification and Verification for Robots that Learn (abstract)
12:00
Moral Permissibility of Actions in Smart Home Systems (abstract)
11:00-12:30 Session 133G (VEMDP)
Location: Maths L6
11:00
Rule-Based Gillespie Simulation of Chemical Systems (abstract)
11:20
Rule-based design of computational DNA devices (abstract)
11:40
Noise control for molecular computing (abstract)
12:00
Molecular Filters for Noise Reduction (abstract)
11:00-12:30 Session 133H: Security (VSTTE)

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)
11:00-11:30 Session 133I: Robotics Demo (VaVAS)

Contributed Talks: Robotics II

Location: Maths LT1
11:00
Robot Demonstration (abstract)
11:00-12:30 Session 133J: Complexity (WST)
11:00
Complexity Analysis for Bitvector Programs (abstract)
11:30
A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (abstract)
12:00
Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (abstract)
11:30-12:30 Session 134: Panel Session (VaVAS)

Panel session focusing on key issues relating to the verification and validation of autonomous systems. Panelists include Calin Belta (Boston University), Jérémie Guiochet  (University of Toulouse III), Florian Lier  (Bielefeld University)  and Alice Miller (University of Glasgow).

Location: Maths LT1
12:30-14:00Lunch Break
14:00-15:30 Session 135A: Invited talk: Yannick Moy (AVOCS)

Mostly harmless - luring programmers into proof with SPARK

14:00
Mostly harmless - luring programmers into proof with SPARK (abstract)
14:00-15:30 Session 135B (EICNCL)
14:00
Cyclic proofs, hypersequents and Kleene algebra - Invited Talk (abstract)
15:00
Proof Translations in BI logic (abstract)
14:00-15:30 Session 135C (MLP)
Location: Blavatnik LT1
14:00
Neural Network Models of Code Edits (abstract)
14:45
Program synthesis and its connections to AGI (abstract)
14:00-15:30 Session 135D: Automated Reasoning II (PAAR)
Location: Maths LT3
14:00
Efficient translation of sequent calculus proofs into natural deduction proofs (abstract)
14:30
Set of Support for Higher-Order Reasoning (abstract)
15:00
Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (abstract)
14:00-15:30 Session 135E: Invited talk II & a short paper (PRUV)
14:00
An abstraction-refinement framework for automated reasoning -- a pragmatic approach (invited talk) (abstract)
15:10
Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure (abstract)
14:00-15:30 Session 135F: Third Presentation Round (ReMOTE)
Chair:
14:00
TBA (abstract)
14:30
The computational neuroscience of human-robot relationships (abstract)
15:00
Trust, Failure, and Self-Assessment During Human-Robot Interaction (abstract)
14:00-15:00 Session 135G: Invited talk: SJ Dunn (VEMDP)
Location: Maths L6
14:00
Uncovering the Biological Programs that Govern Development (abstract)
14:00-15:30 Session 135H: New Applications (VSTTE)

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)
14:00-15:30 Session 135I: Complexity / Applications (WST)
14:00
Control-Flow Refinement via Partial Evaluation (abstract)
14:30
Verification of Rewriting-based Query Optimizers (abstract)
15:00
TTT2 with Termination Templates for Teaching (abstract)
15:00-15:30 Session 136 (VEMDP)
Location: Maths L6
15:00
Bayesian Verification of Chemical Reaction Networks (abstract)
15:10
Computational Approaches for the Programmed Assembly of Nanocellulose Meshes (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 137A: AVoCS Regular Papers 4 (AVOCS)
16:00
Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks (abstract)
16:30
Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (abstract)
16:00-17:30 Session 137B: Intuitionistic and belief logics (EICNCL)
16:00
Intuitionistic multi-agent subatomic natural deduction for belief and knowledge (abstract)
16:30
Hypersequent calculus for the logic of conditional belief: preliminary results (abstract)
17:00
A Forward Calculus for Countermodel Construction in IPL (abstract)
16:00-18:00 Session 137C (MLP)
Location: Blavatnik LT1
16:00
Difflog: Beyond Deductive Methods in Program Analysis (abstract)
16:30
Deep Learning On Code with an Unbounded Vocabulary (abstract)
17:00
Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network (abstract)
17:30
Open Business Meeting for Future of Machine Learning for Programming (abstract)
16:00-18:00 Session 137D: PRUV regular papers (PRUV)
16:00
A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems (abstract)
16:30
A New Probabilistic Algorithm for Approximate Model Counting (abstract)
17:00
Leveraging Probabilistic Existential Rules for Adversarial Deduplication (abstract)
17:30
VolCE: An Efficient Tool for Solving #SMT(LA) Problems (abstract)
16:00-18:00 Session 137F (VEMDP)
Location: Maths L6
16:00
Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework. (abstract)
16:20
Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (abstract)
16:40
Conservative approximations of polymers (abstract)
17:00
Executable Biochemical Space for Specification and Analysis of Biochemical Systems (abstract)
17:20
Formal Verification of Network-Based Biocomputation Circuits (abstract)
16:00-18:00 Session 137G: Off the beaten track (VSTTE)

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)
16:00-17:00 Session 137H: Higher-Order (WST)
16:00
Termination of Lambda-Pi modulo rewriting using the size-change principle (abstract)
16:30
Improving Static Dependency Pairs for Higher-Order Rewriting (abstract)