FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
PROGRAM

Days: 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

Saturday, July 7th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 1C (Domains13)
09:00
Looking Backward; Looking Forward ( abstract )
10:00
A Brouwerian proof of the Fan Theorem ( abstract )
09:00-10:30 Session 1D (GS)
09:00
TBA ( abstract )
10:00
"Operational'' Game Semantics ( abstract )
09:00-10:30 Session 1E (HDRA)
09:00
Homotopy coherent adjunctions and other structures ( abstract )
10:00
Merge-bicategories: towards semi-strictification of higher categories ( abstract )
09:00-10:30 Session 1F (HOR)
09:00
On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification ( abstract )
10:00
Combinatorics of explicit substitutions (extended abstract) ( abstract )
09:00-10:30 Session 1G: 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
Critical pairs for Gray categories ( abstract )
09:00-10:30 Session 1I: Amiga (LOLA)
09:00
Asynchronous games fifteen years later ( abstract )
09:30
Invited talk: Generating and Verifying C ( abstract )
09:00-10:30 Session 1J (Linearity/TLLA)
09:00
Substructural Calculi with Dependent Types ( abstract )
09:20
On the Lambek Calculus with an Exchange Modality ( abstract )
09:55
How to count linear and affine closed lambda terms? ( abstract )
09:00-10:30 Session 1K (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 1M: Tuning solvers and applications (POS)
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 1P: switch (TYDI-0)
09:00
An introduction to deep inference ( abstract )
10:00
Deep-Inference Intersection Types ( abstract )
09:00-10:30 Session 1Q: Invited Talk, and orders and sets of E-unifiers (UNIF)
09:00
Handling substitutions via duality ( abstract )
10:00
Unification based on generalized embedding ( abstract )
09:30-10:30 Session 2A (HoTT/UF)
09:30
Axiomatizing Cubical Sets Models of Univalent Foundations ( abstract )
09:30-10:30 Session 2B: Invited Talk (TERMGRAPH)
09:30
Critical Pairs in Graph Transformation Systems ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 3C (Domains13)
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 3D (GS)
11:00
Some reflections on algorithmic game semantics ( abstract )
11:30
TBA ( abstract )
11:00-12:30 Session 3E (HDRA)
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:30 Session 3F (HOR)
11:00
Wanda: a higher-order termination tool ( abstract )
12:00
Orthogonality and sequentiality in substructural Linear HRSs ( abstract )
11:00-12:30 Session 3G (HoTT/UF)
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 3H: Algebraic Structures and Coherence (IWC)
11:00
Coherence of monoids by insertions ( abstract )
11:30
Coherence modulo relations ( abstract )
12:00
The diamond lemma for free modules ( abstract )
11:00-12:30 Session 3J: 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:30 Session 3K (Linearity/TLLA)
11:00
Termination of lambda-calculus linearization methods ( abstract )
12:00
Taking Linear Logic Apart ( abstract )
11:00-12:30 Session 3L: Contributed papers (NLCS)
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 3N: Pseudo-Boolean and Proofs (POS)
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 3Q: 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 3R: promotion (TYDI-0)
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 3S: 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:30-14:00Lunch Break
14:00-15:30 Session 4C (Domains13)
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 4D (GS)
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 4F (HOR)
14:00
Some applications of quantitative types inside and outside type theory ( abstract )
15:00
Refining Properties of Filter Models: Sensibility, Approximability and Reducibility ( abstract )
14:00-15:30 Session 4G: Term Rewriting (IWC)
14:00
Certified Ordered Completion ( abstract )
14:30
Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL ( abstract )
15:00
Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs ( abstract )
14:00-15:30 Session 4I (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 4J: Contributed papers (NLCS)
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 4L (PC)
14:00
Space Proof Complexity beyond Resolution ( abstract )
14:00-15:30 Session 4M: MAXSAT & local search (POS)
14:00
Pseudo-Random Number Generators for Multi-Threaded Stochastic Local Search ( abstract )
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 )
14:00-15:30 Session 4N: Determinacy, compositionality (SR)
14:00
Compositional Game Theory ( abstract )
14:40
Concurrent games and semi-random determinacy ( abstract )
14:00-15:30 Session 4P: 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 4Q: Medial (TYDI-0)
14:00
Two Unifying Structural Principles ( abstract )
15:00
Deep Inference, Herbrand's Theorem and Expansion Proofs ( abstract )
14:00-15:30 Session 4R: 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 5: Commodore (LOLA)
14:30
Invited talk: Semantic Equivalence Checking for HHVM Bytecode ( abstract )
15:00-15:30 Session 6A (HDRA)
15:00
Towards a fully formalized definition of syllepsis in weak higher categories ( abstract )
15:00-15:30 Session 6B (HoTT/UF)
15:00
Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT ( abstract )
15:30-16:00Coffee Break
16:00-16:50 Session 7C (Domains13)
16:00
Higher-dimensional categories: recursion on extensivity ( abstract )
16:25
A logical view of complex analytic maps ( abstract )
16:00-18:00 Session 7D (GS)
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 7E (HDRA)
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-18:00 Session 7F (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 7G (HoTT/UF)
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 7H: Applications and Business Meeting (IWC)
16:00
Complete Axiom System of Cluster Algebra ( abstract )
16:30
IWC Business Meeting ( abstract )
16:00-18:00 Session 7J: 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:00 Session 7K (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 7L: 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 7P: SAT pragmatics (POS)
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 7Q: 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 7R: 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 7S: Contraction (TYDI-0)
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 7T: 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 )
19:45-22:00 Session : 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).

Sunday, July 8th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 9A (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 9B (Coq)
09:00
Verifying Distributed Systems ( abstract )
10:00
Procrastination, A proof engineering technique ( abstract )
09:00-10:30 Session 9C (DCM)
09:00
Quantitative types: from Foundations to Applications ( abstract )
10:00
Models of Computation that Conserve Data ( abstract )
09:00-10:30 Session 9D (Domains13)
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 9E: 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 9F (GS)
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 9G: 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 9I (ITRS)
09:00
Quantitative types: from Foundations to Applications. (ITRS/DCM joint invited talk) ( abstract )
10:00
On sets of terms with a given intersection type ( abstract )
09:00-10:30 Session 9J (Linearity/TLLA)
09:00
Towards a Functional Language for Species of Structures ( abstract )
09:20
The Bang Calculus and the Two Girard's Translations ( abstract )
09:55
Entropy and Complexity Lower Bounds ( abstract )
09:00-10:30 Session 9K (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 9M: Joint QBF / Proof Complexity session (PC and QBF)
09:00
Lower Bound Techniques for QBF Proof Systems ( abstract )
10:00
Towards the Semantics of QBF Clauses ( abstract )
09:00-10:30 Session 9Q (WiL)
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 10 (HoTT/UF)
09:30
Injective types and searchable types in univalent mathematics ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 11A (COALG)
11:00
Coalgebra and Automated Reasoning ( abstract )
11:45
Coalgebraic Tools for Randomness-Conserving Protocols ( abstract )
11:00-12:30 Session 11B (Coq)
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 11C (DCM)
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 11D (Domains13)
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 11E: 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 11F (GS)
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 11G: 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 11H (HoTT/UF)
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 11J (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 11K (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 11L (MSFP)
11:00
Formalizing Constructive Quantifier Elimination in Agda ( abstract )
11:45
Everybody's Got To Be Somewhere ( abstract )
11:00-12:30 Session 11N: Joint QBF / Proof Complexity session (PC and QBF)
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 11Q (WPTE)
11:00
Optimizing Space of Parallel Processes ( abstract )
11:30
Automating the Diagram Method to Prove Correctness of Program Transformations ( abstract )
12:00
On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems ( abstract )
11:00-12:30 Session 11R (WiL)
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 )
12:15
Stable regularity for relational structures ( abstract )
12:30-14:00Lunch Break
14:00-15:30 Session 12A (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 12B (Coq)
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 12C (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 12D (Domains13)
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 12E: Cryptography (FCS)
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 12F (GS)
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 12G: 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 12H (HoTT/UF)
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 12J (ITRS)
14:00
Intersection Types for Unboundedness Problems (ITRS invited talk) ( abstract )
15:00
Gradual Intersection Types ( abstract )
14:00-15:30 Session 12K (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 12L (MSFP)
14:00
Ornamentation put into practice in ML ( abstract )
15:00
Profunctor Optics and the Yoneda Lemma ( abstract )
14:00-15:30 Session 12P (QBF)
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 12Q: 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 12R (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 12S (WiL)
14:00
POPLMark Reloaded: Mechanizing Logical Relations Proofs ( abstract )
15:00
Towards a Playground for Logicians ( abstract )
15:15
On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving ( abstract )
15:30-16:00Coffee Break
16:00-18:00 Session 13A (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 13B (Coq)
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-18:00 Session 13C (DCM)
16:00
Polyadic approximations and intersection types (ITRS/DCM joint invited talk) ( abstract )
17:00
Generic Graph Semantics ( abstract )
16:00-17:40 Session 13D (Domains13)
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 13E (GS)
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 13F: Technical Papers and Closing Remarks (GraMSec)
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 13G (HoTT/UF)
16:00
(Truncated) Simplicial Models of Type Theory ( abstract )
16:30
Towards the syntax and semantics of higher dimensional type theory ( abstract )
16:00-18:00 Session 13I (ITRS)
16:00
Intersection Subtyping with Constructors ( abstract )
16:30
Polyadic approximations and intersection types (ITRS/DCM joint invited talk) ( abstract )
16:00-18:00 Session 13J (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-18:00 Session 13K (MSFP)
16:00
Backward induction for repeated games ( abstract )
16:45
Relating Idioms, Arrows and Monads from Monoidal Adjunctions ( abstract )
16:00-18:00 Session 13M (PC)
16:00
A Comparison of Algebraic and Semi-Algebraic Proof Systems ( abstract )
16:00-18:00 Session 13N (QBF)
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 13P: 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 13R (WiL)
16:00
Non-well-founded proof system for Transitive Closure Logic ( abstract )
16:15
Hilbert Meets Isabelle ( abstract )
16:30
Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? ( abstract )
16:45
Towards a Logical Framework for Latent Variable Modelling ( abstract )
Monday, July 9th

View this program: with abstractssession overviewtalk overview

10:30-11:00Coffee Break
11:00-12:30 Session 16A: Security protocols I (CSF)
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 16B: 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 16C: ITP Invited Talk: John Harrison (ITP)
11:00
Mike Gordon: Tribute to a pioneer in theorem proving and formal verification ( abstract )
11:00-12:40 Session 16D (LICS)
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 16E (LICS)
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 16F: SAT Invited Talk: Christoph Scholl (SAT)
11:00
Welcome to SAT 2018 ( abstract )
11:15
Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications ( abstract )
12:00-12:30 Session 17 (ITP)
12:00
Efficient Mendler-Style Lambda-Encodings in Cedille ( abstract )
12:30-14:00Lunch Break
14:00-15:00 Session 18A: CSF Invited Talk: Srini Devadas (CSF)
14:00
Sanctum: Towards an Open-Source, Formally-Verified Secure Processor ( abstract )
14:00-15:30 Session 18C (ITP)
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 18D (LICS)
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 18E (LICS)
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 18F: 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 19A: Attack trees (CSF)
15:00
Guided design of attack trees: a system-based approach ( abstract )
15:00-15:30 Session 19B: Quantum Computing (FSCD)
15:00
A diagrammatic axiomatisation of fermionic quantum circuits ( abstract )
15:30-16:00Coffee Break
16:00-18:00 Session 20B: 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 20C (ITP)
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 20D (LICS)
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 20E (LICS)
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 20F: 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 Session : 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 21A: Cryptographic primitives (CSF)
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 21B: 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 21C: ITP Invited Talk: Dan Grayson (ITP)
09:00
Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics ( abstract )
09:00-10:30 Session 21E: 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 22A (ITP)
10:00
CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math” ( abstract )
10:00-10:40 Session 22B (LICS)
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 23A: Secure computation (CSF)
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 23B: 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 23C (ITP)
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 23D (LICS)
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 23E (LICS)
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 24A: Knowledge and hyperproperties (CSF)
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 24B: FSCD Invited talk: Valeria Vignudelli (FSCD)
14:00
Proof techniques for program equivalence in probabilistic higher-order languages ( abstract )
14:00-15:30 Session 24C (ITP)
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 24D (LICS)
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 24E (LICS)
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 24F: QBF I (SAT)
14:00
Circuit-based Search Space Pruning in QBF ( abstract )
14:30
Symmetries for QBF ( abstract )
15:00
Local Soundness for QBF Calculi ( abstract )
15:00-15:30 Session 25: Types (FSCD)
15:00
A Syntax for Higher Inductive-Inductive Types ( abstract )
15:30-16:00Coffee Break
16:00-17:00 Session 26B: 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 26C (ITP)
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 26D (LICS)
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 26E (LICS)
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 26F: 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 27: 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:00 Session 28A: invited talk - Jungers, Raphael (ADHS)
09:00
Provably efficient algorithms on hybrid automata ( abstract )
09:00-10:30 Session 28B: Information flow (CSF)
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 28C: 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 28D (ITP)
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 28F: 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 28G: Sc-square Invited speaker (SCSC)
09:00
Hard Combinatorial Problems: A Challenge for Satisfiability ( abstract )
10:00-10:40 Session 29 (LICS)
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 30 (SCSC)
10:05
RP: Refutation of Products of Linear Polynomials ( abstract )
10:30-11:00Coffee Break
10:50-12:30 Session 31A: 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 31B: 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 32A: CSF Invited Talk: Catuscia Palamidessi (CSF)
11:00
Local Differential Privacy on Metric Spaces: optimizing the trade-off with utility ( abstract )
11:00-12:30 Session 32B: 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 32C (ITP)
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 32D (LICS)
Chair:
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 32E (LICS)
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:30 Session 32G (SCSC)
11:00
RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics ( abstract )
11:25
RP A Practical Polynomial Calculus for Arithmetic Circuit Verification ( abstract )
11:50
EA-New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square ( abstract )
12:10
EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT ( abstract )
12:00-12:30 Session 33: Privacy (CSF)
12:00
Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting ( abstract )
12:30-14:00Lunch Break
14:00-15:40 Session 34B: 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 34C: 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 34D (SCSC)
14:00
RP Evaluation of Equational Constraints for CAD in SMT Solving ( abstract )
14:25
RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple ( abstract )
14:50
EA: SMT-like Queries in Maple ( abstract )
15:10
EA Techniques for Natural-style Proofs in Elementary Analysis ( abstract )
15:30-16:00Coffee Break
16:00-17:00 Session 35A: Electronic voting (CSF)
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 35B: FSCD Invited talk: Grigore Rosu (FSCD)
16:00
Formal Design, Implementation and Verification of Blockchain Languages ( abstract )
16:00-18:00 Session 35C (ITP)
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 35E: 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 35F (SCSC)
16:00
RP: Unknot Recognition Through Quantifier Elimination ( abstract )
16:25
EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving ( abstract )
16:10-17:25 Session 36A: 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 36B: 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 37B: LICS Award Session & Martin Hofmann Memorial (LICS)
Chair:
17:00
LICS Awards: The Kleene Award and the Test of Time Award ( abstract )
18:00
Remembering Martin Hofmann ( abstract )
19:00-21:30 Session : 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 38A: invited talk - Belta, Calin (ADHS)
09:00
Formal Synthesis of Control Strategies for Dynamical Systems ( abstract )
09:00-10:00 Session 38B: FSCD Invited talk: Stéphanie Delaune (FSCD)
09:00
Analysing privacy-type properties in cryptographic protocols ( abstract )
09:00-10:30 Session 38C (ITP)
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 38D (LICS)
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
Two complete axiomatisations of pure-state qubit quantum computing ( abstract )
10:00
Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics ( abstract )
10:20
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics ( abstract )
09:00-10:40 Session 38E (LICS)
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 38F (SMT)
09:00
Invited talk: Automating Separation Logics using SMT ( abstract )
10:00
Revisiting Enumerative Instantiation ( abstract )
09:30-10:30 Session 39: 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 41A: 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 41B: 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 42A: Security protocols II (CSF)
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 42B: 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 42C (ITP)
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 42D: LICS Invited Talk: Val Tannen (LICS)
Chair:
11:00
Provenance Analysis for First-order Model Checking ( abstract )
11:00-12:00 Session 42E: 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 )
11:00-12:30 Session 42F (SMT)
11:00
Building Better Bit-Blasting for Floating-Point Problems ( abstract )
11:30
The next 10^4 UppSAT Approximations ( abstract )
12:00
Alt-Ergo 2.2 ( abstract )
12:00-12:40 Session 43A (LICS)
Chair:
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 44A: 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 44B: 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 44C: FSCD General Meeting (FSCD)

AGENDA of FSCD18 General Meeting (Thursday July 12th from 17:00 to 18:00)

  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.
14:00-15:40 Session 44E (LICS)
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 44F (LICS)
Chair:
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 44G: 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 44H (SMT)
14:00
Invited talk: Towards Scalable Verification of Neural Networks ( abstract )
15:00
Puli - A Problem-Specific OMT Solver ( abstract )
15:00-15:30 Session 45B (ITP)
15:00
ProofWatch: Watchlist Guidance for Large Theories in E ( abstract )
15:30-16:00Coffee Break
16:00-17:00 Session 46B (ITP)
16:00
Verified Tail Bounds for Randomized Programs ( abstract )
16:30
Verified Analysis of Random Binary Tree Structures ( abstract )
16:00-17:30 Session 46E (SMT)
16:00
SMT-based Compile-time Verification of Safety Properties for Smart Contracts ( abstract )
16:30
Selfless Interpolation for Infinite-State Model Checking ( abstract )
17:00
Discovering Universally Quantified Solutions for Constrained Horn Clauses ( abstract )
16:10-17:25 Session 47A: 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 47B: 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 48: 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 49B: Alonzo Church Award Session (LICS)
17:00
The 2018 Alonzo Church Award for Outstanding Contributions to Logic and Computation ( abstract )
17:15
Constraints, Graphs, Algebra, Logic, and Complexity ( abstract )
17:30-18:00 Session 50: Rewriting (FSCD)
17:30
Coherence of Gray categories via rewriting ( abstract )
Friday, July 13th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 51A: invited talk - Abraham, Erika (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 51B: 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 51C: CAV Tutorial: Shaz Qadeer (part 1) (CAV)
09:00
Proving a concurrent program correct by demonstrating it does nothing ( abstract )
09:00-10:30 Session 51E (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 51F (LSB)
09:00
Pathway Logic: Symbolic executable models for reasoning about cellular processes ( abstract )
09:00-10:30 Session 51G (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 51H: 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 51I: 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 51J (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 51K: Machine learning and logic (SoMLMFM)
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 51L (Tetrapod)
09:00
Modularity in Software Synthesis ( abstract )
09:45
Modularity in Mathematical Computation ( abstract )
09:00-10:30 Session 51M: 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 51N (VDMW)
09:00
Model checking and its applications ( abstract )
09:45
TBA ( abstract )
09:00-10:30 Session 51P: Vampire - Past, Present and Future (Vampire)
09:00
Vampire: where have we come from, where are we going ( abstract )
09:00-10:30 Session 51Q (rv4rise)
09:00
Hardware-based runtime verification with Tessla ( abstract )
09:45
Real-time Stream Processing with RTLola ( abstract )
09:30-10:30 Session 52A: Isabelle 1 (Isabelle)
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 53: 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 54A: 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 54B: CAV Tutorial: Shaz Qadeer (part 2) (CAV)
11:00
Proving a concurrent program correct by demonstrating it does nothing (continued) ( abstract )
11:00-12:30 Session 54C (FRIDA)
11:00
Stateless model-checking under the data-centric view ( abstract )
11:30
From Asynchronous Message-Passing Models To Rounds ( abstract )
11:00-12:30 Session 54D (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 54E: Isabelle 2 (Isabelle)
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 54F: LCC: Contributed Talks (LCC)
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 54G (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 54H (LearnAut)
11:00
TBA ( abstract )
12:00
Learning Tree Distributions by Hidden Markov Models ( abstract )
11:00-12:30 Session 54I: 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 54J: 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 54K (SMT)
11:00
Centralizing Equality Reasoning in MCSAT ( abstract )
11:30
Proofs in conflict-driven theory combination ( abstract )
12:00
SMT Solving Modulo Tableau and Rewriting Theories ( abstract )
11:00-12:30 Session 54L: Ethical and fair AI (SoMLMFM)
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 54M (Tetrapod)
11:00
Modularity in Ontologies ( abstract )
11:45
Discussion 1 ( abstract )
11:00-12:30 Session 54N: 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 54P (VDMW)
11:00
Verification of infinite-state systems using decidable logic ( abstract )
11:45
TBA ( abstract )
11:00-12:30 Session 54R (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 55A: 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 55B: 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 55C: CAV Tutorial: Matteo Maffei (CAV)
14:00
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts ( abstract )
14:00-15:30 Session 55D (FRIDA)
14:00
TBA ( abstract )
14:30
Making Parallel Snapshot Isolation Serializable ( abstract )
15:00
TBA ( abstract )
14:00-15:30 Session 55E (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 55F: LCC: Martin Hofmann Memorial Session (LCC)
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 55G (LSB)
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 55H (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 55I: 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 55J: 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 55K (SMT)
14:00
Rewrites for SMT Solvers using Syntax-Guided Enumeration ( 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 55L: Applications of AI (SoMLMFM)
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 55M (Tetrapod)
14:00
Modularity in Proof Checking ( abstract )
14:45
Modularity in Large Proofs ( abstract )
14:00-15:30 Session 55P (VDMW)
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 55R (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-18:00 Session 56B: Isabelle 4 (Isabelle)
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 56C: LCC: Martin Hofmann Memorial Session (LCC)
16:00
My Journey through Observational Equivalence Research with Martin Hofmann ( abstract )
16:30
Memories of Martin ( abstract )
16:00-18:00 Session 56D (LSB)
16:00
A logic modelling workflow for systems pharmacology ( abstract )
16:00-18:00 Session 56E (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 56F: 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 56H: Explainable machine learning (SoMLMFM)
16:00
Influence-directed explanations for machine learning systems ( abstract )
16:20
Explaining the Effectiveness of Random Testing ( abstract )
16:00-18:00 Session 56I (Tetrapod)
16:00
Modularity in Proof Assistants ( abstract )
16:45
Discussion 2 ( abstract )
16:00-18:00 Session 56L (rv4rise)
16:00
Quantitative Regular Expression for Arrhythmia Detection ( abstract )
16:10-18:00 Session 57: Small Models and SL-COMP (ADSL)
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 58: Talks in memoriam Mike Gordon (CAV)
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 )
19:00-21:30 Session : 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).

Saturday, July 14th

View this program: with abstractssession overviewtalk overview

10:00-10:30 Session 62A: Program verification (F-IDE)
10:00
Lightweight Interactive Proving inside an Automatic Program Verifier ( abstract )
10:00-10:30 Session 62B: Overture: Tools (Overture)
Chair:
10:00
Welcome to the Overture Workshop ( abstract )
10:10
Enhancing Testing of VDM-SL models ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 63A: Model Checking (CAV)
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 63B: 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 63C: 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>.

11:00-12:30 Session 63D: 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 63E: SMT 1 (IJCAR)
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 63F: 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: VDM-RT as FMU Controller ( 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 64A: CAV Invited Talk: Eran Yahav (CAV)
14:00
From Programs to interpretable Deep Models, and Back ( abstract )
14:00-15:30 Session 64C: 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 64D: SAT Extensions & Applications (IJCAR)
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 65: 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 66A: Polyhedra (CAV)
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 67A: Synthesis (CAV)
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-18:00 Session 67B: 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 67C: Formal Methods in Industry (FLoC)
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 67E: Rewriting & Termination (IJCAR)
16:00
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems ( abstract )
16:30
Well-Founded Unions ( abstract )
16:00-18:00 Session 67F: 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 68A: 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 )
19:00-21:30 Session : 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 69B (FM)
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 69C: ICLP Invited Talk: Elvira Albert (ICLP)
09:00
Eliminating redundancies in the exploration of concurrent programs ( abstract )
09:00-10:30 Session 69D: Logics and Calculi (IJCAR)
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 69E: SAT (IJCAR)
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 70A: Learning (CAV)
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 71A: Runtime Verification, Hybrid and Timed Systems (CAV)
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 71B: FM Invited Talk: Annabelle McIver (FM)
11:00
Privacy in Text Processing: An information flow perspective ( abstract )
11:00-12:30 Session 71C: 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 71D: Formal Proofs (IJCAR)
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 71E: SMT 2 (IJCAR)
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 73A: Tools (CAV)
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 73C: 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 73D: IJCAR Invited Talk: Martin Giese (IJCAR)
14:00
Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem? ( abstract )
15:00-15:30 Session 74B: Automated Reasoning and Data (IJCAR)
15:00
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics ( abstract )
15:15
Efficient Model Construction for Horn Logic with VLog: System Description ( abstract )
15:30-16:00Coffee Break
16:00-17:00 Session 75A: Probabilistic Systems (CAV)
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 75B (FM)
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 75C: 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 75D: Logics, Frameworks and Proofs (IJCAR)
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 75E: Verification (IJCAR)
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 76A: Tools (CAV)
09:00
Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs ( abstract )
09:15
MaxSMT-Based Type Inference for Python 3 ( abstract )
09:30
The JKind Model Checker ( abstract )
09:45
The DEEPSEC prover ( abstract )
10:00
SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability ( abstract )
10:15
StringFuzz: A Fuzzer for String Solvers ( abstract )
09:00-10:00 Session 76B: FM Invited Talk: Leonardo de Moura (FM)
09:00
Efficient verification and metaprogramming in Lean ( abstract )
09:00-10:30 Session 76C: 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 76D: Decidability & Complexity (IJCAR)
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 77 (FM)
10:00
Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 78B (FM)
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 78C (FM)
11:00
Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE ( abstract )
11:30
Resource-aware Design for Reliable Autonomous Applications with Multiple Periods ( abstract )
12:00
Verifying Auto-Generated C Code from Simulink ( abstract )
11:00-11:30 Session 78D: Implementation of ASP Systems (ICLP)
11:00
Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming ( abstract )
11:00-12:30 Session 78E: Superposition (IJCAR)
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 80: Static Analysis (CAV)
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 81: FLoC Plenary Lecture: Byron Cook (FLoC)
14:00
Formal Reasoning about the Security of Amazon Web Services ( abstract )
15:30-16:00Coffee Break
16:00-18:00 Session 82B (FM)
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 82C (FM)
16:00
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations ( abstract )
16:30
Multi-Robot LTL Planning Under Uncertainty ( abstract )
17:00
Vector Barrier Certificates and Comparison Systems ( abstract )
17:30
Timed Vacuity ( abstract )
19:00-21:30 Session : 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 84A: Theory and Security (CAV)
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 84B (FM)
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 84C: FM I-Day (FM)
09:00
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems ( abstract )
09:30
Interlocking Design Automation using Prover Trident ( abstract )
10:00
Model-Based Testing for Avionics Systems ( abstract )
09:00-10:00 Session 84E: IJCAR Invited Talk: Erika Abraham (IJCAR)
09:00
Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics ( abstract )
10:00-10:30 Session 85: SMT 3 (IJCAR)
10:00
A Separation Logic with Data: Small Models and Automation ( abstract )
10:30-11:00Coffee Break
11:00-12:15 Session 86A: SAT, SMT and Decision Procedures (CAV)
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 86C: 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 (Application paper) ( abstract )
12:00
Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP ( abstract )
11:00-12:30 Session 86D: AR Miscellanea (IJCAR)
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 87 (FM)
12:00
View abstraction for systems with component identities ( abstract )
12:30-14:00Lunch Break
14:00-15:15 Session 88A: Concurrency (CAV)
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 88B (FM)
14:00
Compositional Reasoning for Shared-variable Concurrent Programs ( abstract )
14:30
Statistical Model Checking of LLVM Code ( abstract )
15:00
SDN-Actors: Modeling and Verification of SDN Programs ( abstract )
14:00-15:30 Session 88C: FM I-Day (FM)
14:00
Software Safety and Security and AI ( abstract )
14:30
Variant Analysis with QL ( abstract )
15:00
Object-Oriented Security Proofs ( abstract )
14:00-15:30 Session 88D: 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 88E: System Descriptions (IJCAR)
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 89A: CPS, Hardware, Industrial Applications (CAV)
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 89B (FM)
16:00
CompoSAT: Specification-Guided Coverage for Model Finding ( abstract )
16:30
Approximate Partial Order Reduction ( abstract )
17:00
A lightweight deadlock analysis technique of object-oriented programs ( abstract )
17:30
Formal Specification and Verification of Dynamic Parametrized Architectures ( abstract )
16:00-17:30 Session 89C: FM I-Day (FM)
16:00
Z3 and SMT in Industrial R&D ( abstract )
16:30
Evidential and Continuous Integration of Software Verification Tools ( abstract )
17:00
Disruptive Innovations for the Development and the Deployment of Fault-Free Software ( abstract )
16:00-16:30 Session 89D: 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.

16:30-18:00 Session 90: 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 91A: ARQNL Invited Talk: Larry Moss (ARQNL)
09:00
Automated Reasoning In Natural Language: Current Directions ( abstract )
09:00-10:30 Session 91B (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 91D (ICLP)
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 91F: 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 91I: Parallel algorithms I (PLR)

The first session on parallel algorithms

09:00
Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications ( abstract )
09:45
An Efficient Zielonka's Algorithm for Parallel Parity Games ( abstract )
09:00-10:30 Session 91J (REFINE)
09:00
Automated verification of linearizability ( abstract )
10:00
Correctness of Concurrent Objects under Weak Memory Models ( abstract )
09:00-10:30 Session 91L (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 91M (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 91N (VSTTE)

Model Checking I

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

Invited Speaker

Contributed Talks: Distributed Systems I

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 91Q (WST)
09:00
Termination Checking and Invariant Synthesis for Affine Programs ( abstract )
10:00-10:30 Session 92: 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 93A: 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 93B (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 93C: 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 93D (ICLP)
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 Acquisition and Question Answering via Controlled Natural Language ( abstract )
11:00-12:30 Session 93F: 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 93I: Verifying parallel programs (PLR)

Techniques to verify parallel programs.

 

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 93J (REFINE)
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 in time models ( abstract )
11:00-12:30 Session 93L (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 93M (ThEdu)
11:00
Lucas Interpretation from Programmers’ Perspective ( abstract )
11:30
GeoCoq: formalized foundations of geometry ( abstract )
11:00-12:30 Session 93N (VSTTE)

Model Checking II

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 93P: Distributed Systems II (VaVAS)

Contributed Talks: Distributed Systems II

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 )
12:30-14:00Lunch Break
14:00-15:30 Session 94B (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 94D (ICLP)
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 94F: Declarative Dynamic Programming (LaSh)
14:00
Declarative Dynamic Programming with Inverse Coupled Rewrite Systems ( abstract )
14:00-15:30 Session 94I: Parallel programming tutorial (PLR)

This session will include a tutorial on (advanced) aspects of parallel programming. The speaker is yet to be confirmed. More information will soon follow.

14:00-15:30 Session 94L (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 94M (ThEdu)

ThEdu Business Meeting

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 94N (VSTTE)

Certification & Formalisation I

14:00
Verified Certificate Checking for Counting Votes ( abstract )
14:00-15:30 Session 94P: Invited Speaker; Autonomous Vehicles I (VaVAS)

Invited Speaker

Contributed Talks: Autonomous Vehicles I

14:00
TBA ( abstract )
15:00
Towards validation and verification of an autonomous railway inspection and repair system ( abstract )
15:30-16:00Coffee Break
16:00-17:30 Session 96A: 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 96B: 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 96C (ICLP)
16:00
Model Revision of Logical Regulatory Networks using Logic-based Tools ( abstract )
16:00-18:00 Session 96E: LaSh Session IV (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
A Logic of Information Flows ( abstract )
17:15
Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth ( abstract )
17:40
Decidable Linear Tree Constraints ( abstract )
16:00-18:00 Session 96H: Parallel algorithms II (PLR)

The second session on parallel algorithms.

 

16:00
MASP-Reduce: a proposal for distributed computation of stable models ( abstract )
16:45
Using work-stealing to parallelize symbolic algorithms and parity game solvers ( abstract )
16:00-18:00 Session 96I (REFINE)
16:00
Refining Santa: An Excercise in Efficient Synchronization ( abstract )
16:30
a Theory of Lazy Imperative Timing ( abstract )
16:00-18:00 Session 96K (TLA)
16:00
Invariants in Distributed Algorithms ( abstract )
16:45
Proving properties of a minimal covering algorithm ( abstract )
16:00-18:00 Session 96M (VSTTE)

Certification & Formalisation II

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 96N: Autonomous Vehicles II (VaVAS)

Contributed Talks: Autonomous Vehicles II

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

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

Thursday, July 19th

View this program: with abstractssession overviewtalk overview

09:00-10:30 Session 97B (EICNCL)
09:00
Invited talk ( abstract )
10:00
Effective Translations between Display and Labelled Proofs for Tense Logics ( abstract )
09:00-10:30 Session 97F: 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 97I (VSTTE)

Certification & Formalisation III

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

Invited Speaker

Contributed Talks: Robotics I

09:00
Reproducibility in Robotics - The Big 5 Issues ( abstract )
10:00
RoboTool: Modelling and Verification with RoboChart ( abstract )
09:00-10:30 Session 97K (WST)
09:00
Towards a Unified Method for Termination ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 98A: 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 98B: 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 98F: 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 98I (VSTTE)

Security

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 98J: Robotics II (VaVAS)

Contributed Talks: Robotics II

11:00
Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot ( abstract )
12:30-14:00Lunch Break
14:00-15:30 Session 100B (EICNCL)
14:00
Invited talk ( abstract )
15:00
Proof Translations in BI logic ( abstract )
14:00-15:30 Session 100F: Invited talk II & a short paper (PRUV)
14:00
TBA (invited talk) ( abstract )
15:10
Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure ( abstract )
14:00-15:30 Session 100I (VSTTE)

New Applications

14:00
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms ( abstract )
14:30
Practical Methods for Reasoning about Java 8's Functional Programming Features ( abstract )
15:00
Verification of Binarized Neural Networks via Inter-Neuron Factoring ( abstract )
15:30-16:00Coffee Break
16:00-18:00 Session 101A: 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 )
17:00
Patterns for Modeling Task-level Timing Constraints with Event-B ( abstract )
16:00-17:30 Session 101B: 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 101F: PRUV regular papers (PRUV)
16:00
A New Probabilistic Algorithm for Approximate Model Counting ( abstract )
16:30
Leveraging Probabilistic Existential Rules for Adversarial Deduplication ( abstract )
17:00
VolCE: An Efficient Tool for Solving #SMT(LA) Problems ( abstract )
16:00-18:00 Session 101I (VSTTE)

Off the beaten track

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 )