8 citations · 8 across the 6 of their papers we have counts for
3 papers · 1 filter
SMT-Based Model Checking of Industrial Simulink Models
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki +3
The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes a…
Approximate Translation from Floating-Point to Real-Interval Arithmetic
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties ca…
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki
Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and contin…