[logic-ml] First NII Programming and Logic Workshop

[Makoto Tatsuta]

	       First NII Programming and Logic Workshop

Date: March 2--3, 2017

Place: National Institute of Informatics, Room 2006 (20th floor)
場所: 国立情報学研究所 20階 2006室
    (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分)
    (地図 http://www.nii.ac.jp/about/access/)

Program:

March 2

10:20--11:00 Wei-Ngan Chin (National University of Singapore)
Title: Automated Verification and Analysis of Expressive Specifications

11:00--11:40 Zhenjiang Hu (National Institute of Informatics)
Title: Towards Change-Oriented Programming

11:40--11:55 Break

11:55--12:35 Makoto Tatsuta (National Institute of Informatics)
Title: Presburger and Mutual Inductive Definitions

12:35--14:00 Lunch Break

14:00--14:40 Quang Loc Le (Singapore University of Technology and Design /
National University of Singapore)
Title: A Decidable Fragment in Separation Logic with Inductive
Predicates and Arithmetic

14:40--15:20 Hsiang-Shang Ko (National Institute of Informatics)
Title: An Axiomatic Basis for Bidirectional Programming

15:20--15:35 Break

15:35--16:15 Daisuke Kimura (Toho University)
Title: Decidability of Entailments in Separation Logic with Arrays

16:15--16:55 Mahmudul Faisal Al Ameen (National University of Singapore)
Title: Separation-Logic-Based Analyzer for Detecting Memory Errors

March 3

10:15--10:55 Koji Nakazawa (Nagoya University)
Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and
Inductive Definitions

10:55--11:35 Shin-Cheng Mu (Academia Sinica)
Title: Towards Derivation of Monadic Programs: A Case Study of States
and Nondeterminism

11:35--11:50 Break

11:50--12:30 Andreea Costea National University of Singapore)
Title: Automated Reasoning for Race-Free Channels with Explicit
Synchronization and Precise Disjunction

Abstracts:
----------------------------------------------------------------------
Speaker: Wei-Ngan Chin (National University of Singapore)
Title: Automated Verification and Analysis of Expressive Specifications
Abstract: 
The last two decades have seen a proliferation of research activities
in methodologies, techniques and systems for automated verification
and analysis of software programs. One driving force in this direction
has been the deployment of expressive logics that are able to capture
specifications of programs in a concise and precise manner. One of
these logics that my research group has been pre-occupied with in the
last decade is separation logic itself, made popular by seminal works
of John Reynolds and Peter O’Hearn. Separation logic is a
sub-structural which treats memory locations as resources that can be
transferred, borrowed or consumed. Such a resource logic allows
must-aliasing and updates to be succinctly expressed. We have looked
into various extensions to support expressive specification logics. We
have also explored automated verification techniques that work with
inductive predicates. We have proposed and evaluated decision
procedures on satisfiability and entailment on some fragments of our
logics. We have moreover extended our approach to support incremental
specification inference with the help of second-order unknown
predicates.  These works have challenged us to go beyond properties
that guarantee memory safety and correctness, to include also
termination, immutability infinity, deeper sharing, communication and
concurrency. We shall describe several aspects of our recent
endeavours here.
----------------------------------------------------------------------
Speaker: Zhenjiang Hu (National Institute of Informatics)
Title: Towards Change-Oriented Programming
Abstract:
Change is essential and expensive in software development. Although a
significant amount of work has been done on software change, its
status as a scientific discipline is still an open challenge. In this
talk, I will show that it is possible to treat software change as a
first-class citizen in software development. The success of this work
could lead to change-oriented programming, a new programming paradigm
that can effectively cope with software dynamics.
----------------------------------------------------------------------
Speaker: Makoto Tatsuta (National Institute of Informatics)
Title: Presburger and Mutual Inductive Definitions
Abstract:
This talk proposes some restrictions for a system of Presburger
arithmetic and mutual inductive definitions and proves the
decidability of truth in the system.  To prove it, this talk shows
that every inductively defined predicate in the system represents a
semilinear set.  Since inductively defined predicates can be
eliminated, the truth is decided in the arithmetic.  This system is an
extension of the system given in our APLAS 2016 paper but more
expressive as it can handle mutual inductive definitions and more than
one induction steps in inductive definitions.
----------------------------------------------------------------------
Speaker: Quang Loc Le (Singapore University of Technology and Design /
National University of Singapore)
Title: A Decidable Fragment in Separation Logic with Inductive
Predicates and Arithmetic
Abstract:
We consider the satisfiability problem for a fragment of separation
logic including inductive predicates with shape and arithmetic
properties.  We show that the fragment is decidable if the arithmetic
properties can be represented as semilinear sets. Our decision
procedure is based on a novel algorithm to infer a finite
representation for each inductive predicate which precisely
characterises its satisfiability. Our analysis shows that the proposed
algorithm runs in exponential time in the worst case. To show the
feasibility of our proposal, we have implemented our decision
procedure, integrated it into an existing verification system and
evaluated the solver on a set of satisfiability problems which is
generated from the verification of heap-manipulated programs.
----------------------------------------------------------------------
Speaker: Hsiang-Shang Ko (National Institute of Informatics)
Title: An Axiomatic Basis for Bidirectional Programming
Abstract:
Among the frameworks of bidirectional transformations proposed for
addressing various synchronisation problems, Foster et al.’s lenses
have influenced the design of a generation of bidirectional
programming languages. Most of these languages are highly declarative,
and only allow the programmer to specify a consistency relation with
limited control over the behaviour of the automatically derived
consistency restorer. However, synchronisation problems are diverse
and require vastly different consistency restoration strategies, and
the programmer must be empowered to fully control and reason about the
consistency restoration behaviour of their bidirectional programs. The
putback-based approach to bidirectional programming was proposed to
address this issue once and for all, and this talk will present the
latest result along this line of research: a Hoare-style logic for the
putback-based language BiGUL. With this Hoare-style logic, the BiGUL
programmer can precisely understand the bidirectional behaviour of
their programs by reasoning solely in the putback direction. The
theory underlying the Hoare-style logic has been formalised and
checked in the dependently typed language Agda, but this talk will
give a semi-formal presentation of the logic suitable for human
reasoning.
----------------------------------------------------------------------
Speaker: Daisuke Kimura (Toho University)
Title: Decidability of Entailments in Separation Logic with Arrays
Abstract:
We show decidability of validity of entailments in symbolic-heap
fragment of separation logic with arrays, which is designed for
verifying array-manipulating imperative programs.  Our proof is given
by translating entailments into formulas of Presburger Arithmetic,
which is known to be decidable.  Finally we provide an implementation
of our decision procedure, in which Presburger-formulas are decided by
an internally called SMT-solver.
----------------------------------------------------------------------
Speaker: Mahmudul Faisal Al Ameen (National University of Singapore)
Title: Separation-Logic-Based Analyzer for Detecting Memory Errors
Abstract:
This talk discusses an implementation of a separation-logic-based
analyzer for memory errors. This system is based on symbolic heap with
presburger arithmetic. This implementation extracts errors by
analyzing the strongest postcondition. The system abstracts all the
existentially quantified pointers. A while loop is analyzed using
fixed point analysis and it uses an arithmetic decision procedure. It
is also intended to analyze array and inter-procedure analysis.
----------------------------------------------------------------------
Speaker: Koji Nakazawa (Nagoya University)
Title: Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and
Inductive Definitions
Abstract:
We introduce a new cyclic-proof system CSLID_omega for separation
logic with inductively defined predicates. CSLID_omega is complete and
gives decision procedure for entailment checking based on the
unfold-match approach.
----------------------------------------------------------------------
Speaker: Shin-Cheng Mu (Academia Sinica)
Title: Towards Derivation of Monadic Programs: A Case Study of States
and Nondeterminism
Abstract:
Equational reasoning is among the most important tools that functional
programming provides us. Curiously, relatively little attention has
been paid on reasoning about monadic programs. In this talk we propose
some theorems and patterns useful for derivation of monadic programs,
focusing on non-determinism and states.
----------------------------------------------------------------------
Speaker: Andreea Costea National University of Singapore)
Title: Automated Reasoning for Race-Free Channels with Explicit
Synchronization and Precise Disjunction
Abstract: 
The usage of the message passing for inter-process communication
leveraged the performance and scalability of computing platforms
leading to a rise in the level of concurrency. Together with its
benefits though, message passing also places a burden on the safety
and correctness verification process of concurrent system, which was
already a challenging task even in the absence of message passing.
The current state of the art tackles this problem of safe message
communication assuming the systems rely solely of message passing in
order to obtain concurrency. However, this is generally not true,
since existing software tend to use a combination of synchronization
mechanisms.  Our aim is to break the assumption of unique
synchronization mechanisms, and step further into reasoning about
hybrid communication system, where different concurrency instruments
intermingle. We therefore present a multiparty session logic which
vows to marry the message passing model with explicit synchronization
mechanisms, such as CountDownLatch. In this context, we consider how
to ensure well-formedness of the session logic, and how to build
summaries that can help ensure race-freedom and type safety amongst
shared channels.
----------------------------------------------------------------------

問合せ先　龍田 (tatsuta at nii.ac.jp)