10 citations · 23 across the 7 of their papers we have counts for
15 papers
Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
Tsutomu Kobayashi, Rick Salay, Ichiro Hasuo +3
Formal reasoning on the safety of controller systems interacting with plants is complex because developers need to specify behavior while taking into account perceptual uncertainty…
Architecture-Guided Test Resource Allocation Via Logic
Clovis Eberhart, Akihisa Yamada, Stefan Klikovits +4
We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree represe…
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +3
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with pri…
Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation
Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke +2
A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (proba…
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
Mayuko Kori, Ichiro Hasuo, Shin-ya Katsumata
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, w…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…