Program for Wednesday, July 18th: Talk View

PROGRAM FOR WEDNESDAY, JULY 18TH: 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

Automated Reasoning In Natural Language: Current Directions

Larry Moss

09:00-10:00

Invited Talk: Optimization Problems in Answer Set Programming

Mario Alviano

10:00-10:30

anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)

Vladimir Lifschitz, Patrick Lühne, Torsten Schaub

09:00-09:50

Formal Methods at Amazon Web Services

Michael Tautschnig

09:00-09:30

Proof-relevant resolution for elaboration of programming languages

Frantisek Farka

09:30-10:00

Explaining Actual Causation via Reasoning about Actions and Change

Emily Leblanc

10:00-10:30

Probabalistic Action Language pBC+

Yi Wang

09:00-09:10

Opening and introduction

Marc Denecker

09:10-09:50

Invited Talk: Practical uses of Logic, Formal Methods, B and ProB

Michael Leuschel

09:50-10:30

Invited Talk: On the Development of Industrial Applications with ASP

Nicola Leone, Bernardo Cuteri, Marco Manna, Kristian Reale, Francesco Ricca

09:00-10:05

Monadic Second-Order Model Checking with Fly-Automata

Bruno Courcelle, Irène Durand

10:05-10:30

Lazy Automata Techniques for WS1S

Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal, Tomas Vojnar

09:00-09:45

Opening and demos

Viktor Kuncak

09:45-10:30

Bimodal Software Engineering

Earl Barr

09:00-09:45

Needs in formal methods for the validation of naval systems

Laurent Raffaeli

09:45-10:30

Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems

Alberto Ferrari

09:00-09:45

Parallel Algorithms for Parameter Synthesis from Temporal Logic Specifications

David Safranek

09:45-10:30

MASP-Reduce: a proposal for distributed computation of stable models

Federico Igne, Agostino Dovier, Enrico Pontelli

09:00-10:00

Automated verification of linearizability

Ahmed Bouajjani

10:00-10:30

Correctness of Concurrent Objects under Weak Memory Models

Graeme Smith, Kirsten Winter, Robert Colvin

09:00-09:45

Synthesizing safe AI-based controllers for cyber-physical systems

Jyotirmoy Deshmukh

09:45-10:30

Meta-Interpretive Learning of Logic Programs

Stephen H. Muggleton

09:00-10:00

TLA+ in Engineering Systems: Quinceañera

David Langworthy

10:00-10:30

Modeling Virtual Machines and Interrupts in TLA+ & PlusCal

Valentin Schneider

09:00-09:30

Students' Proof Assistant (SPA)

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

09:30-10:00

Natural Deduction Assistant (NaDeA)

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

10:00-10:30

Rating of Geometric Automated Theorem Provers

Nuno Baeta, Pedro Quaresma

09:00-10:00

Contract-based Compositional Verification of Infinite-State Reactive Systems

Cesare Tinelli

10:00-10:30

A Tree-Based Approach to Data Flow Proofs

Jochen Hoenicke, Alexander Nutz, Andreas Podelski

09:00-10:00

Formal Synthesis of Control Strategies for Dynamical Systems

Calin Belta

10:00-10:30

Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract -

Radu Calinescu, Saud Yonbawi

09:00-10:00

Termination Checking and Invariant Synthesis for Affine Programs

James Worrell

10:00-10:30

Evidence Extraction from Parameterised Boolean Equation Systems

Wieger Wesselink, Tim Willemse

11:00-11:30

Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms

Eugenio Orlandelli, Giovanna Corsi

11:30-12:00

An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics

Tomer Libal

12:00-12:30

Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic

Daniel Mery, Didier Galmiche

11:00-11:30

A Survey of Advances in Epistemic Logic Program Solvers

Anthony Leclerc, Patrick Kahl

11:30-12:00

selp: A Single-Shot Epistemic Logic Program Solver

Manuel Bichler, Michael Morak, Stefan Woltran

12:00-12:30

Partial Evaluation of Logic Programs in Vector Spaces

Chiaki Sakama, Hien Nguyen, Taisuke Sato, Katsumi Inoue

11:00-11:30

Detecting Deadlocks in Formal System Models with Condition Synchronization

Eduard Kamburjan

11:30-12:00

Backward reachability analysis for timed automata with data variables

Rebeka Farkas, Tamás Tóth, Ákos Hajdu, András Vörös

12:00-12:30

An Entailment Checker for Separation Logic with Inductive Definitions

Radu Iosif, Cristina Serban

11:00-11:30

The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering

Arindam Mitra

11:30-12:00

Natural Language Generation From Ontologies

Van Nguyen

12:00-12:30

Knowledge Authoring and Question Answering via Controlled Natural Language

Tiantian Gao

11:00-11:10

Introduction: Role-Based Access Control as a Programming Challenge

Y. Annie Liu

11:10-11:20

Security Policies in Constraint Handling Rules

Thom Fruehwirth

11:20-11:30

LPOP2018 XSB Position Paper

David S. Warren

11:30-11:40

Role-Based Access Control via JASP

R. Costabile, A. Fiorentino, N. Leone, M. Manna, K. Reale, F. Ricca

11:40-11:50

The RBAC challenge in the Knowledge Base Paradigm

Marc Denecker

11:50-12:00

Role-Based Access Control via LogicBlox

Tuncay Tekle

12:00-12:10

Logic-based Methods for Software Engineers and Business People

Joost Vennekens

12:10-12:20

Easier Rules and Constraints for Programming

Yanhong A. Liu, Scott Stoller

12:20-12:30

Questions about RBAC challenge solutions

All Workshop Participants

11:00-12:05

Courcelle’s Theorem – A Game-Theoretic Approach

Joachim Kneis, Alexander Langer, Peter Rossmanith

12:05-12:30

A Derivative-Based Decision Procedure for WS1S

Dmitriy Traytel

11:00-11:45

Static Analysis for Developer Efficiency with Infer

Jules Villard

11:45-12:30

Learning to Type

Liam Atkinson

11:00-11:30

Compositional Taylor Model Based Validated Integration

Kristjan Liiva

11:30-12:00

Automatic Generation and Formal Verification of an Interior Point Algorithm

Pierre-Loïc Garoche

12:00-12:30

Towards Enumerative Invariant Synthesis in SMT Solvers

Andrew Raynolds

11:00-11:45

Permission Inference for Array Programs

J. Dohrau, A. Summers, C. Urban, S. Münger, P. Müller

11:45-12:30

RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL

Yatin Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer

11:00-11:30

Challenges of specifying concurrent program components

Ian J. Hayes

11:30-12:00

Programming Without Refinement

Marwa Ben Abdelali, Lamia Labed Jilani, Wided Ghardallou, Ali Mili

12:00-12:30

Ordering strict partial orders to model behavioural refinement

Mathieu Montin, Marc Pantel

11:00-11:18

Reactive Synthesis from LTL Specification with Spot

Thibaud Michaud, Maximilien Colange

11:18-11:36

On the Expressiveness of HyperLTL Synthesis

Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Leander Tentrup

11:36-11:54

Maximum Realizability for Linear Temporal Logic Specifications

Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

11:54-12:12

Warm-Starting Fixed-Point Based Control Synthesis

Zexiang Liu, Necmiye Ozay, Nicolas Perrin

12:12-12:30

Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants

Abate, Bessa, Cattaruzza, Cordeiro, David, Kesseli, Kroening, Polgreen

11:00-11:45

An Animation Module for TLA+

William Schultz

11:45-12:30

BMCMT – Bounded Model Checking of TLA+ Specifications with SMT

Igor Konnov, Jure Kukovec, Thanh Hai Tran

11:00-11:30

Lucas Interpretation from Programmers’ Perspective

Walther Neuper

11:30-12:30

GeoCoq: formalized foundations of geometry

Julien Narboux

11:00-11:30

Executable Counterexamples in Software Model Checking

Arie Gurfinkel, Temesghen Kahsai, Jorge A Navas

11:30-12:00

Extending VIAP to Handle Array Programs

Pritom Rajkhowa, Fangzhen Lin

12:00-12:30

Lattice-Based Refinement in Bounded Model Checking

K. Even-Mendoza, S. Asadi, A. Hyvärinen, H. Chockler, N. Sharygina

11:00-11:30

Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking

Anna Lukina, Ashish Tiwari, Scott Smolka, Radu Grosu

11:30-12:00

Policing Functions for Machine Learning Systems

T.S. Hoang, N. Sato, T. Myojin, M. Butler, Y. Nakagawa, H. Ogawa

12:00-12:30

Social Consequence Engines (Abstract)

Julian Padget, Marina De Vos, Charlie Page

11:00-11:30

Procedure-Modular Termination Analysis

Cristina David, Daniel Kroening, Peter Schrammel

11:30-12:00

GPO: A Path Ordering for Graphs

Nachum Dershowitz, Jean-Pierre Jouannaud

12:00-12:30

Objective and Subjective Specifications

Eric Hehner

14:00-15:00

Going Beyond First-Order Logic with Vampire

Giles Reger

14:00-14:30

Towards Abstraction in ASP with an Application on Reasoning about Agent Policies

Zeynep G. Saribatur, Thomas Eiter

14:30-15:00

Datalog for Static Analysis Involving Logical Formulae

Aaron Bembenek, Stephen Chong

15:00-15:30

Syntactic Conditions for Antichain Property in Consistency Restoring Prolog

Vu Phan

14:00-14:50

Automatic Verification of Concurrent Objects

Michael Emmi

14:00-14:30

Scalable Robotic Intra-Logistics with Answer Set Programming

Philipp Obermeier

14:30-15:00

Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs

Zhun Yang

15:00-15:30

Speeding Up Lazy-Grounding Answer Set Solving

Richard Taupe

14:00-14:30

Panel: Practice of Modeling and Programming

Panelists - All Morning Speakers

14:30-15:10

Invited Talk: A Modeling Language Based on Semantic Typing

John Hooker

15:10-15:20

A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding

Neng-Fa Zhou, Håkan Kjellerstrand

15:20-15:30

Confluence Analysis of Cognitive Models with Constraint Handling Rules

Daniel Gall

14:00-15:00

Declarative Dynamic Programming with Inverse Coupled Rewrite Systems

Robert Giegerich

15:00-15:30

A Logic of Information Flows

Eugenia Ternovska

14:00-14:45

Neural Meta Program Synthesis

Rishabh Singh

14:45-15:30

Learning to Analyze Programs at Scale

Martin Vechev

14:00-14:30

Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation

Paolo Zuliani

14:30-15:00

Parallel reachability analysis of hybrid systems in XSpeed

Rajarshi Ray

15:00-15:30

The Policy Iterations Algorithm is Actually a Newton Method

Assalé Adjé

14:00-14:45

Tuning Parallel SAT Solvers

Thorsten Ehlers, Dirk Nowotka

14:45-15:30

GPU Accelerated SAT solving

Muhammad Osama, Anton Wijs

14:00-15:00

A more relaxed way to make concrete: uses of heuristic search to discover implementations

John Clark, David White

14:00-14:18

Scalable Synthesis with Symbolic Syntax Graphs

Rohin Shah, Sumith Kulal, Rastislav Bodik

14:18-14:36

On Inductive Verification and Synthesis

Dennis Peuter, Viorica Sofronie-Stokkermans

14:36-14:54

Programming by example: efficient, but not “helpful”

Mark Santolucito, Drew Goldman, Allyson Weseley, Ruzica Piskac

14:54-15:12

Minimal Synthesis of String To String Functions From Examples

Jad Hamza, Viktor Kunčak

14:00-14:30

Applying TLA+ in a Safety-Critical Railway Project

Stefan Resch

14:30-15:30

State Space Explosion or: How To Fight An Uphill Battle

Markus Kuppe

14:00-14:30

Towards intuitive reasoning in axiomatic geometry

Maximilian Doré, Krysia Broda

14:30-15:00

Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable

Jørgen Villadsen

14:00-15:00

Verified Software: Theories, Tools, ... and Engineering

Stuart Matthews

15:00-15:30

Verified Certificate Checking for Counting Votes

Milad Ketab Ghale, Dirk Pattinson, Ramana Kumar

14:00-15:00

Trust me I am autonomous

Jérémie Guiochet

15:00-15:30

Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot

Bruno Lacerda, David Parker, Nick Hawes

14:00-14:30

Comparing on Strings: Semantic Kachinuki Order

Alfons Geser, Dieter Hofbauer, Johannes Waldmann

14:30-15:00

Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions

Dieter Hofbauer

15:00-15:30

Well-founded models in proofs of termination

Salvador Lucas

15:00-15:30

Pseudo-Propositional Logic

Ahmad-Saher Azizi-Sultan

16:00-16:30

Formalization of a Paraconsistent Infinite-Valued Logic

Anders Schlichtkrull

16:30-17:00

System Demonstration: The Higher-Order Prover Leo-III

Alexander Steen, Christoph Benzmüller

16:00-16:30

Analyzing Consistency of Formal Requirements

Jan Steffen Becker

16:30-17:00

Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor

Matt Webster, Michael Breza, Clare Dixon, Michael Fisher, Julie McCann

17:00-17:30

Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation

Jessica Petrasch, Jan-Hendrik Oepen, Sebastian Krings, Moritz Gericke

16:00-16:30

Model Revision of Logical Regulatory Networks using Logic-based Tools

Filipe Gouveia, Ines Lynce, Pedro T. Monteiro

16:00-16:40

Invited Talk: The Young Software Engineer’s Guide to Using Formal Methods

Rustan Leino

16:40-16:50

How to upgrade ASP for true dynamic modelling and solving?

Torsten Schaub

16:50-17:00

A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks

Thom Fruehwirth

17:00-17:10

A software system should be declarative except where it interacts with the real world

Peter Van Roy

17:10-17:20

Questions about logic and constraints in real-world applications

All Workshop Participants

17:20-17:50

Panel: Future of Programming with Logic and Knowledge

Panelists - All Afternoon Speakers

17:50-18:00

Closing

Tuncay Tekle, Marc Denecker

16:00-16:25

ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?

Alan Frisch

16:25-16:50

Automated Constraint Modelling with Conjure

Ozgur Akgun

16:50-17:15

Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth

Johannes Fichte

17:15-17:40

Decidable Linear Tree Constraints

Sabine Bauer

16:00-16:45

DeepBugs: A Learning Approach to Name-based Bug Detection

Michael Pradel

16:45-17:15

Measuring software development productivity: a machine learning approach

Ian Wright, Jean Helie, Albert Ziegler

17:15-17:45

Answering Cloze-style Software Questions Using Stack Overflow

Ezra Winston, Bhuwan Dhingra, Kathryn Mazaitis, Graham Neubig, William Cohen

16:00-17:00

Discussion

Alexandre Chapoutot

16:00-16:45

Using work-stealing to parallelize symbolic algorithms and parity game solvers

Tom van Dijk

16:45-17:30

An Efficient Zielonka's Algorithm for Parallel Parity Games

Loredana Sorrentino, Aniello Murano, Rossella Arcucci, Umberto Marotta

16:00-16:30

Refining Santa: An Excercise in Efficient Synchronization

Emil Sekerinski, Shucai Yao

16:30-17:00

a Theory of Lazy Imperative Timing

Eric Hehner

16:00-16:45

Towards correct-by-construction controller synthesis for self-driving cars

Necmiye Ozay

16:45-17:00

Competition Report: SYNTCOMP

Swen Jacobs

17:00-17:15

Competition Report: SyGuS-COMP

Dana Fisman

17:15-18:00

Probabilistic and Interpretable Models of Code

Martin Vechev

16:00-16:45

Invariants in Distributed Algorithms

Yanhong A. Liu, Scott D. Stoller, Saksham Chand, Xuetian Weng

16:45-17:30

Proving properties of a minimal covering algorithm

Ioannis Filippidis, Richard M. Murray

16:00-17:00

ThEdu'18 business meeting

Pedro Quaresma, Walther Neuper

16:00-16:30

Program Verification in the Presence of I/O: Semantics, verified library routines, and verified

H. Férée, J.�. Pohjola, R. Kumar, S. Owens, M.O. Myreen, S. Ho

16:30-17:00

TWAM: A Certifying Abstract Machine for Logic Programs

Brandon Bohrer, Karl Crary

17:00-17:30

A Java bytecode formalisation

Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert

17:30-18:00

Formalising Executable Specifications of Low-Level Systems

Paolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif

16:00-16:30

Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract

Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman

16:30-17:00

Towards a verifiable decision making framework for self-driving vehicles

Mohammed Al-Nuaimi, Hongyang Qu, Sandor Veres

17:00-17:30

Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent

Gleifer Alves, Louise Dennis, Michael Fisher

16:00-18:00 Termination Competition (report and short talks)

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

15:30-16:00 Coffee Break

19:15-21:30 Workshops dinner at Magdalen College