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@nii.ac.jp)