Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
MSS, NLP (Joint) |
2020-03-09 17:50 |
Aichi |
(Cancelled but technical report was issued) |
Formalization of Modalities in Fillmore's Case Grammar for Language Characterization. Shuji Harazoe (Yamaguchi Univ.), Ren Wu (Yamaguchi JC.), Hiroshi Matsuno (Yamaguchi Univ.) MSS2019-61 |
Modality is a grammatical category that expresses a speaker's will and attitude, which is an essential element of langua... [more] |
MSS2019-61 pp.19-24 |
SS |
2019-03-04 17:10 |
Okinawa |
|
Formal STAMP Modelling toward Safety Verification of Hybrid Systems Mitsuaki Tsuji, Toshinori Takai (NAIST), Masafumi Katahira, Naoki Ishihama (JAXA), Kazuki Kakimoto, Hajimu Iida (NAIST) SS2018-67 |
Safety-critical systems, for example, autonomous vehicles and space systems, are required to be safe and reliable. Recen... [more] |
SS2018-67 pp.91-96 |
MSS, SS |
2017-01-27 10:40 |
Kyoto |
Kyoto Institute of Technology |
Formal Description of a Processing as a Mapping between different sorts of Representations, Considering state-transition Fumiko Kouda (Utokyo) MSS2016-70 SS2016-49 |
We propose a new computing processing model, as a mapping of
representation-translation, considering their semantics, ... [more] |
MSS2016-70 SS2016-49 pp.77-82 |
MSS, CAS, IPSJ-AL [detail] |
2016-11-25 12:55 |
Hyogo |
Kobe Institute of Computing |
Formal Description of Synchronization by Functional Definition of Synchronous Circuits Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) CAS2016-73 MSS2016-53 |
Synchronous circuits are usually defined as D-Flipflop (D-FF) synchronized circuits, but it is doubtful that D-FF comple... [more] |
CAS2016-73 MSS2016-53 pp.99-104 |
VLD, DC, IPSJ-SLDM, CPSY, RECONF, ICD, CPM (Joint) [detail] |
2014-11-26 10:45 |
Oita |
B-ConPlaza |
A hardware description method and sematics providing a timing constrant Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) VLD2014-82 DC2014-36 |
Formal verification methods are wide-spreading due to its mathmatical rigorousaspect, although they limited to synchroun... [more] |
VLD2014-82 DC2014-36 pp.81-86 |
VLD |
2014-03-05 15:45 |
Okinawa |
Okinawa Seinen Kaikan |
A Case Study of Symbolic Model Checking for Verilog-HDL Hardware Design Tomoyuki Yokogawa, Daichi Higashiyama (Okayama Pref. Univ.), Masafumi Kondo (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Pref. Univ.) VLD2013-166 |
In this paper, we show a case study where a design of 8bit microcomputer M8R, which is described by Verilog-HDL, is veri... [more] |
VLD2013-166 pp.177-182 |
ET |
2012-11-17 11:15 |
Saga |
|
Content development for distance education for advanced university mathematics by Mizar Takaya Ido, Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama (Shinshu Univ) ET2012-55 |
Mizar project describes the formalization and proof of the current theorem using mathematical for-
malization descripti... [more] |
ET2012-55 pp.13-17 |
SS |
2011-10-28 11:15 |
Ishikawa |
JAIST |
Iterative Construction of Finite Alloy Descriptions Kei Kogai (Ibaraki National College of Technology), Shin Nakajima (NII), Yoshikazu Ueda (Ibaraki Univ.) SS2011-36 |
In a process of creating Alloy descriptions, it is often to analyze the descriptions by scoped Alloy commands. The comma... [more] |
SS2011-36 pp.55-60 |
MSS |
2010-08-02 14:25 |
Ishikawa |
|
Generating test cases for implementing concurrent systems based on the OTS/CafeOBJ method Takahiro Seino (AIST), Masaki Nakamura (Kanazawa Univ.) CST2010-33 |
In software developments with formal methods, there exists an unavoidable gap between a system description in formal spe... [more] |
CST2010-33 pp.7-12 |
KBSE, SS |
2010-05-28 16:00 |
Kyoto |
Doshisha University, Imadegawa Campus |
Fundamental Program Structure Patterns of Recursive Programs Masanori Ohdan (Shiname Univ./NST), Tadamasa Satou SS2010-15 KBSE2010-15 |
It requires programming aids to improve the understandability for recursive programs that are not easy to follow the log... [more] |
SS2010-15 KBSE2010-15 pp.87-91 |
COMP |
2010-04-22 15:10 |
Shiga |
Ritusmeikan University, Biwako-Kusatsu Campus |
Elementary Formal System with Nonterminal Symbols Tomohiko Koide, Ayumi Shinohara (Tohoku Univ.) COMP2010-7 |
Elementary Formal Systems (EFS) are logic programs over strings, and
they are useful to describe various language class... [more] |
COMP2010-7 pp.47-54 |
SS |
2009-08-06 10:30 |
Hokkaido |
Kitami Institute of Technology |
A Structure Analysis Method for Programs with Recursive Calls Masanori Ohdan (Shimane Univ.), Tadamasa Satou SS2009-12 |
The recursive structure is one of the programming concept hand to master. It provides compact and neat programs, while i... [more] |
SS2009-12 pp.1-6 |
SS |
2008-12-19 11:15 |
Kochi |
Kochi Univiersity of Technology |
XML Processing Techniqes Based on Tree Automata Yoshiaki Takata (Kochi Univ. of Tech.), Hiroyuki Seki (Nara Inst. of Scei and Tech.) SS2008-46 |
Tree automata, which are finite automata over trees, have been investigated in various research areas for a long time. ... [more] |
SS2008-46 pp.43-50 |
VLD, DC, IPSJ-SLDM, CPSY, RECONF, ICD, CPM (Joint) [detail] |
2008-11-18 13:00 |
Fukuoka |
Kitakyushu Science and Research Park |
Improving the Accuracy of Rule-based Equivalence Checking of High-level Desciptions by Identifying Potential Internal Equivalences Hiroaki Yoshida, Masahiro Fujita (Univ. of Tokyo) |
Rule-based equivalence checking of high-level design descriptions proves the equivalence of two high-level design descri... [more] |
VLD2008-78 DC2008-46 pp.109-114 |
SS |
2007-06-22 11:45 |
Ishikawa |
JAIST |
Formal Description and Verification of Domains Yasuhito Arimoto, Kokichi Futatsugi (JAIST) SS2007-15 |
In this paper, we propose a methodology for describing formal domain descriptions and verifying them by
using OTS/Cafe... [more] |
SS2007-15 pp.35-40 |
ET |
2006-09-16 14:30 |
Osaka |
|
Practice and Evaluation of Portfolio Assessment Support System Yasuhiko Morimoto, Isao Kikukawa (Fuji Tokoha Univ.), Maomi Ueno (UEC), Setsuo Yokoyama, Youzou Miyadera (Tokyo Gakugei Univ.) |
Portfolio assessment that used electronic portfolios has attracted as a more authentic means of evaluating learning dire... [more] |
ET2006-42 pp.35-40 |
ET |
2006-01-28 11:25 |
Tokyo |
|
SCORM Extension for Describing Learning State Transitions Based on Learner's Actions Yasuhiko Morimoto (Fuji Tokoha Univ.), Maomi Ueno (Nagaoka Univ. of Technology), Shingo Shibata (COMPAC, Ltd.), Setsuo Yokoyama, Youzou Miyadera (Tokyo Gakugei Univ.) |
SCORM is an international set of standards that describes learning content of WBT. SCORM cannot describe learning state ... [more] |
ET2005-78 pp.25-30 |
SS |
2005-12-20 14:00 |
Kochi |
Kochi Women's University |
A Layered Architecture of Formal Specification Xiaojing Zhang, Yoichi Omori, Keijiro Araki (Kyushu Univ.) |
Software productline extracts similarities of a series of products, thus a specification of a product can be applied to ... [more] |
SS2005-70 pp.43-48 |
SIP, ICD, IE, IPSJ-SLDM |
2005-10-21 15:30 |
Miyagi |
Ichinobo, Sakunami-Spa |
A Monitor Generation Method for Formal Monitor-based Verification Considering Input Constraints Yosuke Kakiuchi (Osaka Univ.), Akira Kitajima (Osaka Electro-Communication Univ.), Kiyoharu Hamaguchi, Toshinobu Kashiwabara (Osaka Univ.) |
In order to verify hardware module interfaces, various verification methods have been proposed. This paper focuses on fo... [more] |
SIP2005-127 ICD2005-146 IE2005-91 pp.73-78 |
ET |
2005-10-15 16:10 |
Hiroshima |
|
Proposal of a Formal Description Method for Portfolio Assessment Support Systems Yasuhiko Morimoto (Fuji Tokoha Univ.), Isao Kikukawa (Tokyo Polytecnic Univ.), Maomi Ueno (Nagaoka Univ. of Technology), Setsuo Yokoyama, Youzou Miyadera (Tokyo Gakugei Univ.) |
Portfolio assessment is receiving increasing attention as the ideal method of educational evaluation for teachers making... [more] |
ET2005-49 pp.63-68 |