Project Colloquium

At ERATO MMSD Project (access instructions:


Masaki Waga / Zhenya Zhang (26 Sep) -- private colloquium, details will not be announced

Chao Huang (3 Oct)

Wed 5 September 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Clovis Eberhart (NII)

Game semantics is a class of models of programming languages in which

types are interpreted as games and programs as strategies.  Such game

models have successfully covered diverse features, such as functional

and imperative programming, or control operators.  Standardly, plays

on a given game form a poset, and strategies are downward-closed sets

of ``accepted'' plays.  Game semantics has recently been extended to

non-deterministic and concurrent languages, which generated an

in-depth recasting of the standard approach: plays are now organised

into a category, on which strategies are presheaves. The fundamental

notion of innocence (which characterises purely functional programs)

has also been recast as a sheaf condition.  I will talk about the work

I have done during my PhD, when I studied various constructions

appearing in this new approach to game semantics.  The goal of this

work is to exhibit links between game models – which have nearly

exclusively been studied on their own until now – in order to give a

unified understanding of game semantics.

We first consider a pattern common to several game models of

concurrent languages, in which games and plays are first organised

into a double category, from which strategies are then derived.  We

provide an abstract construction of such a double category from more

basic data, and prove that, under suitable hypotheses, the result

allows the construction of strategies.

Our second contribution is to relate two established techniques for

defining plays: the standard one, based on justified sequences, and a

more recent one, based on string diagrams.  We first show how to

(fully) embed the notion of plays in the former approach into the

latter and then derive from this an equivalence between the categories

of innocent strategies in both models, thus showing that they induce

essentially the same model.

Finally, we design a framework to study game models from an abstract

point of view.  From a description of the notions of game and play, we

abstractly derive a category of games and strategies whose

construction is based on intuitions from game semantics. We also

refine the axioms to deal with innocence, and prove that, under

suitable hypotheses, innocent strategies are stable under composition.

Mon 27 August 2018, 16:30–18:00

NII Room 1901--1903

Joost-Pieter Katoen (RWTH Aachen University),

Bayes meets Dijkstra -- Exact Inference by Program Verification

In this talk, I will give a perspective on inference in Bayes' networks

(BNs) using program verification. I will argue how weakest precondition

reasoning a la Dijkstra can be used for exact inference (and more). As

exact inference is NP-complete, inference is typically done by means of

simulation. I will show how by means of wp-reasoning exact expected

sampling times of BNs can be obtained in a fully automated fashion. An

experimental evaluation on BN benchmarks demonstrates that very large

expected sampling times (in the magnitude of millions of years) can be

inferred within less than a second. This provides a means to decide

whether sampling-based methods are appropriate for a given BN. The key

ingredients are to reason at program code in a compositional manner.

Wed 1 August 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Taichi Uemura (University of Amsterdam)

Cubical Assemblies and the Independence of the Propositional Resizing Axiom

Cubical type theory gives a constructive justification of the univalence axiom. A model of this type theory in cubical sets is build, informally, in constructive metatheory, so this construction should work internally in suitable categories other than Set. Orton and Pitts have given a sufficient condition for modeling cubical type theory in an elementary topos. Based on their work, I build the cubical set model internally in the category of assemblies. A feature of this new model is that it has a universe which is impredicative as well as univalent, but this model does not satisfy the propositional resizing axiom.

Wed 4 July 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Akihisa Yamada (National Institute of Informatics),

Towards a Unified Method for Termination

The question of how to ensure programs terminate has been for decades

attracting remarkable attention of computer scientists, resulting in a

great number of techniques for proving termination of term rewriting and

other models of computation. Nowadays it has become hard for newcomers

to come up with new termination techniques/tools, since there are so

many to learn/implement before inventing a new one. In this talk, I

present my past and ongoing work towards unified method for

termination, that allow one to learn/implement a single idea and obtain

many well-known techniques as instances.

Mon 25 June 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Georgios Fainekos (Arizona State University),

Temporal Logic Planning for Mobile Robots: What happens when missions cannot be satisfied?



Temporal logic planning methods have provided a viable path towards solving the single- and multi-robot path planning, control and coordination problems from high level formal requirements. In the existing frameworks, the prevalent assumptions are (1) that a plan always exists which satisfies the mission requirements, and (2) that there is a single stakeholder with full or partial knowledge of the environment that the robots operate in. In addition, it is typically assumed that the requirements themselves are fixed and do not change over time. However, any of these assumptions may not be valid in both off-line and on-line temporal logic planning problems. That is, multiple stakeholders and inaccurate sources of information may produce unsatisfiable missions or self-contradictory models of the world or the system. Classical temporal logic planning methods cannot handle non-consistent model environments or missions even though such inconsistencies may not affect the planning problem. In this talk, we present how the user feedback problem for unsatisfiable missions can be reduced to searching for an optimal weighted path on a graph. Albeit the general search problem is NP-complete, the graph formulation of the problem opens-up the possibility for the development of efficient approximation algorithms. We present a number of heuristics for quickly computing such user feedback and we present experimental results on the performance and scalability of our solutions. Finally, we show how inconsistencies and conflicts in the mission requirements and the model of the world can be circumvented by utilizing multi-valued temporal logics and system models.



Georgios Fainekos is an Associate Professor at the School of Computing, Informatics and Decision Systems Engineering (SCIDSE) at Arizona State University (ASU). He is director of the Cyber-Physical Systems (CPS) Lab and he is currently affiliated with the NSF I/UCR Center for Embedded Systems (CES) at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens (NTUA). Before joining ASU, he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. His expertise is on logic, formal verification, testing, control theory, artificial intelligence, and optimization. His research has applications to automotive systems, medical devices, autonomous (ground and aerial) vehicles, and human-robot interaction (HRI). In 2013, Dr. Fainekos received the NSF CAREER award and the ASU SCIDSE Best Researcher Junior Faculty Award. He is also recipient of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. His software toolbox, S-TaLiRo, for testing and monitoring of CPS has been nominated twice as a technological breakthrough by the industry. In 2016, Dr. Fainekos was the program co-Chair for the ACM International Conference on Hybrid Systems: Computation and Control (HSCC).

Wed 20 June 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Kenta Cho (National Institute of Informatics),

An overview of effectus theory

I'll give an overview of effectus theory, which I worked on during my

PhD in Nijmegen, the Netherlands. Effectus theory aims to describe

quantum theory in a categorically axiomatized setting -- where

classical (deterministic and probabilistic) theories are special

cases. The basic notion here is an `effectus', a category with

suitable effect algebra and partially additive structure. In the talk

I'll present selected results in effectus theory, as well as

background information and basic definitions/examples.

Wed 13 June 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Taro Sekiyama (National Institute of Informatics),

Towards automated proof synthesis for intuitionistic propositional logic with deep learning

I report ongoing work on proof synthesis for intuitionistic propositional logic using deep learning.

My talk consists of two parts.  The first is an application of an off-the-shelf deep neural network (DNN)

model for machine translation tasks to proof synthesis.  The idea of this work is to view the proof

synthesis problem as a translation from the proposition logic to the proof language.  Although the DNN

model often generates syntactically and/or logically incorrect proofs, we find that they are useful as a

guide of proof synthesis.  The second part is to introduce a DNN model, which we call

a proposition-to-proof model, specialized to proof synthesis.  To this end, we make a statistical model

for proof synthesis, show that the statistical model can be decomposed to fine-grained probability

distributions, and design the proposition-to-proof model to approximate the fine-grained distributions.  

We also empirically confirmed that the proposition-to-proof model outperforms the off-the-shelf model in

the first part for proof synthesis.

Wed 6 June 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Toru Takisaka (National Institute of Informatics),  
Ranking and Repulsing Supermartingales for Approximating Reachability

(joint work with Yuichiro Oyabu, Natsuki Urabe and Ichiro Hasuo)

Computing reachability probabilities is a fundamental problem in the

analysis of probabilistic programs. This talk aims at a comprehensive

and comparative account on various martingale-based methods for over-

and under-approximating reachability probabilities. Based on the

existing works that stretch across different communities (formal

verification, control theory, etc.), we offer a unifying account. In

particular, we emphasize the role of order-theoretic fixed points---a

classic topic in computer science---in the analysis of probabilistic

programs. This leads us to two new martingale-based techniques, too. We

give rigorous proofs for their soundness and completeness. We also make

an experimental comparison using our implementation of template-based

synthesis algorithms for those martingales.

Wed 30 May 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Tomoo Yokoyama (Kyoto University of Education),  
Topological methods for analyzing two dimensional flows

We introduce new topological methods, called a word representation and

a tree representation, for analyzing 2D flows. Applying the

topological methods to a plate in a time-dependent uniform flow under

mild conditions, we can estimate when the lift-to-drag ratios of the

plate are maximal and can determine the intermediate topologies of the

uniform flow.

Our talk consists of three parts. In fact, first we quickly review

topology and dynamical systems. Second, we present applications of our

methods. Finally we introduce the theoretical background and discuss

the relative works and the relations between topological structures

and data structures (e.g. implementation of representation algorithms,

contour extraction of streamlines from image data, generating all word

representation by an automaton, generating all tree representation by

"regular tree grammar + cyclic order", improvement of industrial

machines, possibilities of analyzing ocean phenomena and medical


Wed 23 May 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Sergiy Bogomolov (The Australian National University),  
Towards Scalable Verification of Cyber-Physical Systems

Cyber-physical systems (CPS) are networks of physical and digital

components and present a next generation of large-scale

highly-interconnected networked embedded systems. On the one hand, CPS

open enormous opportunities as they form the core of emerging smart

devices and services which are going to revolutionize many traditional

industries such as automotive, traffic management, power

generation and delivery, as well as manufacturing. On the other hand,

highly autonomous systems pose special engineering challenges as any

unexpected behaviour might lead to large financial losses or even

human deaths.

In this talk, we address this challenge and propose automatic

techniques to analyze CPS. For this purpose, we use the concept of

hybrid automata which has proven to be particularly useful to model

CPS. We give an overview of techniques to ensure efficient analysis of

hybrid automata. In particular, we present support-function based

representation of region state space and discuss ways to refine it.

Finally, we discuss the connection between verification and hybrid

planning, and use autonomous driving to showcase benefits their

interplay can result at.

Time-Triggered Conversion of Guards for Reachability Analysis

of Hybrid Automata

A promising technique for the formal verification of

embedded and cyber-physical systems is flow-pipe construction, which

creates a sequence of regions covering all reachable states over time.

Flow-pipe construction methods can check whether specifications are

met for all states, rather than just testing using a finite and

incomplete set of simulation traces. A fundamental challenge when

using flow-pipe construction on high-dimensional systems is the cost

of geometric operations, such as intersection and convex hull. In this

talk, we address this challenge by showing that it is often possible

to remove the need to perform high-dimensional geometric operations by

combining two model transformations, direct time-triggered conversion

and dynamics scaling. Further, we discuss how to make the

overapproximation error in the conversion arbitrarily small. Finally,

we show that our transformation-based approach enables the analysis of

a drivetrain system with up to 51 dimensions.

Short Bio

Sergiy Bogomolov is on the faculty of the Australian National University where he leads the Dependable Cyber Physical Systems Lab. Prior to joining ANU Sergiy was a Postdoctoral Researcher in the Institute of Science and Technology Austria. Sergiy is broadly interested in algorithms and techniques to support design and development workflow of trustworthy and resilient autonomous systems. For this purpose, he uses and develops techniques on the interface of cyber-physical systems verification and AI planning. His Ph.D. and M.Sc. degrees are from the University of Freiburg, Germany.

Wed 9 May 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Paolo Arcaini (National Institute of Informatics),  
Decomposition-Based Approach for Model-Based Test Generation

Model-based test generation by model checking is a well-known testing

technique that, however, suffers from the state explosion problem of

model checking and it is, therefore, not always applicable. In this

talk, I present an approach that addresses this issue by decomposing a

system model into suitable subsystem models separately analyzable. The

technique consists in decomposing that portion of a system model that

is of interest for a given testing requirement, into a tree of

subsystems by exploiting information on model variable dependency. The

technique generates tests for the whole system model by merging tests

built from those subsystems. Effectiveness and efficiency of the

proposed decomposition-based test generation approach are measured

both in terms of coverage and time.

Wed 25 April 2018, 16:00–17:00

ERATO MMSD Takebashi Site Common Room 3

Ichiro Hasuo (National Institute of Informatics),  
Approximating Reachability Probabilities by (Super-)Martingales

Reachability is a fundamental problem in the analysis of probabilistic systems. It is well-known that reachability probabilities are efficiently computed for finite-state systems by linear programming. However, this LP method does not apply to systems that have infinitely many configurations, such as probabilistic programs and parametric systems. In such a case, we have to rely on a parametric witness (i.e. a function) for over- or under-approximating reachability probabilities. A well-studied class of such witnesses is that of supermartingales. In this talk I will talk about our recent results that refine existing supermartingale-based methods. The technical keys to those results are: choice of a suitable martingale concentration lemma for over-approximation; and a categorical axiomatization of supermartingales by coalgebras and corecursive algebras. The talk is based on my joint work with Natsuki Urabe, Masaki Hara, Bart Jacobs, Toru Takisaka and Yuichiro Oyabu.

Thu 22 March 2017, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Fuyuki Ishikawa (National Institute of Informatics),  
Formal Methods and Industry - TopSE Experience

Formal Methods have been considered as a representative of "technologies unaccepted by the industry." There have been many negative "myths", true or not, for tens of years. Nevertheless, not limited to Formal Methods, industry-academia collaboration is a vital means to tackle emerging challenges in engineering of complex software systems.

In this talk, I report our TopSE program at NII. TopSE is an educational program for the industry on advanced software engineering (including Formal Methods). Intensive curriculum is provided, not only over 40 lecture classes tailored for the industry but also schemes for application research studies. TopSE has more than 300 graduates and welcomes about 60 "students" (engineers and researchers) in 2018, which I would say a success as a paid course for the industry. I report and discuss the activities on Formal Methods in TopSE including the lecture design, statistics of feedback, and trends in application studies.

Thu 15 March 2017, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Thorsten Wissmann (FAU Erlangen-Nürnberg),  
Efficient Coalgebraic Partition Refinement

This talk presents a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence. Coalgebraic generality implies in particular that not only classical relational systems are covered but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, the generic algorithm runs in time O(m⋅log n) where n and m are the numbers of nodes and edges, respectively. Instances of the generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.

Thu 1 March 2018, 16:00–18:00

ERATO MMSD Takebashi Site Common Room 3


Étienne André (University Paris 13),  
Parametric timed automata: theory and applications

Critical real-time systems must be formally verified to prevent any undesired behavior. When some timing constants are known with only a limited precision, traditional timed model-checking techniques may not apply anymore.

We use here the formalism of parametric timed automata. Parametric timed automata are very expressive, and decision problems are notoriously very hard (in fact most interesting decision problems are undecidable). On the one hand, we review decidability results, and propose new decidable subclasses. On the other hand, we adopt a more pragmatic approach, and show that parametric timed automata allow us to model and verify distributed real-time systems; using the IMITATOR software, we derive best- and worst-case execution times for a real-time system designed by Thales, and subject to uncertainty in some tasks periods.

We also briefly report on recent techniques to speed-up the verification time using abstractions, and on distributed parametric model checking.


Bart Jacobs (Radboud University Nijmegen),  
Privacy and Security in Identity Management and Medical Research

This talk will given an overview of the ideas behind two practically oriented security and privacy projects at Nijmegen, NL:

1. Attribute-based identity management via the IRMA platform, see

If interested, you can before the talk already install the IRMA app on your (Android or iOS) phone and collect some attributes yourself.

2. Polymorphic encryption and Pseudonymisation for a large scale Parkinson research study, see:

Wed 28 February 2018, 10:00–11:30

ERATO MMSD Takebashi Site Common Room 3

Bart Jacobs (Radboud University Nijmegen),
A Channel-Based Perspective on Bayesian Networks

This talk will present a systematic, logical perspective on Bayesian networks, starting from the notion of "channel", that is, Kleisli map for the distribution monad. It will involves, states and predicates and conditioning, predicate- and state-transformation, forward and backward inference. Moreover, the fundamental correspondence between joint states and channels will be described as the basis of Bayesian networks. In the end, a new "transformation inference" algorithm will be described and compared to the standard "variable elimination" inference algorithm.

Background reading:

- B. Jacobs and Fabio Zanasi, A predicate/state transformer semantics for Bayesian learning. In: L. Birdedal (ed), Mathematical Foundations of Program Semantics (MFPS 2016), ENTCS 325, p.185-200, 2016.

- K. Cho, B. Jacobs, Disintegration and Bayesian Inversion, Both Abstractly and Concretely,

- K. Cho, B. Jacobs, The EfProb Library for Probabilistic Calculations. In: F. Bonchi and B. König (eds), CALCO 2017. LIPIcs 72, 25:1-7, 2017.

Additionally for people who like metrics:

- B. Jacobs, F. Zanasi, A Formal Semantics of Influence in Bayesian Reasoning. In: K. Larsen, H. Bodlaender and J.-F. Raskin (eds), Mathematical Foundations of Computer Science (MFCS), LIPIcs 83, 2017.

- B. Jacobs and Bram Westerbaan, Distances between States and between Predicates.

Thu 22 February 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Takeo Uramoto (Tohoku University),  
Recent developments in algebraic language theory

The purpose of this talk is to introduce a recent (2008~) active research trend in  algebraic language theory. This field, among other approaches to formal languages, is characterized by its methodology: one reduces combinatorial / logical problems on formal languages (say, regular languages) into some tractable problems on algebraic structures (resp., finite semigroups). Recent works in the last decade shed new lights on this field (or its methodology) from the viewpoint of Stone-type duality theorem; and most importantly, indicated several new research directions extending classical frameworks. In this talk, based on our own works, we introduce this research trend (and its background motivation) and then carefully discuss its possible future directions.


Thu 15 February 2018, 16:30–18:00

ERATO MMSD Takebashi Site Common Room 3

Georg Moser (University of Innsbruck),  
Uniform Resource Analysis

In this talk, I'll describe how rewriting techniques can be successfully employed to built state-of-the-art automated resource analysis tools which favourably compare to other approaches. Furthermore I'll sketch the genesis of a uniform framework for resource analysis, emphasising success stories, without hiding intricate weaknesses

and how those can be overcome in future work.

Thu 8 December 2017, 10:00–11:30

ERATO MMSD Takebashi Site Common Room 3

Toru Takisaka (Kyoto University),  
On Use of Martingales to Refute Almost Reachability

It is well known that supermartingales can

Thu 28 December 2017, 10:00–11:30

ERATO MMSD Takebashi Site Common Room 3

Toru Takisaka (Kyoto University),  
On Use of Martingales to Refute Almost Reachability

It is well known that supermartingales can be used to prove almost-termination of probabilistic transition systems.

Recently Chatterjee et al. [1] proposed a way of their use to refute almost-termination.

A crucial tool in their proofs is the Azuma's inequality, which roughly states that one does not have much chance to earn money in a fair gambling. In this talk we do the similar argument as [1] using another inequality instead of Azuma's one. The resulting martingale technique is much simpler and complete, i.e. finding a witnessing supermartingale for given non-almost-terminating system is always possible.

[1] C. Chatterjee, P. Novotny and D. Zikelic. Stochastic Invariants for Probabilitsic Termination. Proc. POPL2017.

Thu 30 November 2017, 16:30–18:45

ERATO MMSD Takebashi Site Common Room 3


Jérémy Dubut (NII),  
Some thoughts on bisimilarity using open morphisms

In this talk, I will present some work I have done on open morphisms during my PhD. I will start by giving an introduction on this categorical formalism from Joyal, et al.’s work on bisimilarity defined as the existence of a span of morphisms having some lifting properties with respect to “execution shapes”. I will show you examples, relational and logical characterisations for this bisimilarity.

Next, I would like to present two quite different aspects of this theory that I used during my PhD. First, a general framework, called the accessible categorical models, where the open morphisms formalism is particularly nice. This is a case where it is possible to define a nice notion of trees. In this framework, we show that bisimilarity can be precisely captured by the existence of some bisimulation relation on executions, but also that there is a fine notion of unfolding, which acts very similarly as a universal covering. Secondly, a particular case of the theory of Joyal et al.: the bisimilarity of diagrams, namely functors from a small category to a specified category of values. I will show you that this case is equivalent to the existence of a nice notion of bisimulations, which allows us to translate the problem of bisimilarity, to a problem of isomorphisms in the category A, which is useful for (un)decidability. I will finally show you how to translate the general setting of Joyal et al. where the category of paths is small into diagrams, and I will describe the relation between the different bisimilarities involved.


Akihisa Yamada (NII),  

Mathematics for Complexity Analysis

IsaFoR is a library of Isabelle-formalized theorems for validating program analyzers, originally on term rewriting. My previous work was to extend the library for more practical programing languages and also to enrich the library with deep results from mathematics. In this talk, I will explain how complexity analysis leads us to formalizing algebraic numbers, the Berlekamp factorization, Jordan normal forms, and the Perron-Frobenius theorem.

Thu 9 November 2017, 16:30–18:45

ERATO MMSD Takebashi Site Common Room 3


Jurriaan Rot (Radboud University),  
Traces and Triangles

In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore category. I will talk about recent joint work with Bart Jacobs, which elaborates two new unifying ideas in the theory of coalgebraic trace semantics: 1) previous approaches can be placed and connected in so-called state-and-effect triangles, that arise in the semantics of programs; 2) coalgebraic trace semantics is naturally presented in terms of corecursive algebras. This perspective puts the different approaches under a common roof, and allows us to derive conditions under which they coincide.


Kenta Cho (Radboud University),  

String diagrams in probability theory

String diagrams are a graphical language for monoidal categories, which has become very popular in categorical quantum mechanics initiated by Abramsky and Coecke. In this talk I will explain that string diagrams are also useful for (classical) probability theory. The Kleisli categories of the distribution and the Giry monad give concrete interpretation of string diagrams, respectively, for discrete probability and general measure-theoretic probability. Topics include disintegration, Bayesian inversion, and conditional independence. The talk is based on joint work with Bart Jacobs; see preprint

Thu 26 October 2017, 16:30–18:45

ERATO MMSD Takebashi Site Common Room 3


Zhenya Zhang (SOKENDAI, ERATO MMSD),  
Localization of Linearizability Faults on the Coarse-Grained Level

Linearizability is an important correctness criterion that guarantees the safety of concurrent data structures. Due to the nondeterminism of concurrent executions, reproduction and localization of a linearizability fault still remain challenging. The existing work mainly focuses on model checking the thread schedule space of a concurrent program on a fine-grained (state) level, and hence suffers from the severe problem of state space explosion. This paper presents a tool called CGVT to build a small test case that is sufficient enough for reproducing a linearizability fault. Given a possibly long history that has been detected non-linearizable, CGVT first locates the operations causing a linearizability violation, and then synthesizes a minimum test case for further investigation. Moreover, we present several optimization techniques to improve the effectiveness and efficiency of CGVT.We have applied CGVT to 10 concurrent objects, while the linearizability of some of the objects is unknown yet. The experiments show that CGVT is powerful and efficient enough to build the test cases more adaptable for a fine-grained fault localization.


David Sprunger (NII, ERATO MMSD),  

Bisimulation and precongruence approaches to coinductive predicates

In this talk, I will take a very low-level view of coalgebras to contrast two very similar approaches to behavioral equivalence. Bisimulation has a long history stretching back to Milner and Park's use in the context of concurrent systems. Often bisimulation is used in concert with a restriction on the transition system type to ensure certain nice properties of bisimulations hold, namely that the type functor preserve weak pullbacks. I will use several representation results due to Adamek and various collaborators to bypass the typical categorical presentation of coalgebras and give a view closer to "bare metal" on the weak pullback preservation condition and why it is often needed when using bisimulations.

A lesser known approach to behavioral equivalence involves a type of relation called a precongruence, introduced by Aczel and Mendler in 1989. Precongruences are subtly different than bisimulations for system types which do not preserve weak pullbacks. However, they retain many of the important properties we use the weak pullback preservation property to obtain for bisimulations. I will show how using a precongruence approach to two coinductive predicates--behavioral equivalence and language inclusion--obviates the need for this property.

Thu 12 October 2017, 16:30–18:45

ERATO MMSD Takebashi Site Common Room 3


Krzysztof Czarnecki (University of Waterloo),  
Designing and Testing Autonomous Vehicles: What the Engineers are Doing and Thinking

How do you design and then test a vehicle that is supposed to drive itself.  In any environment. Without getting into an accident.  Ever?  This presentation will explore autonomous vehicles from an engineering standpoint.  What is an autonomous vehicle and how (and when) will vehicles evolve to reach this state?  Crash course on how autonomous vehicles work.  What are the challenges in programming and then testing automated vehicle technologies? What are the legal and ethical issues that arise?

The second part of the presentation will focus on the ongoing work at the University of Waterloo on safety assurance and validation and verification of autonomous vehicles.


Sean Sedwards (National Institute of Informatics),  

Lightweight Verification of Markov Decision Processes

Markov decision processes (MDP) are a useful abstraction of discrete nondeterminism that can be used to optimise both discrete and continuous time models. MDPs may be verified numerically (i.e. optimised) in polynomial time with respect to the size of their state space, however this increases exponentially with the number of state variables. Popular existing approximative verification techniques tend to only partially address this “state explosion” and have other problems.

I will present a recently developed technique of “lightweight" verification of Markov decision processes, based on an O(1) memory representation of history-dependent schedulers. This allows schedulers to be chosen at random and constructed on the fly, thus facilitating scalable verification on massively parallel computational architectures.

Fri 22 September 2017, 15:00–17:00

NII meeting room 2010 

Masaaki Konishi (Research Manager, ERATO MMSD),
Practical issues and measures of Search Base Test for engine control software

My former job was Verification and Validation application development on vehicle control software in an automotive company. Automotive control software is getting larger and more complicate to meet customers’ demand and various kinds of regulations and it takes huge amount of time and manpower to ensure software quality.  In this situation “Falsification” (Search Base Test) using closed loop simulation is expected to be a promising approach. However, there still remain some practical issues to apply and expand the usage. In this talk I will introduce  the issues and measures on two items, 1) metrics to measure searching extent and 2) evaluation of realistic input scenario.

Fri 15 September 2017, 15:00–17:15

NII meeting room 2010 


Xavier Rival (INRIA/CNRS/ENS Paris),  
Towards a library of abstract domains to describe memory properties

In this talk, we will present MemCAD, an abstract interpreter that integrates a library of abstract domains to represent properties of memory states. It can describes structures, dynamic structures, and arrays. It can also interact with abstract domains that represent numeric properties and constraints over set symbols. It relies on interfaces that allow adding novel abstract domains, and to define combination operators, to build up advanced abstract domains from basic ones.

We will present the structure of the analyzer and highlight the main abstract domains that it implements. We will also highlight the core analysis algorithms, and show a few examples of static analyses using these domains.


Kokichi Futatsugi (National Institute of Advanced Industrial Science and Technology),  Specification Verification with CafeOBJ

Specification is description of model, and its verification is to show that the model has desired properties by deducing the properties from the specification.  As the proverb says “All models are wrong, some are useful”, and specification verification is an effective way for getting the useful models.

CafeOBJ is an executable algebraic specification language system which can be used as a specification verification system. CafeOBJ's specification is a set of equations and transition rules (including conditional ones), and the deduction is equational inference.  The equational inference is implemented through reduction by interpreting the specification's equations as left to right rewriting/reduction rules.  This transparent view of CafeOBJ's specification verification relaxes inherent difficulty of specification verification.  CafeOBJ language also has powerful constructs for modules including parameterized ones, and it makes it easy to write well formed reusable specifications and proof scores (scripts).

This talk gives an overview of specification verification with CafeOBJ, focusing on recent developments about "specification calculus" and "refinement of proof constants".

Fri 1 September 2017, 13:00–15:00

NII meeting room 2010 

Shaukat Ali (Simula Research Laboratory),  Uncertainty-based Test Case Generation and Minimization for Cyber-Physical Systems: A Multi-Objective Search-based Approach

Cyber-Physical Systems (CPSs) typically operate in highly indeterminate environmental conditions, which require the development of testing methods that must explicitly consider uncertainty in test design, test generation, and test optimization. Towards this direction, we propose uncertainty-wise test case generation and test case minimization strategies that rely on test ready models explicitly specifying subjective uncertainty. We propose two test case generation strategies and four test case minimization strategies based on Uncertainty Theory and multi-objective search. These strategies include a novel methodology for designing and introducing indeterminacy sources in the environment during test execution and a novel set of uncertainty-wise test verdicts. We performed an extensive empirical study to select the best algorithm out of eight commonly used multi-objective search algorithms, for each of the four minimization strategies, with five use cases of two industrial CPS case studies. The minimized set of test cases obtained with the best algorithm for each minimization strategy were executed on the two real CPSs. The results showed that our best test strategy managed to observe 51% more uncertainties due to unknown indeterminate behaviors of the physical environment of the CPSs as compared to the rest of the test strategies. In addition, the same test strategy managed to observed 118% more unknown uncertainties as compared to the unique number of known uncertainties.

Download Link:

Fri 25 August 2017, 15:00–17:00

NII meeting room 1901 

Yusuke Kawamoto (National Institute of Advanced Industrial Science and Technology),  Hybrid method for program analysis -- combining statistical analyses with symbolic techniques

In modeling and analyzing a probabilistic system, the statistical approach is often useful to efficiently evaluate quantitative aspects of the behaviors of the system. It is usually considered as a blackbox testing approach in which the analyst runs the system many times and records the execution traces to construct an approximate model of the system. Due to this random sampling of the system, statistical analysis provides only approximate estimates while it can evaluate the accuracy and error of the analysis, e.g. by statistical hypothesis testing. Although a large sample size may be required to have accurate estimates, it can be reduced by employing symbolic techniques from program analysis.

In this talk we introduce basic ideas on the statistical analysis on probabilistic programs, and on a hybrid method that combines the statistical analysis with symbolic techniques. We then show how the hybrid method (presented in [1,2]) is used in estimating entropy-based properties in the context of quantitative information flow. In particular, we present the mathematical details on how to correct the bias of the estimate and how to compute a confidence interval to evaluate the accuracy of the estimation.

[1] Yusuke Kawamoto, Fabrizio Biondi and Axel Legay.

Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow.

In Proc. of 21st International Symposium on Formal Methods (FM 2016), Lecture Notes in Computer Science, Vol.9995, pp.406-425, November 2016.

[2] Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, and Louis-Marie Traonouez.

HyLeak: Hybrid Analysis Tool for Information Leakage.

In Proc. of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), Lecture Notes in Computer Science, October 2017, To appear.

Fri 4 August 2017, 15:00–17:00

NII meeting room 2010 

Masako Kishida (National Institute of Informatics),  Introduction to event- and self-triggered control

Many of recent control systems are connected via networks. This is because the use of network for communications among the system elements reduces the deployment cost and increases the flexibility compared with the conventional wired communications. However, the use of network often forces the system to perform control tasks with limited resources such as communication channel bandwidth and battery power. Thus, the importance of resource-aware control approaches that satisfy given performance requirements has been increased.

This talk starts with an introduction to control theory, where we will go over the basics and concepts of control theory as well as some control approaches to different types of control problems. Following the introduction, recent studies of event-triggered and self-triggered controls that are designed to be resource-efficient will be presented.

Fri 14 July 2017, 15:00–17:00

NII meeting room 2010 

Hayato Waki (Kyushu University),  Computational aspects on non-strictly feasible semidefinite program

 Semidefinite program (SDP) is the convex minimization on matrix variables. Some efficient algorithms to solve SDPs, e.g., the ellipsoid method and interior-point method are proposed, and applications of combinatorial optimization, polynomial optimization, control and statistics etc are well-known. The strict feasibility of SDP guarantees the celebrated strong duality theorem on SDP and the convergence of algorithms to solve SDP. However non-strictly feasible SDPs often appear in these applications, and we can see that the behavior of  algorithms are numerically unstable.  We talk on computational aspects on such SDPs. In particular, we present some properties of non-strictly feasible SDPs in control theory are and numerical remedy for such SDPs.

Fri 30 June 2017, 15:00–17:00

NII meeting room 2010 

Georgios Fainekos (Arizona State University),  Beyond Requirements Falsification : Semi-formal methods and tools for the analysis of Cyber-Physical Systems

Correct-by-design synthesis methods for Cyber-Physical Systems (CPS) are still in their infancy for CPS with complex physical dynamics. For that reason, a combination of design theories for simpler systems and/or ad-hoc design approaches are utilized. Hence, numerous design and implementation errors are discovered while CPS are operational in the field. Such errors can have catastrophic effects to human life and to the economy. Over the last few years, requirements guided falsification methods have proven to be a practical approach to the verification problem of industrial size CPS. However, requirements falsification is just one component of the necessary tools for the development of safe and reliable CPS. In this talk, we provide an overview of our research in providing support for all the stages of the development for CPS, from formal requirements elicitation and mining to system conformance to on-line monitoring. Most of our methods have been implemented in a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). Finally, in this talk, we demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive industry.


Georgios Fainekos is an Associate Professor at the School of Computing, Informatics and Decision Systems Engineering (SCIDSE) at Arizona State University (ASU). He is director of the Cyber-Physical Systems (CPS) Lab and he is currently affiliated with the NSF I/UCRC Center for Embedded Systems (CES) at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens and an M.Sc. degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU, he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. He is currently working on Cyber-Physical Systems (CPS) and robotics. In particular, his expertise is on formal methods, logic, control theory, artificial intelligence, and optimization. His research has applications to automotive systems, medical devices, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2013, Dr. Fainekos received the NSF CAREER award. He was also recipient of the SCIDSE Best Researcher Junior Faculty award for 2013 and of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. Two of his conference papers have been nominated for student best paper awards. In 2016, Dr. Fainekos was the program co-Chair for the ACM International Conference on Hybrid Systems: Computation and Control.

Fri 23 June 2017, 15:00–17:00

NII meeting room 2010 

Gidon Ernst (ERATO MMSD),  Flashix: A verified, crash-tolerant flash file system

In the Flashix project, a file system for flash memory has been developed. It is proven functionally correct and tolerates system crashes such as abrupt power cuts at any point in time during its execution. The development approach is based in incremental and modular refinement. This talk gives an overview over the verification approach, the challenges for the practical development, and the results.

Fri 16 June 2017, 15:00–17:00

NII meeting room 2010 

Kenji Tei (NII),  Models@run.time for self-adaptive systems: A controller synthesis approach

In many application domains, continuous operation is a desirable attribute for software-intensive systems. As the environment or system requirements change, so the system should change and adapt without stopping or unduly disturbing its operation. There is, therefore, a need for sound engineering techniques that can cope with dynamic change.

 In this talk, I will show models@run.time-based approach for self-adaptive systems. Models are hold and used event at runtime for analysis and reasoning about software system to guarantee adaptations. I will overview architecture and key techniques about this approach.

 In particular, I will talk about the problem of dynamic update of controllers in reactive systems when the specification (environment assumptions, requirements and interface) of the current system changes. I will present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur. Indeed, using controller synthesis I will show how to automatically build a controller that guarantees both progress towards update and safe update.

Thu 15 June 2017, 14:30–20:00

NII meeting room 1208-1210 

ERATO MMSD Project Kick-off Workshop

14:30-14:35 Introduction
14:35-14:55 Kengo Kido
           Nonstandard Static Analysis
           (Metatheoretical Transfer via Logic)
15:00-15:20 Natsuki Urabe
           Coalgebraic Unfolding in Forward and Backward Simulations
           (Metatheoretical Transfer via Category Theory)
15:25-15:45 Shin-ya Katsumata
           Simulations and Fibrational Liftings
           (Categorical Foundation for System Approximation)
15:45-16:00 Break
16:00-16:05 Interlude
16:05-16:25 Takamasa Okudono
           Generating Polynomial Interpolant with Semidefinite Programming
           (Numerical Optimization and Formal Methods)
16:30-16:50 Masaki Waga
           Efficient Timed Pattern Matching by Automata-Based Skipping
           (Automata Theory in Light-Weight Formal Methods)
16:55-17:15 Fuyuki Ishikawa
           Insights into Verification of Complex Systems from Software Testing Research
           (Formal Methods and Intelligence)

18:00-20:00 Continued Discussion

Fri 26 May 2017, 15:00–17:00

NII meeting room 2010 

Natsuki Urabe (The University of Tokyo & ERATO MMSD),  Categorical Liveness Checking by Corecursive Algebras

Final coalgebras as "categorical greatest fixed points" play a central role in the theory of coalgebras. Somewhat analogously, most proof methods studied therein have focused on greatest fixed-point properties like safety and bisimilarity. Here we make a step towards categorical proof methods for least fixed-point properties over dynamical systems modeled as coalgebras. Concretely, we seek a categorical axiomatization of well-known proof methods for liveness, namely ranking functions (in nondeterministic settings) and ranking supermartingales (in probabilistic ones). We find an answer in a suitable combination of coalgebraic simulation (studied previously by the authors) and corecursive algebra as a classifier for (non-)well-foundedness.


Fri 28 April 2017, 15:15–17:00

NII meeting room 2010 

Sean Sedwards (ERATO MMSD), Rare Event Simulation for Statistical Model Checking

Statistical model checking (SMC) avoids the intractable number of states associated with numerical model checking by estimating the probability of a property from a number of execution traces (simulations). Rare events nevertheless pose an important challenge to SMC because interesting properties, such as bugs and optima, are often very rare and occur infrequently in simulations. A key objective for SMC is thus to reduce the number and length of simulations necessary to produce an estimate with a given level of statistical confidence. In this talk I will describe two variance reduction approaches that address this problem: importance sampling and importance splitting. Importance sampling weights the probabilities of a system to make a rare property occur more frequently in simulations, then compensates the results by the weights. Importance splitting decomposes a rare property into the product of sub-properties that are less rare and easier to simulate. I will outline the challenges of using these techniques in SMC and highlight some practical solutions, including the recent successful application of importance sampling to stochastic timed automata.

Thu 13 April 2017, 17:00–18:00

Takebashi Site Common Room 3

Zhoulai Fu (UC Davis), A Mathematical Method for Reasoning about Numerical Code

 I will present Mathematical Execution (ME), a new, unconventional method for reasoning about numerical code. The idea is to reduce the problem of testing/verifying a program into the problem of minimizing a derived representing function. ME is particularly efficient for numerical code; it directs input space exploration by only executing the representing function, which avoids static or symbolic reasoning about the program semantics. We have applied ME on several instances: (1) satisfiability solving, (2) boundary value analysis, (3) coverage-based testing, and (4) path reachability. The results are extremely promising. During my presentation I will explain the unified method, that is ME, behind our very good results. I will use (1) and (2) above as two case studies.

Fri 7 April 2017, 15:00–16:00

Takebashi Site Common Room 3

Ichiro Hasuo (NII & ERATO MMSD), The ERATO MMSD Project: an Overview

Goals, Strategies and Tactics of the project.