FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
PROGRAM

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

Sunday, July 1st

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

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

Discussions about UNIF 2018 issues and future of UNIF

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

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

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

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

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

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

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

Location: Balliol College
Sunday, July 8th

View this program: with abstractssession overviewtalk overview

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

View this program: with abstractssession overviewtalk overview

10:30-11:00Coffee Break
11:00-12:30 Session 45A: Security protocols I (CSF)
Location: Maths LT2
11:00
An extensive formal analysis of multi-factor authentication protocols (abstract)
11:30
Composition Theorems for CryptoVerif and Application to TLS 1.3 (abstract)
12:00
A Cryptographic Look at Multi-Party Channels (abstract)
11:00-12:30 Session 45B: Linear Logic (FSCD)
11:00
Proof nets for bi-intuitionistic linear logic (abstract)
11:30
Unique perfect matchings and proof nets (abstract)
12:00
Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories (abstract)
11:00-12:00 Session 45C: ITP Invited Talk: John Harrison (ITP)
Location: Blavatnik LT1
11:00
Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification (abstract)
11:00-12:40 Session 45D (LICS)
Location: Maths LT1
11:00
Definable decompositions for graphs of bounded linear cliquewidth (abstract)
11:20
Parameterized circuit complexity of model-checking on sparse structures (abstract)
11:40
Sequential Relational Decomposition (abstract)
12:00
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (abstract)
12:20
Regular and First Order List Functions (abstract)
11:00-12:40 Session 45E (LICS)
Location: Maths LT3
11:00
A theory of linear typings as flows on 3-valent graphs (abstract)
11:20
Cellular Cohomology in Homotopy Type Theory (abstract)
11:40
Free Higher Groups in Homotopy Type Theory (abstract)
12:00
Higher Groups in Homotopy Type Theory (abstract)
12:20
Strong Sums in Focused Logic (abstract)
11:00-12:15 Session 45F: SAT Invited Talk: Christoph Scholl (SAT)
11:00
Welcome to SAT 2018 (abstract)
11:05
Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (abstract)
12:00-12:30 Session 46 (ITP)
Location: Blavatnik LT1
12:00
Efficient Mendler-Style Lambda-Encodings in Cedille (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 47A: CSF Invited Talk: Srini Devadas (CSF)
Location: Maths LT2
14:00
Sanctum: Towards an Open-Source, Formally Verified Secure Processor (abstract)
14:00-15:30 Session 47C (ITP)
Location: Blavatnik LT1
14:00
Formalizing Implicative Algebras in Coq (abstract)
14:30
Software Tool Support for Modular Reasoning in Modal Logics of Actions (abstract)
15:00
The Coinductive Formulation of Common Knowledge (abstract)
14:00-15:40 Session 47D (LICS)
Location: Maths LT1
14:00
A modal mu perspective on solving parity games in quasipolynomial time. (abstract)
14:20
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (abstract)
14:40
Rational Synthesis Under Imperfect Information (abstract)
15:00
Playing with Repetitions in Data Words Using Energy Games (abstract)
15:20
Compositional game theory (abstract)
14:00-15:40 Session 47E (LICS)
Location: Maths LT3
14:00
Concurrency and Probability: Removing Confusion, Compositionally (abstract)
14:20
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (abstract)
14:40
Eager Functions as Processes (abstract)
15:00
Quasi-Open Bisimilarity with Mismatch is Intuitionistic (abstract)
15:20
Causal Computational Complexity of Distributed Processes (abstract)
14:00-15:30 Session 47F: MaxSAT (SAT)
14:00
Approximately Propagation Complete and Conflict Propagating Constraint Encodings (abstract)
14:30
Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (abstract)
15:00
Solving MaxSAT with Bit-Vector Optimization (abstract)
15:00-15:30 Session 48A: Attack trees (CSF)
Location: Maths LT2
15:00
Guided design of attack trees: a system-based approach (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 49B: Corrado Böhm Memorial (FSCD)
16:00
ALGORAND A Truly Distributed Ledger (abstract)
17:00
Corrado Böhm: the white magician in programming and its semantics (abstract)
16:00-18:00 Session 49C (ITP)
Location: Blavatnik LT1
16:00
Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (abstract)
16:30
Boosting the Reuse of Formal Specifications (abstract)
17:00
Formalization of a Polymorphic Subtyping Algorithm (abstract)
17:30
A Formal Equational Theory for Call-by-Push-Value (abstract)
16:00-18:00 Session 49D (LICS)
Location: Maths LT1
16:00
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (abstract)
16:20
A Simple and Optimal Complementation Algorithm for Büchi Automata (abstract)
16:40
The State Complexity of Alternating Automata (abstract)
17:00
Automaton-Based Criteria for Membership in CTL (abstract)
17:20
PTL-separability and closures for WQOs on words (abstract)
17:40
Regular Transducer Expressions for Regular Transformations over infinite words (abstract)
16:00-18:00 Session 49E (LICS)
Location: Maths LT3
16:00
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (abstract)
16:20
An algebraic theory of Markov processes (abstract)
16:40
Boolean-Valued Semantics for Stochastic Lambda-Calculus (abstract)
17:00
Sound up-to techniques and Complete abstract domains (abstract)
17:20
Every λ-Term is Meaningful for the Infinitary Relational Model (abstract)
17:40
Probabilistic Böhm Trees and Probabilistic Separation (abstract)
16:00-18:00 Session 49F: CDCL (SAT)
16:00
Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (abstract)
16:30
Machine Learning-based Restart Policy for CDCL SAT Solvers (abstract)
17:00
Chronological Backtracking (abstract)
17:30
Centrality-Based Improvements to CDCL Heuristics (abstract)
19:00-21:30 FLoC reception at Ashmolean Museum (FLoC)

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

Tuesday, July 10th

View this program: with abstractssession overviewtalk overview

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

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

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

View this program: with abstractssession overviewtalk overview

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

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

Thursday, July 12th

View this program: with abstractssession overviewtalk overview

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

AGENDA of FSCD18 General Meeting

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

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

Location: Balliol College
Friday, July 13th

View this program: with abstractssession overviewtalk overview

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

Panel session preceded by an introductory talk.

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

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

Location: Keble College
Saturday, July 14th

View this program: with abstractssession overviewtalk overview

10:00-10:30 Session 91A: Program verification (F-IDE)
10:00
Lightweight Interactive Proving inside an Automatic Program Verifier (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 92A: Model Checking (CAV)
Location: Maths LT1
11:00
Propositional Dynamic Logic for Higher-Order Functional Programs (abstract)
11:15
Syntax-Guided Termination Analysis (abstract)
11:30
Model Checking Quantitative Hyperproperties (abstract)
11:45
Exploiting Synchrony and Symmetry in Relational Verification (abstract)
12:00
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (abstract)
12:15
Eager Abstraction for Symbolic Model Checking (abstract)
11:00-12:30 Session 92B: 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 92C: User interfaces for formal tools (F-IDE)
11:00
User Support for the Combinator Logic Synthesizer Framework (abstract)
11:30
AsmetaF: a flattener for the ASMETA framework (abstract)
12:00
Improving the Visualization of Alloy Instances (abstract)
11:00-12:30 Session 92D: Ally Skills (FLoC)

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

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

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

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

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

Chair:
11:00
Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs (abstract)
11:20
ViennaVM: a Virtual Machine for VDM-SL development (abstract)
11:40
Multi-modelling of Cooperative Swarms (abstract)
12:00
Design Space Exploration for Secure Building Control (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 93A: 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 93B (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 93D: Foundations II (ICLP)
14:00
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (abstract)
14:30
First-order answer set programming as constructive proof search (abstract)
15:00
Solving Horn Clauses on Inductive Data Types Without Induction (abstract)
14:00-15:30 Session 93E: SAT Extensions & Applications (IJCAR)
Location: Maths LT2
14:00
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (abstract)
14:30
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (abstract)
15:00
A New Probabilistic Algorithm for Approximate Model Counting (abstract)
14:50-15:30 Session 94: Overture: Perspectives and Methods (Overture)

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

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

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

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

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

Sunday, July 15th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 98B (FM)
Location: Blavatnik LT1
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 98C: ICLP Invited Talk: Elvira Albert (ICLP)
Chair:
09:00
Avoiding redundancies in the exploration of concurrent programs (abstract)
09:00-10:30 Session 98D: Logics and Calculi (IJCAR)
Location: Maths LT2
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 98E: SAT (IJCAR)
Location: Maths LT3
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)
10:00-10:30 Session 99A: Learning (CAV)
Location: Maths LT1
10:00
Learning Abstractions for Program Synthesis (abstract)
10:15
The Learnability of Symbolic Automata (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 100A: Runtime Verification, Hybrid and Timed Systems (CAV)
Location: Maths LT1
11:00
Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (abstract)
11:15
Spacetime Interpolants (abstract)
11:30
Monitoring Weak Consistency (abstract)
11:45
Monitoring CTMCs By Multi-Clock Timed Automata (abstract)
12:00
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (abstract)
12:15
A Counting Semantics for Monitoring LTL Specifications over Finite Traces (abstract)
11:00-12:00 Session 100B: FM Invited Talk: Annabelle McIver (FM)
Location: Blavatnik LT1
11:00
Privacy in Text Processing: An information flow perspective (abstract)
11:00-12:30 Session 100C: Implementation I (ICLP)
11:00
Top-down and Bottom-up Evaluation Procedurally Integrated (abstract)
11:30
Certified Graph View Maintenance with Regular Datalog (abstract)
12:00
An iterative approach to precondition inference using constrained Horn clauses (abstract)
11:00-12:30 Session 100D: Formal Proofs (IJCAR)
Location: Maths LT2
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 100E: SMT 2 (IJCAR)
Location: Maths LT3
11:00
Exploring Approximations for Floating-Point Arithmetic using UppSAT (abstract)
11:30
Datatypes with Shared Selectors (abstract)
12:00
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 102A: 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 102C: Learning and Reasoning (ICLP)
14:00
Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (abstract)
14:30
Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (abstract)
15:00
A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (abstract)
14:00-15:00 Session 102D: IJCAR Invited Talk: Martin Giese (IJCAR)
Location: Maths LT2
14:00
Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 104A: Probabilistic Systems (CAV)
Location: Maths LT1
16:00
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (abstract)
16:15
Sound Value Iteration (abstract)
16:30
Safety-Aware Apprenticeship Learning (abstract)
16:45
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (abstract)
16:00-18:00 Session 104B (FM)
Location: Blavatnik LT1
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 104C: Technical Communications I (ICLP)
16:00
Cumulative Scoring-based Induction of Default Theories (abstract)
16:15
Epistemic Logic Programs with World View Constraints (abstract)
16:30
SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (abstract)
16:45
Introspecting Preferences In Answer Set Programming (abstract)
17:00
Application of Logic-Based Methods to Machine Component Design (abstract)
17:15
Improving Candidate Quality of Probabilistic Logic Models (abstract)
17:30
Natural Language Generation From Ontologies: Application Paper (abstract)
17:45
MASP-Reduce: a proposal for distributed computation of stable models (abstract)
16:00-18:00 Session 104D: Logics, Frameworks and Proofs (IJCAR)
Location: Maths LT2
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 104E: Verification (IJCAR)
Location: Maths LT3
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 106A: Tools (CAV)
Location: Maths LT1
09:00
Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (abstract)
09:15
MaxSMT-Based Type Inference for Python 3 (abstract)
09:30
The JKind Model Checker (abstract)
09:45
The DEEPSEC prover (abstract)
10:00
SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (abstract)
10:15
StringFuzz: A Fuzzer for String Solvers (abstract)
09:00-10:30 Session 106C: Language and Reasoning (ICLP)
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 106D: Decidability & Complexity (IJCAR)
Location: Maths LT2
09:00
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (abstract)
09:30
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (abstract)
10:00
Focussing, MALL and the polynomial hierarchy (abstract)
10:00-10:30 Session 107 (FM)
Location: Blavatnik LT1
10:00
Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 108B (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 108C (FM)
Location: Blavatnik LT2
11:00
Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (abstract)
11:30
Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (abstract)
12:00
Verifying Auto-Generated C Code from Simulink (abstract)
11:00-12:30 Session 108E: Superposition (IJCAR)
Location: Maths LT2
11:00
Superposition with Datatypes and Codatatypes (abstract)
11:30
Superposition for Lambda-Free Higher-Order Logic (abstract)
12:00
Efficient encodings of first-order Horn formulas in equational logic (abstract)
12:00-12:30 Session 110: Static Analysis (CAV)
Location: Maths LT1
12:00
Permission Inference for Array Programs (abstract)
12:15
Program Analysis is Harder than Verification: A Computability Perspective (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 111: FLoC Plenary Lecture: Byron Cook (FLoC)
Location: Maths LT1
14:00
Formal Reasoning about the Security of Amazon Web Services (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 112B (FM)
Location: Blavatnik LT1
16:00
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (abstract)
16:30
Modular Verification of Programs with Effects and Effect Handlers in Coq (abstract)
17:00
Combining Tools for Optimization and Analysis of Floating-Point Computations (abstract)
17:30
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (abstract)
16:00-18:00 Session 112C (FM)
Location: Blavatnik LT2
16:00
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (abstract)
16:30
Multi-Robot LTL Planning Under Uncertainty (abstract)
17:00
Vector Barrier Certificates and Comparison Systems (abstract)
17:30
Timed Vacuity (abstract)
19:00-21:30 FLoC banquet at Ashmolean Museum (FLoC)

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

Tuesday, July 17th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 114A: Theory and Security (CAV)
Location: Maths LT1
09:00
Automata vs Linear-Programming Discounted-Sum Inclusion (abstract)
09:15
Model checking indistinguishability of randomized security protocols (abstract)
09:30
Lazy Self-Composition for Security Verification (abstract)
09:45
SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (abstract)
10:00
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (abstract)
10:15
Attracting Tangles to Solve Parity Games (abstract)
09:00-10:30 Session 114B (FM)
Location: Blavatnik LT1
09:00
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (abstract)
09:30
Dynamic Symbolic Verification of MPI Programs (abstract)
10:00
To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation (abstract)
09:00-10:30 Session 114C: FM I-Day (FM)
Location: Blavatnik LT2
09:00
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (abstract)
09:30
Interlocking Design Automation using Prover Trident (abstract)
10:00
Model-Based Testing for Avionics Systems (abstract)
09:00-10:00 Session 114E: IJCAR Invited Talk: Erika Abraham (IJCAR)
Location: Maths LT2
09:00
Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics (abstract)
10:00-10:30 Session 115: SMT 3 (IJCAR)
Location: Maths LT2
10:00
A Separation Logic with Data: Small Models and Automation (abstract)
10:30-11:00Coffee Break
11:00-12:15 Session 116A: SAT, SMT and Decision Procedures (CAV)
Location: Maths LT1
11:00
Delta-Decision Procedures for Exists-Forall Problems over the Reals (abstract)
11:15
Solving Quantified Bit-Vectors using Invertibility Conditions (abstract)
11:30
Understanding and Extending Incremental Determinization for 2QBF (abstract)
11:45
The Proof Complexity of SMT Solvers (abstract)
12:00
Model Generation for Quantified Formulas: A Taint-Based Approach (abstract)
11:00-12:30 Session 116C: Applications (ICLP)
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 116D: AR Miscellanea (IJCAR)
Location: Maths LT2
11:00
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (abstract)
11:30
Automated Reasoning about Key Sets (abstract)
12:00
An abstraction-refinement framework for reasoning with large theories (abstract)
12:00-12:30 Session 117 (FM)
Location: Blavatnik LT1
12:00
View abstraction for systems with component identities (abstract)
12:30-14:00Lunch Break
14:00-15:15 Session 118A: Concurrency (CAV)
Location: Maths LT1
14:00
Partial Order Aware Concurrency Sampling (abstract)
14:15
Reasoning About TSO Programs Using Reduction and Abstraction (abstract)
14:30
Quasi-Optimal Partial Order Reduction (abstract)
14:45
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (abstract)
15:00
Constrained Dynamic Partial Order Reduction (abstract)
14:00-15:30 Session 118B (FM)
Location: Blavatnik LT1
14:00
Compositional Reasoning for Shared-variable Concurrent Programs (abstract)
14:30
Statistical Model Checking of LLVM Code (abstract)
15:00
A lightweight deadlock analysis technique of object-oriented programs (abstract)
14:00-15:30 Session 118C: FM I-Day (FM)
Location: Blavatnik LT2
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 118D: Probabilistic and Constraint LP (ICLP)
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 118E: 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 119A: CPS, Hardware, Industrial Applications (CAV)
Location: Maths LT1
16:00
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (abstract)
16:15
Continuous formal verification of Amazon s2n (abstract)
16:30
Symbolic Liveness Analysis of Real-World Software (abstract)
16:45
Model Checking Boot Code from AWS Data Centers (abstract)
17:00
Android Stack Systems (abstract)
17:15
Formally Verified Montgomery Multiplication (abstract)
17:30
Inner and Outer Approximating Flowpipes for Delay Differential Equations (abstract)
16:00-18:00 Session 119B (FM)
Location: Blavatnik LT1
16:00
CompoSAT: Specification-Guided Coverage for Model Finding (abstract)
16:30
Approximate Partial Order Reduction (abstract)
17:00
SDN-Actors: Modeling and Verification of SDN Programs (abstract)
17:30
Formal Specification and Verification of Dynamic Parametrized Architectures (abstract)
16:00-17:30 Session 119C: FM I-Day (FM)
Location: Blavatnik LT2
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 119D: 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:
16:30-18:00 Session 120: Technical Communications II (ICLP)
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 121A: ARQNL Invited Talk: Larry Moss (ARQNL)
09:00
Automated Reasoning In Natural Language: Current Directions (abstract)
09:00-10:30 Session 121B (ASPOCP)
09:00
Invited Talk: Optimization Problems in Answer Set Programming (abstract)
10:00
anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report) (abstract)
09:00-10:30 Session 121C: Invited talk: Michael Tautschnig (AVOCS)

Formal Methods at Amazon Web Services

09:00
Experiences with thread-modular static analysis of concurrent embedded systems (abstract)
09:00-10:30 Session 121D (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 121E: Logic and Practice of Programming (LPOP)
09:00
Opening and introduction (abstract)
09:10
Invited Talk: Practical uses of Logic, Formal Methods, B and ProB (abstract)
09:50
Invited Talk: On the Development of Industrial Applications with ASP (abstract)
09:00-10:30 Session 121F: Practical MSO Model Checking 1 (LaSh)
09:00
Monadic Second-Order Model Checking with Fly-Automata (abstract)
10:05
Lazy Automata Techniques for WS1S (abstract)
09:00-10:30 Session 121H: Industrial Session (NSV)
09:00
Needs in formal methods for the validation of naval systems (abstract)
09:45
Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering (abstract)
09:00-10:30 Session 121I: Parallel graph algorithms (PLR)

On parallel algorithms working with graphs.

Chair:
09:00
Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications (abstract)
09:45
MASP-Reduce: a proposal for distributed computation of stable models (abstract)
09:00-10:30 Session 121J (REFINE)
Location: Blavatnik LT2
09:00
Automated verification of linearizability (abstract)
10:00
Correctness of Concurrent Objects under Weak Memory Models (abstract)
09:00-10:30 Session 121K (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 121L (TLA)
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 121M (ThEdu)
09:00
Students' Proof Assistant (SPA) (abstract)
09:30
Natural Deduction Assistant (NaDeA) (abstract)
10:00
Rating of Geometric Automated Theorem Provers (abstract)
09:00-10:30 Session 121N: Model Checking I (VSTTE)

Model Checking I

Location: Maths LT2
09:00
A Tree-Based Approach to Data Flow Proofs (abstract)
09:00-10:30 Session 121P: Invited Speaker; Distributed Systems I (VaVAS)

Invited Speaker

Contributed Talks: Distributed Systems I

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

Automated verification

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

Techniques to verify parallel programs.

 

Chair:
11:00
Permission Inference for Array Programs (abstract)
11:45
RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL (abstract)
11:00-12:30 Session 123J (REFINE)
Location: Blavatnik LT2
11:00
Challenges of specifying concurrent program components (abstract)
11:30
Programming Without Refinement (abstract)
12:00
Ordering strict partial orders to model behavioural refinement (abstract)
11:00-12:30 Session 123K (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 123L (TLA)
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 123M (ThEdu)
11:00
Lucas Interpretation from Programmers’ Perspective (abstract)
11:30
GeoCoq: formalized foundations of geometry (abstract)
11:00-12:30 Session 123N: Model Checking II (VSTTE)

Model Checking II

Location: Maths LT2
11:00
Executable Counterexamples in Software Model Checking (abstract)
11:30
Extending VIAP to Handle Array Programs (abstract)
12:00
Lattice-Based Refinement in Bounded Model Checking (abstract)
11:00-12:30 Session 123P: Distributed Systems II (VaVAS)

Contributed Talks: Distributed Systems II

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

Automatic Verification of Concurrent Objects

14:00
Automatic Verification of Concurrent Objects (abstract)
14:00-15:30 Session 124D (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 124E: Challenge Solutions and Constraint Solving (LPOP)
14:00
Panel: Practice of Modeling and Programming (abstract)
14:30
Invited Talk: A Modeling Language Based on Semantic Typing (abstract)
15:10
A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding (abstract)
15:20
Confluence Analysis of Cognitive Models with Constraint Handling Rules (abstract)
14:00-15:30 Session 124F: Frameworks (LaSh)
14:00
Declarative Dynamic Programming with Inverse Coupled Rewrite Systems (abstract)
15:00
A Logic of Information Flows (abstract)
14:00-15:30 Session 124H: Hybrid systems verification (NSV)
14:00
Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation (abstract)
14:30
Parallel reachability analysis of hybrid systems in XSpeed (abstract)
15:00
The Policy Iterations Algorithm is Actually a Newton Method (abstract)
14:00-15:30 Session 124I: Parallel SAT solving (PLR)

Parallel approaches to perform SAT solving.

Chair:
14:00
Tuning Parallel SAT Solvers (abstract)
14:45
GPU Accelerated SAT solving (abstract)
14:00-15:30 Session 124J (REFINE)
Location: Blavatnik LT2
14:00
A more relaxed way to make concrete: uses of heuristic search to discover implementations (abstract)
14:00-15:30 Session 124K (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 124L (TLA)
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 124M (ThEdu)
14:00
Towards intuitive reasoning in axiomatic geometry (abstract)
14:30
Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable (abstract)
15:00
edukera, an online proof assistant to Logic and Math (abstract)
14:00-15:30 Session 124N: Certification & Formalisation I (VSTTE)

Certification & Formalisation I

Location: Maths LT2
14:00
Invited Talk, TBA (abstract)
15:00
Verified Certificate Checking for Counting Votes (abstract)
14:00-15:30 Session 124P: Invited Speaker; Autonomous Vehicles I (VaVAS)

Invited Speaker

Contributed Talks: Autonomous Vehicles I

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

On parallel algorithms to solve parity games.

 

Chair:
16:00
Using work-stealing to parallelize symbolic algorithms and parity game solvers (abstract)
16:45
An Efficient Zielonka's Algorithm for Parallel Parity Games (abstract)
16:00-18:00 Session 126I (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 126J (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
TBA (abstract)
16:00-18:00 Session 126K (TLA)
16:00
Invariants in Distributed Algorithms (abstract)
16:45
Proving properties of a minimal covering algorithm (abstract)
16:00-18:00 Session 126L (ThEdu)

ThEdu Bussiness Meeting

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

Certification & Formalisation II

Location: Maths LT2
16:00
Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications (abstract)
16:30
TWAM: A Certifying Abstract Machine for Logic Programs (abstract)
17:00
A Java bytecode formalisation (abstract)
17:30
Formalising Executable Specifications of Low-Level Systems (abstract)
16:00-18:00 Session 126N: Autonomous Vehicles II (VaVAS)

Contributed Talks: Autonomous Vehicles II

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)
19:15-21:30 Workshops dinner at Magdalen College (FLoC)

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

Thursday, July 19th

View this program: with abstractssession overviewtalk overview

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

Experiences with thread-modular static analysis of concurrent embedded systems

09:00
Experiences with thread-modular static analysis of concurrent embedded systems (abstract)
09:00-10:30 Session 127B (EICNCL)
09:00
Title TBA - Invited talk (abstract)
10:00
Effective Translations between Display and Labelled Proofs for Tense Logics (abstract)
09:00-10:30 Session 127D: Welcome and Invited Talk (PAAR)
Location: Maths LT3
09:00
The CakeML Verified Compiler and Toolchain (abstract)
10:00
Dynamic Strategy Priority: Empower the strong and abandon the weak (abstract)
09:00-10:30 Session 127E: Welcome & invited talk I (PRUV)
09:00
Welcome to PRUV (abstract)
09:10
Quantitative Logic Reasoning -- Combining logical reasoning with probabilities and counting (invited talk) (abstract)
09:00-10:30 Session 127F: Opening and First Presentation Round (ReMOTE)
09:00
Welcome and Introduction (abstract)
09:15
Understanding Ethical Reasoning (abstract)
09:45
Human morality, robots’ moral competence, and the deepest kind of trust (abstract)
10:15
Elements of a Model of Trust in Technology (abstract)
09:00-10:00 Session 127G: 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 127H: Certification & Formalisation III (VSTTE)

Certification & Formalisation III

Location: Maths LT2
09:00
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars (abstract)
09:00-10:30 Session 127I: Invited Speaker; Robotics I (VaVAS)

Invited Speaker

Contributed Talks: Robotics I

Location: Maths LT1
09:00
Reproducibility in Robotics - The Big 5 Issues (abstract)
10:00
RoboTool: Modelling and Verification with RoboChart (abstract)
10:00-10:30 Session 128 (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 129A: AVoCS Regular Papers 3 (AVOCS)
11:00
Using SMT engine to generate Symbolic Automata (abstract)
11:30
Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (abstract)
12:00
A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (abstract)
11:00-12:30 Session 129B: Modal logics (EICNCL)
11:00
Toward intuitionistic non-normal modal logic and its calculi (abstract)
11:30
Proof theory for quantified monotone modal logics (abstract)
12:00
Sequent Calculi for Logic that Includes an Infinite Number of Modalities (abstract)
11:00-12:30 Session 129C (MLP)
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 129D: Automated Reasoning I (PAAR)
Location: Maths LT3
11:00
A Verified Simple Prover for First-Order Logic (abstract)
11:30
Proof Search Optimizations for Non-clausal Connection Calculi (abstract)
12:00
TFX: The TPTP Extended Typed First-order Form (abstract)
11:00-12:30 Session 129E: PRUV regular papers (PRUV)

PRUV regular papers

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

Security

Location: Maths LT2
11:00
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components (abstract)
11:30
SideTrail: Verifying Time-Balancing of Cryptosystems (abstract)
12:00
Towards verification of Ethereum smart contracts: a formalization of core of Solidity (abstract)
11:00-11:30 Session 129I: Robotics II (VaVAS)

Contributed Talks: Robotics II

Location: Maths LT1
11:00
Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot (abstract)
11:00-12:30 Session 129J: Complexity (WST)
11:00
Complexity Analysis for Bitvector Programs (abstract)
11:30
A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving (abstract)
12:00
Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 131A: Invited talk: Yannick Moy (AVOCS)

Mostly harmless - luring programmers into proof with SPARK

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

New Applications

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

Off the beaten track

Location: Maths LT2
16:00
The Map Equality Domain (abstract)
16:30
Loop Detection by Logically Constrained Term Rewriting (abstract)
17:00
Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment (abstract)
16:00-17:00 Session 133H: Higher-Order (WST)
16:00
Termination of Lambda-Pi modulo rewriting using the size-change principle (abstract)
16:30
Improving Static Dependency Pairs for Higher-Order Rewriting (abstract)