Thursday, November 24, 2016
Ichiro Hasuo, Associate Professor at Department of Computer
Science, the University of Tokyo, Japan
Talk 1: "Lattice-theoretic progress measures and co-algebraic model checking"
Abstract:
In the context of formal verification in general and model checking in
particular, parity games serve as a mighty vehicle: many problems are
encoded as parity games, which are then solved by the seminal
algorithm by Jurdzinski. In this paper we identify the essence of this
workflow to be the notion of progress measure, and formalize it in
general, possibly infinitary, lattice-theoretic terms. Our view on
progress measures is that they are to nested/alternating fixed points
what invariants are to safety/greatest fixed points, and what ranking
functions are to liveness/least fixed points. That is, progress
measures are combination of the latter two notions (invariant and
ranking function) that have been extensively studied in the context of
(program) verification.
We then apply our theory of progress measures to a general
model-checking framework, where systems are categorically presented as
coalgebras. The framework's theoretical robustness is witnessed by a
smooth transfer from the branching-time setting to the linear-time
one. Although the framework can be used to derive some decision
procedures for finite settings, we also expect the proposed framework
to form a basis for sound proof methods for some
undecidable/infinitary problems.
(Based on the joint work with Shunsuke Shimizu and Corina Cirstea
presented at POPL 2016)
============================
Talk 2: "Time Robustness in MTL and Expressivity in Hybrid System Falsification"
Abstract:
Building on the work by Fainekos and Pappas and the one by Donze and
Maler, we introduce AvSTL, an extension of metric interval temporal
logic by averaged temporal operators. Its expressivity in capturing
both space and time robustness helps solving falsification problems,
(i.e. searching for a critical path in hybrid system models); it does
so by communicating a designer's intention more faithfully to the
stochastic optimization engine employed in a falsification solver. We
also introduce a sliding window-like algorithm that keeps the cost of
computing truth/robustness values tractable.
(Based on the joint work with Takumi Akazaki presented at CAV 2015)
============================
Short bio:
Ichiro Hasuo is an Associate Professor at Department of Computer
Science, the University of Tokyo, Japan, and is the research director
of the JST ERATO "Metamathematics for Systems Design" Project. He
received PhD (cum laude) in Computer Science from Radboud University
Nijmegen, the Netherlands, in 2008 where he was affiliated with the
Security of Systems group and supervized by Prof.Dr. Bart Jacobs.
Before joining UTokyo he held an Assistant Professor position at
Research Institute for Mathematical Sciences (RIMS), Kyoto University,
Japan. His research interests include: mathematical (logical,
algebraic and categorical) structures in software science (esp. formal
methods); abstraction and generalization of deductive and
automata-theoretic verification techniques; and their application to
cyber-physical systems. He is a recipient of: Hiroshi Fujiwara
Encouragement Prize for Mathematical Sciences in 2012 (supported by
Mathematical Society of Japan); the best paper award at CONCUR 2014
(jointly with Natsuki Urabe); a JST PRESTO researchership; and a JST
ERATO project (three were granted in 2016 out of proposals from all
scientific fields).