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)
Location: St Anne's College
| 09:00 | Computational learning theory I (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 2 (FoPSS)
Location: St Anne's College
| 11:00 | Computational learning theory II (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 3 (FoPSS)
Location: St Anne's College
| 14:00 | Statistical learning theory I (abstract) |
15:30-16:00Coffee Break
16:00-17:30 Session 4 (FoPSS)
Location: St Anne's College
| 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
11:00-12:30 Session 12 (FoPSS)
Location: St Anne's College
| 11:00 | Learning in Verification II (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 13 (FoPSS)
Location: St Anne's College
| 14:00 | Verification of machine learning programs I (abstract) |
15:30-16:00Coffee Break
16:00-17:30 Session 14 (FoPSS)
Location: St Anne's College
| 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)
Location: St Anne's College
| 09:00 | Learning and epistemic modal logic I (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 16 (FoPSS)
Location: St Anne's College
| 11:00 | Learning and epistemic modal logic II (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 17 (FoPSS)
Location: St Anne's College
| 14:00 | Inductive logic programming I (abstract) |
15:30-16:00Coffee Break
16:00-17:30 Session 18 (FoPSS)
Location: St Anne's College
| 16:00 | Inductive logic programming II (abstract) |
Friday, July 6th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 19 (FoPSS)
Location: St Anne's College
| 09:00 | Inductive logic programming and deep learning I (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 20 (FoPSS)
Location: St Anne's College
| 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)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
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 23C (GS)
Chair:
Location: Maths LT3
| 09:00 | TBA (abstract) |
| 10:00 | "Operational'' Game Semantics (abstract) |
09:00-10:30 Session 23D: Invited talk: Emily Riehl (HDRA)
Chair:
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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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 23K: Invited tutorial (first part) (PARIS)
Chair:
Location: Maths L4
| 09:00 | Workshop introduction (abstract) |
| 09:15 | An Introduction to Cyclic Proofs (abstract) |
09:00-10:30 Session 23L: Tuning solvers and applications (POS)
Chair:
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 23M: SR Invited tutorial: Edith Elkind (SR)
Chair:
Location: Maths Seminar C3
| 09:00 | Strategic behavior in social choice - Part 1 (abstract) |
09:00-10:30 Session 23N: switch (TYDI)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 09:00 | Handling substitutions via duality (abstract) |
| 10:00 | Unification based on generalized embedding (abstract) |
09:30-10:30 Session 24A (HoTT/UF)
Chair:
Location: Blavatnik LT1
| 09:30 | Axiomatizing Cubical Sets Models of Univalent Foundations (abstract) |
09:30-10:30 Session 24B: Invited Talk (TERMGRAPH)
Chair:
Location: Maths Seminar C1
| 09:30 | Critical Pairs in Graph Transformation Systems (abstract) |
10:00-10:30 Session 25 (HOR)
Chair:
Location: Maths Seminar C5
| 10:00 | Combinatorics of explicit substitutions (extended abstract) (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 26A (CL&C)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Maths Seminar C5
| 11:00 | Some applications of quantitative types inside and outside type theory (abstract) |
11:00-12:30 Session 26F (HoTT/UF)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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 26N: SR Invited tutorial: Edith Elkind (SR)
Chair:
Location: Maths Seminar C3
| 11:00 | Strategic behavior in social choice - Part 2 (abstract) |
11:00-12:30 Session 26P: Frameworks (TERMGRAPH)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
Location: Maths Seminar C5
| 12:00 | Orthogonality and sequentiality in substructural Linear HRSs (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 28A (CL&C)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
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)
Chair:
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:00 Session 28D: HRDA & HoTT/UF Invited Talk: Paige North (HDRA and HoTT/UF)
Chair:
Location: Blavatnik LT2
| 14:00 | A homotopy type theory for directed homotopy theory (abstract) |
14:00-15:00 Session 28E: Invited talk: Cynthia Kop (HOR)
Chair:
Location: Maths Seminar C5
| 14:00 | Wanda: a higher-order termination tool (abstract) |
14:00-15:30 Session 28F: Term Rewriting (IWC)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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:
Location: Maths Seminar C3
| 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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
Location: Blavatnik Seminar Room 3
| 14:30 | Invited talk: Semantic Equivalence Checking for HHVM Bytecode (abstract) |
14:30-15:30 Session 29B: MAXSAT & local search (POS)
Chair:
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)
Chair:
Location: Blavatnik LT2
| 15:00 | Towards a fully formalized definition of syllepsis in weak higher categories (abstract) |
15:00-15:30 Session 30B (HOR)
Chair:
Location: Maths Seminar C5
| 15:00 | Refining Properties of Filter Models: Sensibility, Approximability and Reducibility (abstract) |
15:00-15:30 Session 30C (HoTT/UF)
Chair:
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)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
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 31G: Applications and Business Meeting (IWC)
Chair:
Location: Blavatnik Seminar Room 4
| 16:00 | Complete Axiom System of Cluster Algebra (abstract) |
| 16:30 | IWC Business Meeting (abstract) |
16:00-18:00 Session 31H: Implementation (LFMTP)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Maths Seminar C3
| 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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 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) |
17:00-18:00 Session 32B: Special session in honour of Kris Rose (HOR)
Chair:
Location: Maths Seminar C5
18:10-18:40 Session 33: UNIF 2018 Wrap Up (UNIF)
Discussions about UNIF 2018 issues and future of UNIF
Chairs:
Location: Maths Seminar C4
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.
Location: Thaikhun Restaurant
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 09:00 | Quantitative types: from Foundations to Applications (abstract) |
09:00-10:30 Session 34D (Domains13)
Chair:
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)
Chair:
Location: St Luke's Chapel
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C1
| 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 34H: Invited Talks (IFIP WG 1.6)
Chair:
Location: Maths Seminar C2
| 09:00 | TBA (abstract) |
| 09:45 | TBA (abstract) |
09:00-10:30 Session 34I (LMW)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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 34M: SR Invited tutorial: Marcin Jurdziński (SR)
Chair:
Location: Maths Seminar C3
| 09:00 | Parity Games - Part 1 (abstract) |
09:00-10:30 Session 34N (WiL)
Chair:
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:15-10:30 Session 35: Invited Talk (PARIS)
Chair:
Location: Maths L4
| 09:15 | Riding Modal Cycles (abstract) |
09:30-10:30 Session 36A (HoTT/UF)
Chair:
Location: Blavatnik LT1
| 09:30 | Injective types and searchable types in univalent mathematics (abstract) |
09:30-10:30 Session 36B (WPTE)
Chair:
Location: Blavatnik Seminar Room 4
| 09:30 | A framework for graph rewriting. (abstract) |
10:00-10:30 Session 37 (DCM)
Chair:
Location: Maths Seminar C4
| 10:00 | Models of Computation that Conserve Data (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 38A (COALG)
Chair:
Location: Blavatnik Seminar Room 3
| 11:00 | Coalgebra and Automated Reasoning (abstract) |
| 11:45 | Coalgebraic Tools for Randomness-Conserving Protocols (abstract) |
11:00-12:30 Session 38B (Coq)
Chair:
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:
Location: Maths Seminar C4
| 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)
Chair:
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)
Chair:
Location: St Luke's Chapel
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
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 38I: Invited Talk, Report on ISR (IFIP WG 1.6)
Chair:
Location: Maths Seminar C2
| 11:00 | TBA (abstract) |
| 11:45 | Report on ISR (abstract) |
11:00-12:30 Session 38J (ITRS)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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 38P: SR Invited tutorial: Marcin Jurdziński (SR)
Chair:
Location: Maths Seminar C3
| 11:00 | Parity Games - Part 2 (abstract) |
11:00-12:30 Session 38Q (WPTE)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
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:
Location: St Luke's Chapel
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C2
| 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:
Location: Maths Seminar C5
| 14:00 | Intersection Types for Unboundedness Problems (ITRS invited talk) (abstract) |
| 15:00 | Gradual Intersection Types (abstract) |
14:00-15:30 Session 40K (LMW)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 14:00 | Ornamentation put into practice in ML (abstract) |
| 15:00 | Profunctor Optics and the Yoneda Lemma (abstract) |
14:00-15:30 Session 40N: Invited tutorial (second part) (PARIS)
Chair:
Location: Maths L4
| 14:00 | An Introduction to Cyclic Proofs (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)
Chair:
Location: Maths Seminar C3
| 14:00 | Infinite-Duration Richman Bidding Games (abstract) |
| 14:40 | Solving Parity Games: Explicit vs Symbolic (abstract) |
14:00-15:30 Session 40R (WPTE)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
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-16:30 Session 42C (DCM)
Chair:
Location: Maths Seminar C4
| 16:00 | Generic Graph Semantics (abstract) |
16:00-17:15 Session 42D (Domains13)
Chair:
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)
Chair:
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:
Location: Maths Seminar C1
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C5
| 16:00 | Intersection Subtyping with Constructors (abstract) |
16:00-18:00 Session 42K (Linearity/TLLA)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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)
Chair:
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-18:00 Session 42Q: Strategy Logic (SR)
Chair:
Location: Maths Seminar C3
| 16:00 | Quantifying Bounds in Strategy Logic (abstract) |
| 16:40 | Strategy Logic with Imperfect Information (abstract) |
| 17:20 | Dependences in Strategy Logic (abstract) |
16:00-17:00 Session 42R (WiL)
Chair:
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)
Chair:
Location: Maths Seminar C5
| 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".
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Chair:
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)
Chair:
Location: Maths LT2
| 14:00 | Sanctum: Towards an Open-Source, Formally Verified Secure Processor (abstract) |
14:00-15:00 Session 49B: FSCD Invited talk: Peter Selinger (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 14:00 | Challenges in quantum programming languages (abstract) |
14:00-15:30 Session 49C (ITP)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Chair:
Location: Maths LT2
| 15:00 | Guided design of attack trees: a system-based approach (abstract) |
15:00-15:30 Session 50B: Quantum Computing (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 15:00 | A diagrammatic axiomatisation of fermionic quantum circuits (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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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).
Location: Ashmolean Museum
Tuesday, July 10th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 52A: Cryptographic primitives (CSF)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
Location: Blavatnik LT1
| 09:00 | Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics (abstract) |
09:00-10:00 Session 52D: LICS Invited Talk: Ursula Martin (LICS)
Chair:
Location: Maths LT1
| 09:00 | On Diversity (abstract) |
09:00-10:30 Session 52E: Model Counting (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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)
Chair:
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) |
11:00-12:00 Session 54F: SAT Invited Talk: Rahul Santhanam (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Modelling SAT (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 55A: Knowledge and hyperproperties (CSF)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 14:00 | Proof techniques for program equivalence in probabilistic higher-order languages (abstract) |
14:00-15:30 Session 55C (ITP)
Chair:
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)
Chair:
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:
Location: Blavatnik Seminar Rooms 1 & 2
| 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:00-15:30 Session 56: Types (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 15:00 | A Syntax for Higher Inductive-Inductive Types (abstract) |
15:30-16:00Coffee Break
15:40-16:40 Session 57A: Complexity (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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-16:30 Session 58A: Blockchain (CSF)
Chair:
Location: Maths LT2
| 16:00 | KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (abstract) |
16:00-17:00 Session 58B (ITP)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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).
Chair:
Location: Sheldonian Theatre
| 17:00 | Unifying Logic and Probability: the BLOG Language (abstract) |
Wednesday, July 11th
View this program: with abstractssession overviewtalk overview
09:00-10:15 Session 60A: Invited talk: Raphael Jungers (ADHS)
Location: CS Lecture Theatre B
| 09:00 | Provably efficient algorithms on hybrid automata (abstract) |
09:00-10:30 Session 60B: Information flow (CSF)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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:00 Session 60E: LICS Invited Talk: Thierry Coquand (LICS)
Chair:
Location: Maths LT1
| 09:00 | Univalent Type Theory (abstract) |
09:00-10:30 Session 60F: Theory (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 09:00 | Hard Combinatorial Problems: A Challenge for Satisfiability (abstract) |
10:00-10:40 Session 61 (LICS)
Chair:
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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Location: CS Lecture Theatre A
| 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)
Location: CS Lecture Theatre B
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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:00 Session 64F: SAT Invited Talk: Marijn Heule (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Computable Short Proofs (abstract) |
11:00-12:40 Session 64G: Extended Abstracts: Symbolic Computation (SCSC)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
Location: Maths LT2
| 12:00 | Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (abstract) |
12:00-12:20 Session 65B: Industry Presentation (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 12:00 | Satalia's SolveEngine (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 66A: FLoC Keynote Lecture: Shafi Goldwasser (FLoC)
Chair:
Location: Maths LT1
| 14:00 | Pseudo deterministic algorithms and proofs (abstract) |
14:00-15:40 Session 66B: Applications 1 (ADHS)
Location: CS Lecture Theatre A
| 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)
Location: CS Lecture Theatre B
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 16:00 | Formal Design, Implementation and Verification of Blockchain Languages (abstract) |
16:00-18:00 Session 67C (ITP)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Location: CS Lecture Theatre A
| 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)
Location: CS Lecture Theatre B
| 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).
Location: Examination Schools
Thursday, July 12th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 70A: Invited talk: Calin Belta (ADHS)
Location: CS Lecture Theatre B
| 09:00 | Formal Synthesis of Control Strategies for Dynamical Systems (abstract) |
09:00-10:00 Session 70B: FSCD Invited talk: Stéphanie Delaune (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 09:00 | Analysing privacy-type properties in cryptographic protocols (abstract) |
09:00-10:30 Session 70C (ITP)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
Location: St Luke's Chapel
| 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:00-10:30 Session 72: Unification (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 10:00 | Term-Graph Anti-Unification (abstract) |
10:30-11:00Coffee Break
10:50-12:30 Session 73A: Reachability and safety analysis (ADHS)
Location: CS Lecture Theatre A
| 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)
Chair:
Location: CS Lecture Theatre B
| 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:
Location: St Luke's Chapel
| 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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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) |
11:00-12:30 Session 74F (SMT)
Chair:
Location: Green Templeton Lecture Theatre
| 11:00 | Building Better Bit-Blasting for Floating-Point Problems (abstract) |
| 11:30 | The next 10^4 UppSAT Approximations (abstract) |
| 12:00 | Alt-Ergo 2.2 (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:00-12:30 Session 75B: Tools & Applications I (SAT)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 12:00 | XORSAT Set Membership Filters (abstract) |
12:30-14:00Lunch Break
14:00-15:40 Session 76A: Optimal and model predictive control (ADHS)
Location: CS Lecture Theatre A
| 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)
Location: CS Lecture Theatre B
| 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
- Welcome by Steering Committee Chair, Luke Ong
- Report of FSCD18 PC Chair, Helene Kirchner
- Report of FSCD18 Conference Chair, Paula Severi
- Progress Report of FSCD19 - PC Chair: Herman Geuvers - Conference Chair: Jakob Rehof
- Election of two Steering Committee members
- Proposal to host FSCD20 (colocating with IJCAR2020) in Paris: Stefano Guerrini and Giulio Manzonetto
- AOB
- Handover to new SC Chair (2018-2021), Delia Kesner.
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
14:00-15:00 Session 76D: ITP Invited Talk: Jean-Christophe Filliâtre (ITP)
Chair:
Location: Blavatnik LT1
| 14:00 | Deductive Program Verification (abstract) |
14:00-15:40 Session 76E (LICS)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 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)
Location: Green Templeton Lecture Theatre
| 14:00 | Invited talk: Verifying Learners and Learning Verifiers (abstract) |
| 15:00 | Puli - A Problem-Specific OMT Solver (abstract) |
15:00-15:30 Session 77A: System presentation (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 15:00 | ProTeM: A Proof Term Manipulator (abstract) |
15:00-15:30 Session 77B (ITP)
Chair:
Location: Blavatnik LT1
| 15:00 | ProofWatch: Watchlist Guidance for Large Theories in E (abstract) |
15:30-16:00Coffee Break
16:00-16:30 Session 78A: Confluence Competition presentation (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 16:00 | Confluence Competition 2018 (abstract) |
16:00-17:00 Session 78B (ITP)
Chair:
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:00 Session 78C: LICS Invited Talk: Javier Esparza (LICS)
Chair:
Location: Maths LT1
| 16:00 | Verification of population protocols (abstract) |
16:00-18:00 Session 78D: Awards & Competitions (SAT)
Chairs:
Location: Blavatnik Seminar Rooms 1 & 2
| 16:00 | Award Ceremony (abstract) |
| 16:05 | MaxSAT Evaluation 2018 (abstract) |
| 16:33 | QBFEVAL’18 (abstract) |
| 17:01 | Sparkle SAT Challenge 2018 (abstract) |
| 17:29 | SAT Competition 2018 (abstract) |
16:00-17:30 Session 78E (SMT)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Location: CS Lecture Theatre A
| 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)
Location: CS Lecture Theatre B
| 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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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) |
17:30-18:00 Session 82: Rewriting (FSCD)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 17:30 | Coherence of Gray categories via rewriting (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)
Chair:
Location: CS Lecture Theatre B
| 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)
Chair:
Location: St Anne's Seminar Room 7
| 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)
Chair:
Location: St Anne's Seminar Room 8
| 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)
Chair:
Location: St Luke's Chapel
| 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)
Chair:
Location: Blavatnik Seminar Room 3
| 09:00 | Pathway Logic: Symbolic executable models for reasoning about cellular processes (abstract) |
09:00-10:30 Session 83G (LearnAut)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
Location: Blavatnik LT2
| 09:00 | Model checking and its applications (abstract) |
| 09:45 | Computation and inference (abstract) |
09:00-10:30 Session 83P: Vampire - Past, Present and Future (Vampire)
Chair:
Location: Maths Seminar C2
| 09:00 | Vampire: where have we come from, where are we going (abstract) |
09:00-10:30 Session 83Q (rv4rise)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
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) |
09:30-10:30 Session 84B: LCC Invited Talk: Mikolaj Bojanczyk (LCC)
Chair:
Location: Maths L5
| 09:30 | On polynomial time for infinite structures (abstract) |
10:30-11:00Coffee Break
10:50-12:05 Session 85: Stochastic systems 2 (ADHS)
Location: CS Lecture Theatre A
| 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)
Chair:
Location: St Anne's Seminar Room 7
| 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)
Chair:
Location: St Anne's Seminar Room 8
| 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)
Chair:
Location: St Luke's Chapel
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
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)
Chair:
Location: Maths L6
| 11:00 | Modularity in Proof Assistants (abstract) |
| 11:45 | Discussion 1 (abstract) |
11:00-12:30 Session 86N: UITP 2 (UITP)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
Location: Maths Seminar C2
| 11:00 | Counterexample-Guided Quantifier Instantiation in Logical Theories (abstract) |
11:00-12:30 Session 86R (rv4rise)
Chair:
Location: Blavatnik Seminar Room 1
| 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
12:30-14:00 FLOC Steering Committee Lunchtime Meeting (FLoC)
Location: Upper Common Room, St Anne's College
14:00-15:15 Session 87A: Control Synthesis (ADHS)
Location: CS Lecture Theatre A
| 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)
Chair:
Location: St Anne's Seminar Room 7
| 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)
Chair:
Location: St Anne's Seminar Room 8
| 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)
Chair:
Location: St Luke's Chapel
| 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)
Chair:
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:
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
Location: Maths Seminar C1
| 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)
Chair:
Location: Green Templeton Lecture Theatre
| 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)
Chair:
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)
Chair:
Location: Maths L6
| 14:00 | Modularity in Proof Checking (abstract) |
| 14:45 | Modularity in Large Proofs (abstract) |
14:00-15:30 Session 87N: UITP 3/ Isabelle 3 Joint Session (Isabelle and UITP)
Chair:
Location: Blavatnik Seminar Room 4
| 14:00 | Isabelle/PIDE after 10 years of development (abstract) |
| 14:30 | Text-Orientated Formal Mathematics (abstract) |
| 15:00 | Drawing Trees (abstract) |
14:00-15:30 Session 87P (VDMW)
Chair:
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)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: St Anne's Seminar Room 8
| 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-17:00 Session 88B (HCVS)
Chair:
Location: St Luke's Chapel
| 16:00 | Report on the CHC competition (abstract) |
16:00-18:00 Session 88C: Isabelle 4 (Isabelle)
Chair:
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)
Chair:
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:
Location: Blavatnik Seminar Room 3
| 16:00 | A logic modelling workflow for systems pharmacology (abstract) |
16:00-17:30 Session 88F (LearnAut)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C5
| 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-17:30 Session 88H: SMT-LIB Updates and Discussion (SMT)
Chair:
Location: Green Templeton Lecture Theatre
16:00-16:40 Session 88I: Explainable machine learning (SoMLMFM)
Chair:
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:30 Session 88L: Contributed Talks (Vampire)
Chair:
Location: Maths Seminar C2
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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:
Location: St Anne's Seminar Room 7
| 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)
Chair:
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.
Chair:
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
09:00-10:30 Session 93A: FLoC Keynote Lecture: Georges Gonthier (FLoC)
Chair:
Location: Maths LT1
| 09:00 | The Logic of Real Proofs (abstract) |
09:00-10:00 Session 93B: F-IDE/Overture invited talk: Jean-Christophe Filliatre (F-IDE and Overture)
Chair:
Location: Blavatnik Seminar Room 1
| 09:00 | Auto-active verification using Why3's IDE (abstract) |
10:00-10:30 Session 94A: Program verification (F-IDE)
Chair:
Location: Blavatnik Seminar Room 1
| 10:00 | Lightweight Interactive Proving inside an Automatic Program Verifier (abstract) |
10:00-10:30 Session 94B: Overture: Tools (Overture)
Chair:
Location: Blavatnik Seminar Room 2
| 10:00 | Welcome to the Overture Workshop (abstract) |
| 10:10 | Enhancing Testing of VDM-SL models (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 95A: Model Checking (CAV)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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>.
Chairs:
Location: Blavatnik LT2
11:00-12:30 Session 95E: Foundations I (ICLP)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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:00-14:50 Session 96F: Overture/F-IDE invited talk: Leo Freitas (F-IDE and Overture)
Chair:
Location: Blavatnik Seminar Room 2
| 14:00 | VDM at large: analysing the EMV Next Generation Kernel (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.
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths LT1
| 15:00 | Fast Numerical Program Analysis with Reinforcement Learning (abstract) |
| 15:15 | A Direct Encoding for NNC Polyhedra (abstract) |
15:00-15:30 Session 98B: Experience in analyzing large programs (F-IDE)
Chair:
Location: Blavatnik Seminar Room 1
| 15:00 | Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 99A: Synthesis (CAV)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
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 99E: ICLP Invited Talk: Thomas Eiter (ICLP)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 16:00 | Answer Set Programs go 30: Past and Future (abstract) |
16:00-17:00 Session 99F: Tools and Rewriting (IJCAR)
Chair:
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.
Chair:
Location: Blavatnik Seminar Room 2
| 16:00 | The Overture Strategic Research Agenda (abstract) |
17:00-18:00 Session 100A: ASP Extensions (ICLP)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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?
Chair:
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).
Location: Oxford Town Hall
Sunday, July 15th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 101B (FM)
Chair:
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:
Location: Blavatnik Seminar Rooms 3 & 4
| 09:00 | Avoiding redundancies in the exploration of concurrent programs (abstract) |
09:00-10:30 Session 101D: Logics and Calculi (IJCAR)
Chair:
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)
Chair:
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.
Chair:
Location: Maths LT1
10:00-10:30 Session 103A: Learning (CAV)
Chair:
Location: Maths LT1
| 10:00 | Learning Abstractions for Program Synthesis (abstract) |
| 10:15 | The Learnability of Symbolic Automata (abstract) |
10:00-10:30 Session 103B: ASP Applications (ICLP)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 10:00 | Temporal Answer Set Programming on Finite Traces (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 104A: Runtime Verification, Hybrid and Timed Systems (CAV)
Chair:
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)
Chair:
Location: Maths LT2
| 11:00 | Privacy in Text Processing: An information flow perspective (abstract) |
11:00-12:30 Session 104C: Implementation I (ICLP)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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:00-12:30 Session 105 (FM)
Chair:
Location: Maths LT2
| 12:00 | FSM Inference from Long Traces (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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
Location: Blavatnik LT1
| 14:00 | Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? (abstract) |
15:00-15:30 Session 107A (FM)
Chair:
Location: Maths LT2
| 15:00 | A Weakness Measure for GR(1) Formulae (abstract) |
15:00-15:30 Session 107B: Termination (IJCAR)
Chair:
Location: Blavatnik LT1
| 15:00 | Well-Founded Unions (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 108A: Probabilistic Systems (CAV)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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)
Chair:
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:00 Session 110B: FM Invited Talk: Leonardo de Moura (FM)
Chair:
Location: Blavatnik LT1
| 09:00 | Efficient verification and metaprogramming in Lean (abstract) |
09:00-10:30 Session 110C: Language and Reasoning (ICLP)
Chair:
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)
Chair:
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)
Chair:
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:00 Session 112A: CAV Invited Talk: Somesh Jha (CAV)
Location: Maths LT1
| 11:00 | Semantic Adversarial Deep Learning (abstract) |
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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-11:30 Session 112D: Implementation of ASP Systems (ICLP)
Chair:
Location: Blavatnik LT2
| 11:00 | Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (abstract) |
11:00-12:30 Session 112E: Superposition (IJCAR)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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) |
17:30-18:30 Session 117: Competitions Presentations (IJCAR)
Chair:
Location: Maths LT2
| 17:30 | IJCAR competition presentations (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).
Location: Ashmolean Museum
Tuesday, July 17th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 118A: Theory and Security (CAV)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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:30 Session 118D: Test of Time Awards and Best DC Paper (ICLP)
Chair:
Location: Blavatnik LT2
| 09:00 | Test of time 20 (abstract) |
| 09:30 | TEST OF TIME 10 (abstract) |
| 10:00 | Best DC Paper (abstract) |
09:00-10:00 Session 118E: IJCAR Invited Talk: Erika Abraham (IJCAR)
Chair:
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)
Chair:
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)
Chair:
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:00 Session 120B: FM Invited Talk: Kim G. Larsen (FM)
Chair:
Location: Blavatnik LT1
| 11:00 | 20 Years of "Real" Real-Time Model Checking (abstract) |
11:00-12:30 Session 120C: Applications (ICLP)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 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)
Chair:
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)
Chair:
Location: CS Lecture Theatre A
| 09:00 | Automated Reasoning In Natural Language: Current Directions (abstract) |
09:00-10:30 Session 125B (ASPOCP)
Chairs:
Location: Blavatnik Seminar Room 3
| 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
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
Location: Blavatnik LT1
| 09:00 | Opening and demos (abstract) |
| 09:45 | Bimodal Software Engineering (abstract) |
09:00-10:30 Session 125H: Industrial Session (NSV)
Chair:
Location: St Luke's Chapel
| 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:
Location: Maths Seminar C5
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: CS Lecture Theatre B
| 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
Chair:
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
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 09:00 | Termination Checking and Invariant Synthesis for Affine Programs (abstract) |
10:00-10:30 Session 126: ARQNL Regular Papers 1 (ARQNL)
Chair:
Location: CS Lecture Theatre A
| 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)
Chair:
Location: CS Lecture Theatre A
| 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)
Chair:
Location: Blavatnik Seminar Room 3
| 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
Chair:
Location: Blavatnik Seminar Room 1
| 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:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
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)
Chair:
Location: St Luke's Chapel
| 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:
Location: Maths Seminar C5
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: CS Lecture Theatre B
| 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
Chair:
Location: Maths LT2
| 11:00 | Executable Counterexamples in Software Model Checking (abstract) |
| 11:30 | Extending VIAP to Handle Array Programs (abstract) |
| 12:00 | Lattice-Based Refinement in Bounded Model Checking (abstract) |
11:00-12:30 Session 127P: Distributed Systems II (VaVAS)
Contributed Talks: Distributed Systems II
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 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:00 Session 128A: ARQNL Invited Talk: Giles Reger (ARQNL)
Chair:
Location: CS Lecture Theatre A
| 14:00 | Going Beyond First-Order Logic with Vampire (abstract) |
14:00-15:30 Session 128B (ASPOCP)
Chair:
Location: Blavatnik Seminar Room 3
| 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
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
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)
Chair:
Location: St Luke's Chapel
| 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:
Location: Maths Seminar C5
| 14:00 | Tuning Parallel SAT Solvers (abstract) |
| 14:45 | GPU Accelerated SAT solving (abstract) |
14:00-15:30 Session 128J (REFINE)
Chair:
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)
Chair:
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)
Chair:
Location: CS Lecture Theatre B
| 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
Chair:
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
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 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:00-15:30 Session 129: ARQNL Regular Papers 3 (ARQNL)
Chair:
Location: CS Lecture Theatre A
| 15:00 | Pseudo-Propositional Logic (abstract) |
15:30-16:00Coffee Break
16:00-17:30 Session 130A: ARQNL Presentation only & System demos (ARQNL)
Chair:
Location: CS Lecture Theatre A
| 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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Chair:
Location: Blavatnik Seminar Room 2
| 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)
Chair:
Location: Maths Seminar C4
| 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)
Chair:
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 130G: Discussion, concluding remarks (NSV)
Chair:
Location: St Luke's Chapel
| 16:00 | Discussion (abstract) |
16:00-18:00 Session 130H: Parallel parity game solving (PLR)
On parallel algorithms to solve parity games.
Chair:
Location: Maths Seminar C5
| 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)
Chair:
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
Chairs:
Location: CS Lecture Theatre B
| 16:00 | ThEdu'18 business meeting (abstract) |
16:00-18:00 Session 130M: Certification & Formalisation II (VSTTE)
Certification & Formalisation II
Chair:
Location: Maths LT2
| 16:00 | Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications (abstract) |
| 16:30 | TWAM: A Certifying Abstract Machine for Logic Programs (abstract) |
| 17:00 | A Java bytecode formalisation (abstract) |
| 17:30 | Formalising Executable Specifications of Low-Level Systems (abstract) |
16:00-18:00 Session 130N: Autonomous Vehicles (VaVAS)
Contributed Talks: Autonomous Vehicles
Chair:
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
Chair:
Location: Blavatnik Seminar Room 4
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).
Location: Magdalen College
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
Chair:
Location: Blavatnik Seminar Room 1
| 09:00 | Experiences with thread-modular static analysis of concurrent embedded systems by abstract interpretation (abstract) |
09:00-10:30 Session 131B (EICNCL)
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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)
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Maths Seminar C5
| 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
Chair:
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
Chair:
Location: Maths LT1
| 09:00 | Reproducibility in Robotics - The Big 5 Issues (abstract) |
| 10:00 | RoboTool: Modelling and Verification with RoboChart (abstract) |
09:00-10:30 Session 131J: Invited talk (WST)
Chair:
Location: Blavatnik Seminar Room 4
| 09:00 | Towards a Unified Method for Termination (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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Location: Blavatnik Seminar Room 2
| 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
Chair:
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)
Chair:
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
Location: Blavatnik Seminar Room 3
| 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)
Chair:
Location: Maths Seminar C5
| 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)
Chair:
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
Chair:
Location: Maths LT2
| 11:00 | Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components (abstract) |
| 11:30 | SideTrail: Verifying Time-Balancing of Cryptosystems (abstract) |
| 12:00 | Towards verification of Ethereum smart contracts: a formalization of core of Solidity (abstract) |
11:00-11:30 Session 133I: Robotics Demo (VaVAS)
Contributed Talks: Robotics II
Chair:
Location: Maths LT1
| 11:00 | Robot Demonstration (abstract) |
11:00-12:30 Session 133J: Complexity (WST)
Chair:
Location: Blavatnik Seminar Room 4
| 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).
Chair:
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
Chair:
Location: Blavatnik Seminar Room 1
| 14:00 | Mostly harmless - luring programmers into proof with SPARK (abstract) |
14:00-15:30 Session 135B (EICNCL)
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Chair:
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)
Location: Blavatnik Seminar Room 3
| 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:
Location: Maths Seminar C5
| 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)
Chair:
Location: Maths L6
| 14:00 | Uncovering the Biological Programs that Govern Development (abstract) |
14:00-15:30 Session 135H: New Applications (VSTTE)
New Applications
Chair:
Location: Maths LT2
| 14:00 | Relational Equivalence Proofs Between Imperative and MapReduce Algorithms (abstract) |
| 14:30 | Practical Methods for Reasoning about Java 8's Functional Programming Features (abstract) |
| 15:00 | Verification of Binarized Neural Networks via Inter-Neuron Factoring (abstract) |
14:00-15:30 Session 135I: Complexity / Applications (WST)
Chair:
Location: Blavatnik Seminar Room 4
| 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)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 1
| 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)
Location: Blavatnik Seminar Room 2
| 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)
Chair:
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)
Location: Blavatnik Seminar Room 3
| 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 137E: Poster Presentations and Panel Discussion (ReMOTE)
Chair:
Location: Maths Seminar C5
| 16:00 | Safety and Trust in Autonomous Driving (abstract) |
16:00-18:00 Session 137F (VEMDP)
Chair:
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)
Chair:
Location: Blavatnik Seminar Room 4
| 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) |