Program for Thursday, July 19th: Talk View

PROGRAM FOR THURSDAY, JULY 19TH: TALK VIEW

Days:

previous 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

09:00-09:50

Experiences with thread-modular static analysis of concurrent embedded systems by abstract

Antoine Miné

09:00-10:00

Title TBA - Invited talk

Dirk Pattinson

10:00-10:30

Effective Translations between Display and Labelled Proofs for Tense Logics

Tim Lyon, Agata Ciabattoni, Revantha Ramanayake, Alwen Tiu

09:00-09:45

Why is Software Natural? and how can Naturalness be exploited?

Prem Devambu

09:45-10:30

Program Synthesis as High-Level Machine Learning

Swarat Chaudhuri

09:00-10:00

The CakeML Verified Compiler and Toolchain

Magnus O. Myreen

10:00-10:30

Dynamic Strategy Priority: Empower the strong and abandon the weak

Michael Rawson, Giles Reger

09:00-09:10

Welcome to PRUV

Anni-Yasmin Turhan

09:10-10:10

Quantitative Logic Reasoning -- Combining logical reasoning with probabilities and counting (invited

Marcelo Finger

09:00-09:15

Welcome and Introduction

Morteza Lahijanian

09:15-09:45

Understanding Ethical Reasoning

Jörg Hardy

09:45-10:15

Human morality, robots’ moral competence, and the deepest kind of trust

Bertram F. Malle

10:15-10:30

Elements of a Model of Trust in Technology

Joachim Iden

09:00-10:00

Controlling Assembly and Function of DNA Nanostructures and Molecular Machinery

Andrew Turberfield

09:00-10:00

Synthesis of Surveillance Strategies for Mobile Sensors

Rayna Dimitrova

10:00-10:30

A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars

Alessandro Coglio

09:00-10:00

Reproducibility in Robotics - The Big 5 Issues

Florian Lier

10:00-10:30

RoboTool: Modelling and Verification with RoboChart

A. Miyazawa, A. Cavalcanti, S. Foster, W. Li, P. Ribeiro, J. Timmis, J. Woodcock

09:00-10:00

Towards a Unified Method for Termination

Akihisa Yamada

10:00-10:20

Computing properties of stable configurations of thermodynamic binding networks

Keenan Breik, Chris Thachuk, Marijn Heule, David Soloveichik

11:00-11:30

Using SMT engine to generate Symbolic Automata

Xudong Qin, Eric Madelaine, Simon Bliutze, Min Zhang

11:30-12:00

Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software

Dross, Foliard, Jouanny, Matias, Matthews, Mota, Moy, Pignard, Soulat

12:00-12:30

A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian

Christophe Limbrée, Charles Pecheur

11:00-11:30

Toward intuitionistic non-normal modal logic and its calculi

Tiziano Dalmonte, Charles Grellois, Nicola Olivetti

11:30-12:00

Proof theory for quantified monotone modal logics

Eugenio Orlandelli, Sara Negri

12:00-12:30

Sequent Calculi for Logic that Includes an Infinite Number of Modalities

Tomoaki Kawano

11:00-11:45

code2vec: Learning Distributed Representations of Code

Eran Yahav

11:45-12:30

Understanding & Generating Source Code with Graph Neural Networks

Miltos Allamanis

11:00-11:30

A Verified Simple Prover for First-Order Logic

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

11:30-12:00

Proof Search Optimizations for Non-clausal Connection Calculi

Jens Otten

12:00-12:30

TFX: The TPTP Extended Typed First-order Form

Geoff Sutcliffe, Evgenii Kotelnikov

11:00-11:30

Measuring Disagreement among Knowledge Bases

Nico Potyka

11:30-12:00

Evidential Group Decision Making Model with Belief-Based Preferences

Aouatef Rouahi, Kais Ben Salah, Khaled Ghedira

12:00-12:30

A new logic for jointly representing hard and soft constraints

Jan Maly, Stefan Woltran

11:00-11:30

How to Free Yourself from the Curse of Bad Equilibria

Michael Wooldridge

11:30-12:00

Specification and Verification for Robots that Learn

Sanjit A. Seshia

12:00-12:15

Moral Permissibility of Actions in Smart Home Systems

Martin Mose Bentzen, Felix Lindner, Louise Dennis, Michael Fisher

11:00-11:20

Rule-Based Gillespie Simulation of Chemical Systems

Jakob Lykke Andersen, Christoph Flamm, Daniel Merkle, Peter F. Stadler

11:20-11:40

Rule-based design of computational DNA devices

Carlo Spaccasassi, Matthew Lakin, Andrew Phillips

11:40-12:00

Noise control for molecular computing

Tomislav Plesa, Radek Erban, Konstantinos Zygalakis, David Anderson

12:00-12:20

Molecular Filters for Noise Reduction

Luca Laurenti, Marta Z Kwiatkowska, Attila Csikász-Nagy, Luca Cardelli

11:00-11:30

Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box

Robin Adams, Sibylle Schupp

11:30-12:00

SideTrail: Verifying Time-Balancing of Cryptosystems

Athanasiou, Cook, Emmi, MacCarthaigh, Schwartz-Narbonne, Tasiran

12:00-12:30

Towards verification of Ethereum smart contracts: a formalization of core of Solidity

Jakub Zakrzewski

11:00-11:30

Robot Demonstration

Bruno Lacerda, David Parker, Nick Hawes

11:00-11:30

Complexity Analysis for Bitvector Programs

Jera Hensel, Florian Frohn, Jürgen Giesl

11:30-12:00

A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

12:00-12:30

Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations

Alicia Merayo, Samir Genaim

11:30-12:30 Panel Session

14:00-15:00

Mostly harmless - luring programmers into proof with SPARK

Yannick Moy

14:00-15:00

Cyclic proofs, hypersequents and Kleene algebra - Invited Talk

Anupam Das

15:00-15:30

Proof Translations in BI logic

Didier Galmiche, Daniel Mery, Michel Marti

14:00-14:45

Neural Network Models of Code Edits

Danny Tarlow

14:45-15:30

Program synthesis and its connections to AGI

Pushmeet Kohli

14:00-14:30

Efficient translation of sequent calculus proofs into natural deduction proofs

Gabriel Ebner, Matthias Schlaipfer

14:30-15:00

Set of Support for Higher-Order Reasoning

Ahmed Bhayat, Giles Reger

15:00-15:30

Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics

Ullrich Hustadt, Cláudia Nalon, Clare Dixon

14:00-15:10

An abstraction-refinement framework for automated reasoning -- a pragmatic approach (invited talk)

Konstantin Korovin

15:10-15:30

Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure

Laura Giordano, Valentina Gliozzi

14:00-14:30

TBA

Rachid Alami

14:30-15:00

The computational neuroscience of human-robot relationships

Aldo Faisal

15:00-15:30

Trust, Failure, and Self-Assessment During Human-Robot Interaction

Aaron Steinfeld

14:00-15:00

Uncovering the Biological Programs that Govern Development

Sara-Jane Dunn

14:00-14:30

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

B. Beckert, T. Bingmann, M. Kiefer, P. Sanders, M. Ulbrich, A. Weigl

14:30-15:00

Practical Methods for Reasoning about Java 8's Functional Programming Features

David Cok, Serdar Tasiran

15:00-15:30

Verification of Binarized Neural Networks via Inter-Neuron Factoring

Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess

14:00-14:30

Control-Flow Refinement via Partial Evaluation

Jesús Doménech, Samir Genaim, John P. Gallagher

14:30-15:00

Verification of Rewriting-based Query Optimizers

Aalok Thakkar, Balaji Krishnamurthy, Piyush Gupta

15:00-15:30

TTT2 with Termination Templates for Teaching

Jonas Schöpf, Christian Sternagel

15:00-15:10

Bayesian Verification of Chemical Reaction Networks

Gareth Molyneux, Viraj Brian Wijesuriya, Alessandro Abate

15:10-15:20

Computational Approaches for the Programmed Assembly of Nanocellulose Meshes

Amarioarei, Spencer, Romica, Barad, Dobre, Itcus, Tusa, Paun, Paun, Czeizler

16:00-16:30

Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks

Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz

16:30-17:00

Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base

Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud, Samuel Hym

16:00-16:30

Intuitionistic multi-agent subatomic natural deduction for belief and knowledge

Bartosz Więckowski

16:30-17:00

Hypersequent calculus for the logic of conditional belief: preliminary results

Marianna Girlando, Bjoern Lellmann, Nicola Olivetti

17:00-17:30

A Forward Calculus for Countermodel Construction in IPL

Camillo Fiorentini, Mauro Ferrari

16:00-16:30

Difflog: Beyond Deductive Methods in Program Analysis

M. Raghothaman, S. Kulkarni, R. Zhang, X. Si, K. Heo, W. Lee, M. Naik

16:30-17:00

Deep Learning On Code with an Unbounded Vocabulary

Milan Cvitkovic, Badal Singh, Anima Anandkumar

17:00-17:30

Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network

V. Markovtsev, W. Long, E. Bulychev, R. Keramitas, K. Slavnov, G. Markowski

17:30-18:00

Open Business Meeting for Future of Machine Learning for Programming

Bruno Marnette

16:00-16:30

A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems

Alireza Ensan, Eugenia Ternovska, Heng Liu

16:30-17:00

A New Probabilistic Algorithm for Approximate Model Counting

Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma

17:00-17:30

Leveraging Probabilistic Existential Rules for Adversarial Deduplication

José Paredes, Maria Vanina Martinez, Gerardo Simari, Marcelo A. Falappa

17:30-17:50

VolCE: An Efficient Tool for Solving #SMT(LA) Problems

Cunjing Ge, Feifei Ma, Jian Zhang

16:00-16:30

Safety and Trust in Autonomous Driving

Lu Feng

16:00-16:20

Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.

Stefan Badelt, Erik Winfree

16:20-16:40

Using Transitivity and Modularity in Chemical Reaction Network Bisimulation

Robert F. Johnson

16:40-17:00

Conservative approximations of polymers

Ken Chanseau Saint-Germain, Jerome Feret

17:00-17:20

Executable Biochemical Space for Specification and Analysis of Biochemical Systems

M. Troják, J. Šalagovič, D. Šafránek, J. Červený, L. Brim, M. Hajnal

17:20-17:40

Formal Verification of Network-Based Biocomputation Circuits

Hillel Kugler, Till Korten, Stefan Diez, Dan Nicolau Jr.

16:00-16:30

The Map Equality Domain

D. Dietsch, M. Heizmann, J. Hoenicke, A. Nutz, A. Podelski

16:30-17:00

Loop Detection by Logically Constrained Term Rewriting

Naoki Nishida, Sarah Winkler

17:00-17:30

Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment

Jonas Oberhauser

16:00-16:30

Termination of Lambda-Pi modulo rewriting using the size-change principle

Guillaume Genestier, Frédéric Blanqui

16:30-17:00

Improving Static Dependency Pairs for Higher-Order Rewriting

Carsten Fuhs, Cynthia Kop

17:00-18:00 WST 2018 business meeting

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

15:30-16:00 Coffee Break