Title: Model checking event clock automata (Mizuhito Ogawa)
Abstract: Model checking event clock automata has been an open problem, even for discrete CTL. The difficulty lies the failure of the finite region construction for event clock automata, contrary to what widely believed, We investigate how the well quasi ordering techniques work for the problem.
Title: Reaching to the Top of the Tower (Yuxi Fu)
Abstract: We will talk about a new complexity upper bound (much better than the one you heard me talking about last time in Japan) on the VASS reachability problem.
Title: Regularity Preservation Property of Register Pushdown Systems (Hiroyuki Seki)
Abstract: Pushdown system (PDS) is an infinite-state model for recursive schema and
PDS preserves regularity, where a transformation T is said to preserve regularity
if T(L) is always regular for any regular language L.
Register pushdown system (RPDS) is an extension of PDS by adding the capability
of manipulating data values in a restricted way. Murawski et al. showed that
every RPDS has backward (pre*) regularity preservation property. Note that
we say that a data language L is regular if L is recognized by a register automaton.
In this talk, we first propose an alternative definition of RPDS by using equivalence
relation between registers. Then, it is shown that every RPDS has both backward
and forward (post*) regularity preservation property. Also, we discuss an application
of these preservation results to RPDS model checking problems.
This is a joint work with Ryoma Senda and Yoshiaki Takata.
Title: Synthesizing Simple Strategies for Efficient Counterexample-Guided Quantified SMT Solving (Tachio Terauchi)
Abstract: We present a new algorithm for deciding the satisfiability of SMT formulas containing quantifiers. We build our algorithm on the recent approach proposed by Farzan and Kincaid that reduces the problem to synthesizing a winning strategy to a certain perfect-information two-player game. We show that their approach (as well as similar approaches used in Z3 and CVC4) can be inefficient incurring exponentially many strategy synthesis iterations even on simple examples having linear-size winning strategies. Then, we present a new strategy synthesis approach that is able to efficiently solve such instances by quickly converging to simple winning strategies. (This is a work-in-progress work.)
Title: Proof normalization for classical truth-table natural deduction (Koji Nakazawa)
Abstract: Geuvers et al. proposed a framework in which we can induce
natural-deduction-style
inference rules for general logical connectives from their truth
tables. They also defined
the proof normalization for intuitionistic variant of the truth-table
natural deduction (TTND)
and van der Giessen proved the subformula property and the strong
normalization, which are
important properties deriving consistency and conservativeness.
However, for Geuvers'
original definition of classical variant of TTND, it seems hard to
define the proof normalization
with good properties. In this talk, we proposed another classical
variant of TTND, which is an
extension of the intuitionistic TTND with multiple conclusion
sequents, and in which we can
easily get the notion of proof normalization along the idea of
Parigot's lambda-mu calculus.
We also prove the subformula property and strong normalization of the
proof normalization
in classical TTND.
This is a joint work with Kosuke Fukui and Saori Ishii.
Title: Verifying Quantum Communication Protocols with Ground Bisimulation (Xudong Qin)
Abstract: One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.
Title: Reversing Parallel Programs with Blocks and Procedures (Shoji Yuen)
Abstract: We show how to reverse a while language extended with blocks, local variables, procedures and the
interleaving parallel composition. Annotation is defined along with a set of operational semantics
capable of storing necessary reversal information, and identifiers are introduced to capture the interleaving
order of an execution. Inversion is defined with a set of operational semantics that use
saved information to undo an execution. We prove that annotation does not alter the behaviour of the
original program, and that inversion correctly restores the initial program state.
(Joint work with: James Hoey and Irek Ulidowski)
Title: Formal Verification of Software Countermeasures (Fu Song)
Abstract: Cryptographic algorithms are widely used to protect data privacy in many aspects of our daily lives from smart card to cyber-physical systems. Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks, which infer private data via statistical analysis of the correlation between power consumptions of an electronic device and private data. To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, programs that rely on secure masking schemes are not secure a priori. Indeed, designing effective masking programs is a labor intensive and error-prone task. Although some techniques have been proposed for formally verifying masking countermeasures and for quantifying masking strength, they are currently limited to Boolean programs and suffer from low accuracy.
In this talk, I will present our recent results on formal verification of cryptographic programs against power side-channel attacks. First, I will talk about a refinement based qualitative verification approach that can be viewed as a synergistic integration of a rule-based approach for inferring distribution types and an model-counting based approach for refining these types. Second, I will present an algorithm for quantifying the amount of side-channel information leakage from a software implementation using the notion of quantitative masking strength. Finally, I will discuss some open problems for future work.
Title: Accelerating Robustness Verification of Image Classification Neural Networks Guided by Spurious Adversarial Label (Min Zhang)
Abstract: Neural networks (NNs) for image classification have become key components of many safety-critical applications such as autonomous driving, medical diagnosis, and so on. Their safety must be guaranteed in that they must produce safe results for any inputs. Most existing safety verification approaches of NNs either struggle to scale beyond small networks or suffer from high precision loss for deeper networks. In this talk, we will present a novel approach to accelerate the safety verification of NNs against adversarial perturbations by integrating symbolic constraints propagation technique, linear relaxation method and spurious adversarial label strategy. We implement our approach as part of a prototype called VeriFast, used for safety verification of ReLU-based NNs. Evaluation results show that VeriFast can find exact minimum distortions similar to state-of-the-art solver-based tools such as MIPVerify for small networks; and achieves up to 190× efficiency. It also shows that our system is scalable to large MNIST networks (e.g., 9 layers with 9,000 neurons in total), which the solver-based systems fail to verify.
This is joint work with Fei Gao, Frederic Mallet and Mingsong Chen
Title: Fully Static Multiparty Session Programming with Global
Protocol Combinators
(Keigo Imai)
Abstract: Multiparty Session Types (MPST) is a typing discipline for
communication protocols. It ensures the absence of communication
errors and deadlocks for well-typed communicating processes. Current
implementations of the MPST theory rely on (1) runtime linearity
checks to ensure correct usage of communication channels and (2)
external domain specific languages for specifying and verifying of
multiparty protocols.
To overcome these limitations, we propose a library for programming
with global combinators -- a set of functions for writing and
verifying multiparty protocols in OCaml. Local behaviours for all
processes in a protocol are inferred at once from a global combinator.
We formalise our implementation in MiO, a minimal session-based
functional language, and prove that MiO is type-safe. Our approach
enables fully-static verification and implementation of the whole
protocol, from the protocol specification to the process
implementations, to happen in the same language.
We compare our implementation to untyped and continuation-passing
style implementations, and demonstrate its expressiveness by
implementing a plethora of protocols. We show our library can
interoperate with existing libraries and services, implementing DNS
(Domain Name Service) protocol and the OAuth (Open Authentication)
protocol.
This is joint work with Rumyana Neykova (Brunel University London, UK)
and Nobuko Yoshida (Imperial College London, UK).
Title: Proof Script Generation from Proof Scores
(Kazuhiro Ogata)
Abstract: CafeOBJ is an algebraic specification language and
processor. Various kinds of systems, such as security protocols,
have been formally specified in CafeOBJ and formally verified by
writing proof scores in CafeOBJ. Proof scores are proof plans
manually written by human users and subject to human errors in
that human users may overlook some cases, which CafeOBJ does not
take care of. The 1st implementation of CafeOBJ is done in Common
Lisp. There is the 2nd implementation called CafeInMaude on top
of Maude, which is a sibling language of CafeOBJ. CafeInMaude has
a proof assistant called CafeInMaude Proof Assistant (CiMPA) and
a proof generator called CafeInMaude Proof
Generator (CiMPG). Given proof scores written in CafeOBJ, CiMPG
automatically generates proof scripts that can be fed into
CiMPA. If the generated proof scripts can be discharged by CiMPA,
the proof scores are correct. Thus, CiMPG can check if proof
scores are correct. An example is used to describe how to write
systems specifications in CafeOBJ, how to write proof scores in
CafeOBJ and how to use CiMPA and CiMPG.
Title: Łoś and Tarski meet Lovász (Yijia Chen)
Abstract: The Łoś–Tarski preservation theorem states that any FO-definable property which is closed under induced substructures can be defined by a universal FO-sentence. We show that this theorem can give a pure logic proof of the following result due to Lovász.
For every constant k, there exists a finite sequence of graphs H_1, \ldots, H_{m_k} such that for any graph G
G has a vertex cover of size at most k iff no H_i is an (induced) subgraph of G.
This might be surprising since
1. the Łoś–Tarski preservation theorem famously fails on finite structures, hence fails on graphs,
2. Lovász's result (and also his proof) is purely combinatorial.
Our key observation is that the above graph-theoretic problem can be easily generalized to infinite graphs. I will explain a few other results we've obtained using such a strategy. Among others, we apply Craig's interpolation theorem to show the collapse of monadic second-order logic to FO on graphs of bounded shrub-depth.
This is joint work with Jörg Flum.
Title: Formal Verification of Probabilistic Programs: Termination, Cost Analysis and Sensitivity (Hongfei Fu)
Abstract: Formal verification is the study to ensure correctness of systems through rigorous mathematical approaches.
Probabilistic programs are classical programs extended with random number generators that
capture a large class of application scenarios with probability, such as artificial intelligence, random walks,
randomized algorithms, stochastic systems, etc.
Formal verification of probabilistic programs aims at developing methodologies that can prove correctness
of fundamental probabilistic properties such as termination with probability one, expected resource consumption, and
expected sensitivity against slight perturbation of inputs, etc.
In the talk, I will introduce our theoretical results on verifying termination, cost and sensitivity of probabilistic programs.