Program for Friday, July 13th: Talk View

PROGRAM FOR FRIDAY, JULY 13TH: TALK VIEW

Days:

previous day

next day

all days

View: with abstracts session overview

9:00

9:30

10:00

10:30

11:00

11:30

12:00

12:30

13:00

13:30

14:00

14:30

15:00

15:30

16:00

16:30

17:00

17:30

18:00

18:30

19:00

19:30

20:00

20:30

21:00

21:30

09:00-10:00

Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid

Erika Abraham

09:00-09:50

Resource semantics: substructural logic as a modelling technology (keynote)

David Pym

09:50-10:20

Automating the Flow Framework

Siddharth Krishna, Dennis Shasha, Thomas Wies

09:00-10:30

Proving a concurrent program correct by demonstrating it does nothing

Shaz Qadeer, Bernhard Kragl

09:00-09:30

Building verified distributed systems with IVy

Kenneth McMillan

09:30-10:00

The latest gossip on BFT consensus

Ethan Buchman

10:00-10:30

Formal Verification of Internet of Things Protocols

Giorgio Delzanno

09:00-10:00

Horn Clauses and Beyond for Relational and Temporal Program Verification

Hiroshi Unno

10:00-10:30

Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs

E. De Angelis, F. Fioravanti, A. Palacios, A. Pettorossi, M. Proietti

09:00-09:45

Pathway Logic: Symbolic executable models for reasoning about cellular processes

Carolyn Talcott

09:00-10:00

Algorithms for Weighted and Probabilistic Context-Free Grammars and Convex Optimization

Kousha Etessami

10:00-10:30

Learning Graph Weighted Models on Pictures

Philip Amortila, Guillaume Rabusseau

09:00-10:00

Conditioning and quantiles in Markovian models

Christel Baier

10:00-10:30

Multiple Objectives and Cost Bounds in MDP

Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann

09:00-09:22

Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted

Mancini, Mari, Massini, Melatti, Salvo, Sinisi, Tronci, Ehrig, Röblitz, Leeners

09:22-09:44

Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network

Mancini, Tronci, Scialanca, Lanciotti, Finzi, Guarneri, Di Pompeo

09:44-10:06

Greedy Randomized Search for Scalable Compilation of Quantum Circuits

Angelo Oddi, Riccardo Rasconi

10:06-10:28

Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application

Marco Gavanelli, Maddalena Nonato, Andrea Peano, Davide Bertozzi

09:00-10: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

Christoph Benzmüller

10:00-10:30

Higher-Order SMT Solving

H. Barbosa, A. Reynolds, P. Fontaine, D. El Ouraoui, C. Tinelli

09:00-09:30

Machine learning and logic: Fast and slow thinking

Moshe Vardi

09:30-10:00

Provably beneficial artificial intelligence

Stuart Russell

10:00-10:30

Towards Robust and Explainable Artificial Intelligence

Pushmeet Kohli

09:00-09:45

Modularity in Software Synthesis

Douglas Smith

09:45-10:30

Modularity in Mathematical Computation

Nicolas Thiery

09:00-10:00

Designing Globular: formal proofs as geometrical objects (Invited Talk)

Jamie Vicary

10:00-10:30

Interfacing with a Prover using Focusing and Logic Programming

Tomer Libal

09:00-09:45

Model checking and its applications

Orna Grumberg

09:45-10:30

Computation and inference

Natarajan Shankar

09:00-10:30

Vampire: where have we come from, where are we going

Giles Reger

09:00-09:45

Hardware-based runtime verification with Tessla

Martin Leucker

09:45-10:30

Real-time Stream Processing with RTLola

Hazem Torfah

09:30-10:00

A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

10:00-10:30

Lazy Algebraic Types in Isabelle/HOL

Andreas Lochbihler, Pascal Stoop

09:30-10:30

On polynomial time for infinite structures

Mikolaj Bojanczyk

10:50-11:15

Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain

Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

11:15-11:40

Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations

Haesaert, Nilsson, Vasile, Rohan, Agha-Mohammadi, Ames, Murray

11:40-12:05

Concentration of Measure for Chance-Constrained Optimization

Sadegh Soudjani, Rupak Majumdar

11:00-11:30

Cyclic Theorem Prover for Separation Logic by Magic Wand

Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura

11:30-12:00

Labelled Cyclic Proofs for Separation Logic

Didier Galmiche, Daniel Mery

12:00-12:30

A Complete Proof System for Basic Symbolic Heaps with Permissions

Stéphane Demri, Etienne Lozes, Denis Lugiez

11:00-12:30

Proving a concurrent program correct by demonstrating it does nothing (continued)

Shaz Qadeer

11:00-11:30

Specifying Non-Atomic Methods of Concurrent Objects

Michael Emmi

11:30-12:00

Peregrine - A Tool for Population Protocols

Stefan Jaax

12:00-12:30

From Asynchronous Message-Passing Models To Rounds

Adam Shimi

11:00-11:30

Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions

Qi Zhou, David Heath, William Harris

11:30-12:00

A simple functional presentation and an inductive correctness proof of the Horn algorithm

António Ravara

12:00-12:30

Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract

Ekaterina Komendantskaya, Yue Li

11:00-11:30

Formal Verification of Bounds for the LLL Basis Reduction Algorithm

Max W. Haslbeck, René Thiemann

11:30-12:00

Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle

Stock et.al

12:00-12:30

Further Scaling of Isabelle Technology

Makarius Wenzel

11:00-11:15

Traversal-invariant definability and Logarithmic-space computation

Steven Lindell, Scott Weinstein

11:15-11:30

A recursion-theoretic characterisation of the positive polynomial-time functions

Anupam Das, Isabel Oitavem

11:30-11:45

Feasibly constructive proofs of succinct weak circuit lower bounds

Moritz Müller, Ján Pich

11:45-12:00

Computability over locally finite structures from algebra

Siddharth Bhaskar

12:00-12:15

A General Equational Framework for Static Profiling of Parametric Resource Usage

Pedro Lopez-Garcia, Maximiliano Klemen, Umer Liqat, Manuel V. Hermenegildo

12:15-12:30

Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties

Edwin Pin

11:00-11:45

Counterfactual resimulation for causal analysis of rule-based models

Jonathan Laurent

11:45-12:30

Bio-curation and rule-based modelling of protein interaction networks in KAMI

Sébastien Légaré

11:00-12:00

TBA

Doina Precup

12:00-12:30

Learning Tree Distributions by Hidden Markov Models

Davide Bacciu, Daniele Castellana

11:00-11:30

Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives

Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin

11:30-12:00

Parameterized complexity of games with monotonically ordered omega-regular objectives

Véronique Bruyère, Quentin Hautem, Jean-Francois Raskin

12:00-12:30

Comfort and Energy Optimization for Floor Heating Systems

Adrien Le Coent, Kim Guldstrand Larsen, Marco Muniz, Jiri Srba

11:00-11:22

Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic

Paul Tarau

11:22-11:44

Externally Supported Models for Efficient Computation of Paracoherent Answer Sets

Giovanni Amendola, Carmine Dodaro, Wolfgang Faber, Francesco Ricca

11:44-12:06

Algebraic Crossover Operators for Permutations

Marco Baioletti, Alfredo Milani, Valentino Santucci

12:06-12:28

An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock

Slimane Abou-Msabah, Ahmed Riadh Baba Ali, Basma Sagr

11:00-11:30

Centralizing Equality Reasoning in MCSAT

François Bobot, Stephane Graham-Lengrand, Bruno Marre, Guillaume Bury

11:30-12:00

Proofs in conflict-driven theory combination

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

12:00-12:30

Selfless Interpolation for Infinite-State Model Checking

Tanja Schindler, Dejan Jovanović

11:00-11:20

Ethically Aligned AI Systems

Francesca Rossi

11:20-11:40

Program Fairness – a Formal Methods Perspective

Aditya Nori

11:40-12:00

Deep Learning Methods for Large Scale Theorem Proving

Christian Szegedy

12:00-12:30

AI2: AI Safety and Robustness with Abstract Interpretation

Martin Vechev

11:00-11:45

Modularity in Ontologies

Till Mossakowski

11:45-12:30

Discussion 1

Dennis Müller

11:00-11:30

Partial Regularization of First-Order Resolution Proofs

Jan Gorzny, Ezequiel Postan, Bruno Woltzenlogel Paleo

11:30-12:00

Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons

Sarah Grebing, An Thuy Tien Luong, Alexander Weigl

12:00-12:30

Automated Theorem Proving in a Chat Environment

Rustam Zhumagambetov, Mark Sterling

11:00-11:45

Verification of infinite-state systems using decidable logic

Sharon Shoham

11:45-12:30

Should I join a startup?

Cristina David

11:00-12:00

TBA

Cesare Tinelli

11:00-11:45

Systematic analysis and improvement of CNNs.

Tommaso Dreossi

11:45-12:30

Formalizing Requirements for Cyber-Physical Systems: Real-World Experiences and Challenges

Jim Kapinski

12:30-14:00 FLOC Steering Committee Lunchtime Meeting

14:00-14:25

Algorithm for Bernstein Polynomial Control Design

Tareq Hamadneh, Rafal Wisniewski

14:25-14:50

Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle

Ariadna Estrada, Ian M. Mitchell

14:50-15:15

An Interval-Based Sliding Horizon Motion Planning Method

Julien Alexandre Dit Sandretto, Elliot Brendel, Alexandre Chapoutot

14:00-14:50

Weak memory made easy by separation logic (keynote)

Viktor Vafeiadis

14:50-15:20

On the Complexity of Pointer Arithmetic in Separation Logic

James Brotherston, Max Kanovich

15:20-15:50

The Complexity of Prenex Separation Logic with One Selector

Mnacho Echenim, Radu Iosif, Nicolas Peltier

14:00-15:30

Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts

Matteo Maffei, Clara Schneidewind

14:00-14:30

Specifying and Verifying Concurrent Objects

Constantin Enea

14:30-15:00

Making Parallel Snapshot Isolation Serializable

Andrea Cerone

15:00-15:30

Parameterized Reachability for All Flavors of Threshold Automata

Jure Kukovec

14:00-15:00

Tree dimension in verification of constrained Horn clauses

Pierre Ganty

15:00-15:30

Declarative Parameterized Verification of Topology-sensitive Distributed Protocols

Giorgio Delzanno, Sylvain Conchon, Angelo Ferrando

14:00-15:00

Characterizing Complexity Classes in Presence of Higher-Order Functions — How Martin Hofmann Contributed to Shaping

Ugo Dal Lago

15:00-15:30

Static Prediction of Heap Space Usage for First-Order Functional Programs -- A Retrospective on my First Paper with Martin

Steffen Jost

14:00-14:45

A logical framework for systems biology and biomedicine

Joëlle Despeyroux

14:45-15:30

Introducing iota, a logic for biological modelling

Adrien Husson

14:00-15:00

Weak and Strong learning of Probabilistic Context-Free Grammars: theoretical and empirical

Alexander Clark

15:00-15:30

Decision problems for Clark-congruential languages

Makoto Kanazawa, Tobias Kappé

14:00-15:00

A journey through negatively-weighted timed games: undecidability, decidability, approximability

Benjamin Monmege

15:00-15:30

Stochastic o-minimal hybrid systems

Thomas Brihaye, Mickael Randour, Cédric Rivière

14:00-14:22

Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns

Richard Wallace

14:22-14:44

Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems

Richard Wallace

14:44-15:06

Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited

Neng-Fa Zhou, Håkan Kjellerstrand

15:06-15:28

On the Configuration of SAT Formulae

Mauro Vallati

14:00-14:30

Discovering Universally Quantified Solutions for Constrained Horn Clauses

Arie Gurfinkel, Sharon Shoham, Yakir Vizel

14:30-15:00

What is the Point of an SMT-LIB Problem?

Giles Reger, Martin Riener

15:00-15:30

SMT-COMP 2018 Report

Smt-Comp Organizers

14:00-14:30

The realities of applied AI

Alison Lowndes

14:30-15:00

Safe reinforcement learning via formal methods

André Platzer

15:00-15:30

Programming from examples: PL meets ML

Sumit Gulwani

14:00-14:45

Modularity in Proof Checking

Catherine Dubois

14:45-15:30

Modularity in Large Proofs

Georges Gonthier

14:00-14:30

Isabelle/PIDE after 10 years of development

Makarius Wenzel

14:30-15:00

Text-Orientated Formal Mathematics

Steffen Frerix, Peter Koepke

15:00-15:30

Drawing Trees

Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen

14:00-14:30

Isabelle/PIDE after 10 years of development

Makarius Wenzel

14:30-15:00

Text-Orientated Formal Mathematics

Steffen Frerix, Peter Koepke

15:00-15:30

Drawing Trees

Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen

14:00-14:30

How to get a paper accepted?

Lawrence C. Paulson

14:30-15:00

How to attend a conference?

Tom Melham

15:00-15:30

Hands-on: Elevator pitch

Jasmin Christian Blanchette

14:00-14:30

Towards Word Sense Disambiguation by Reasoning

Javier Álvez, Itziar Gonzalez-Dios, German Rigau

14:30-15:00

Testing ATP folklore: a statistical analysis of Vampire proofs.

Michael Rawson, Giles Reger

15:00-15:30

Foundations of SPECTRE

Bernhard Gleiss, Simon Robillard, Laura Kovacs

14:00-14:45

Signal classification using temporal logic

Calin Belta

14:45-15:30

First order temporal properties of continuous signals

Thomas Ferrère

16:00-16:30

Stateless model-checking under the data-centric view

Andreas Pavlogiannis

16:30-17:00

Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction

Ilina Stoilkovska

16:00-17:00

Report on the CHC competition

Arie Gurfinkel

16:00-16:15

Substitutionless First-Order Logic: A Formal Soundness Proof

A.H. From, J.B. Larsen, A. Schlichtkrull, J. Villadsen

16:15-16:30

The remote_build Tool

Christian Sternagel

16:30-17:00

PaMpeR: A Proof Method Recommendation System for Isabelle/HOL

Yutaka Nagashima, Yilun He

17:00-17:30

Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study

Joshua Bockenek, Peter Lammich, Yakoub Nemouchi, Burkhart Wolff

16:00-16:30

My Journey through Observational Equivalence Research with Martin Hofmann

Vivek Nigam

16:30-17:00

Memories of Martin

Don Sannella

16:00-16:45

A logic modelling workflow for systems pharmacology

Luis Tobalina Segura

16:00-16:30

The Learnability of Symbolic Automata

George Argyros

16:30-17:00

Automatic clustering of a network protocol with weakly-supervised clustering

Tobias Schrank, Franz Pernkopf

17:00-17:30

Toward Learning Boolean Functions from Positive Examples

Nicolas Basset, Oded Maler, Irini-Eleftheria Mens

17:30-18:00

Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches

Alexis Linard

16:00-16:30

Multi-Scenario Uncertainty in Markov Decision Processes

Dimitri Scheftelowitsch

16:30-17:00

Safe and Optimal Scheduling of Hard and Soft Tasks

Gilles Geeraerts, Shibashis Guha, Jean-Francois Raskin

17:00-17:30

Logically-Constrained Reinforcement Learning

Mohammadhosein Hasanbeig, Alessandro Abate, Daniel Kroening

16:00-17:30 SMT-LIB Updates and Discussion

16:00-16:20

Influence-directed explanations for machine learning systems

Anupam Datta

16:20-16:40

Safety verification for deep neural networks with provable guarantees

Marta Kwiatkowska

16:00-16:45

Modularity in Proof Assistants

Natarajan Shankar

16:45-17:30

Discussion 2

Dennis Müller

16:00-17:00

Learning from failure

Byron Cook

16:00-16:30

Experimenting with Theory Instantiation in Vampire

Giles Reger, Martin Riener

16:30-17:00

Giving AVATAR Quantifiers to Play With

Giles Reger, Andrew Reynolds, Martin Suda

17:00-17:30

Developments in Higher-order Theorem proving within Vampire

Ahmed Bhayat, Giles Reger

16:00-16:45

Using the F1/10 Autonomous Racing Platform for Runtime Verification Research

Houssam Abbas

16:10-16:40

Sloth: Separation Logic and Theories via Small Models

Jens Katelaan, Dejan Jovanović, Georg Weissenbacher

16:40-18:00

Presentation of Results from SL-COMP 2018

Mihaela Sighireanu

16:30-17:00

Proof Scripting from HOL to Goaled

Tom Melham

17:00-17:30

HOL Developed and HOL Used: Interconnected Stories of Real-World Applications

Michael Norrish

17:30-18:00

From Processor Verification Upwards

Magnus Myreen

16:40-17:00

What Just Happened in AI

Adnan Darwiche

17:00-18:00

Panel session

Adnan Darwiche, Stuart Russell, Vasu Singh, Chris Holmes

17:30-18:00 SMT Business meeting

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

15:30-16:00 Coffee Break

19:00-21:30 Workshops dinner at Keble College