Abe Tatsuya 安部達也

Researcher Number	50547388
Other IDs
Affiliation (Current)	2021: 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員
Affiliation (based on the past Project Information) *help	2015 – 2018: 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 2013 – 2014: 独立行政法人理化学研究所, 計算科学研究機構, 研究員
Review Section/Research Field	Principal Investigator High performance computing / Software
Keywords	Principal Investigator メモリ一貫性モデル / プログラム検証 / モデル検査 / プログラム論理 / PGAS言語 / 形式的体系 / ガベージコレクション / Non-multi-copy atomicity / IRIW / 定理証明 / 数理論理学

A unified theory of program verision with memory consistency models and its implementationsPrincipal Investigator
- Principal Investigator
  
  ABE Tatsuya
- Project Period (FY)
  2016 – 2018
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Software
  High performance computing
- Research Institution
  Chiba Institute of Technology
A Program Verification Theory of Memory Consistency Models on PGAS languages and its ImplementationPrincipal Investigator
- Principal Investigator
  
  Abe Tatsuya
- Project Period (FY)
  2013 – 2016
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  High performance computing
  Software
- Research Institution
  Chiba Institute of Technology
  The Institute of Physical and Chemical Research

All 2018 2017 2016 2015 2014 2013 Other

All Journal Article Presentation

[Journal Article] Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN2018
- Author(s)
  Kosuke Matsumoto, Tomoharu Ugawa, Tatsuya Abe
- Journal Title
  
  Journal of Information Processing
  
  Volume: 26 Issue: 0 Pages: 314-326
- DOI
  10.2197/ipsjjip.26.314
- NAID
  130006507556
- ISSN
  1882-6652
- Language
  English
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-16K00103, KAKENHI-PROJECT-16K21335
[Journal Article] Local Data Race Freedom with Non-Multi-Copy Atomicity2018
- Author(s)
  Tatsuya Abe
- Journal Title
  
  Proceedings of SPIN
  
  Volume: LNCS 10869
- DOI
  10.1007/978-3-319-94111-0_12
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K21335
[Journal Article] A verifier of directed acyclic graphs for model checking with memory consistency models2017
- Author(s)
  Tatsuya Abe
- Journal Title
  
  Proceedings of HVC
  
  Volume: 10629
- DOI
  10.1007/978-3-319-70389-3_4
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K21335
[Journal Article] Model checking copy phases of concurrent copying garbage collection with various memory models2017
- Author(s)
  Ugawa Tomoharu、Abe Tatsuya、Maeda Toshiyuki
- Journal Title
  
  Proceedings of the ACM on Programming Languages
  
  Volume: 1 Pages: 1-26
- DOI
  10.1145/3133877
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-16K00103, KAKENHI-PROJECT-16K21335
[Journal Article] Reordering control approaches to state explosion in model checking with memory consistency models2017
- Author(s)
  Tatsuya Abe, Tomoharu Ugawa, and Toshiyuki Maeda
- Journal Title
  
  Proceedings of VSTTE
  
  Volume: 10712
- DOI
  10.1007/978-3-319-72308-2_11
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K21335
[Journal Article] A general model checking framework for various memory consistency models2017
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Journal Title
  
  International Journal on Software Tools for Technology Transfer
  
  Volume: 印刷中
- DOI
  10.1007/s10009-016-0429-y
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25871113
[Journal Article] Concurrent Program Logic for Relaxed Memory Consistency Models with Dependencies across Loop Iterations2017
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Journal Title
  
  Journal of Information Processing
  
  Volume: 25 Issue: 0 Pages: 244-255
- DOI
  10.2197/ipsjjip.25.244
- NAID
  130005395246
- ISSN
  1882-6652
- Language
  English
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25871113, KAKENHI-PROJECT-16K21335
[Journal Article] Reducing state explosion for software model checking with relaxed memory consistency models2016
- Author(s)
  Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda, and Kousuke Matsumoto
- Journal Title
  
  Proceedings of the 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications
  
  Volume: LNCS 9984
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K21335
[Journal Article] メモリモデルを考慮したメモリアクセス命令を提供する SPIN 用ライブラリ2016
- Author(s)
  松元稿如、鵜川始陽、安部達也
- Journal Title
  
  第 23 回ソフトウェア工学の基礎ワークショップ
  
  Volume: なし
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K21335
[Journal Article] Reducing state explosion for software model checking with relaxed memory consistency models2016
- Author(s)
  Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda, and Kousuke Matsumoto
- Journal Title
  
  The 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications
  
  Volume: LNCS 9984
- DOI
  10.1007/978-3-319-47677-3_8
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-25871113
[Journal Article] Observation-based concurrent program logic for relaxed memory con- sistency models2016
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Journal Title
  
  Proceedings of the 14th Asian Symposium on Programming Languages and Systems
  
  Volume: LNCS 10017
- DOI
  10.1007/978-3-319-47958-3
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K21335
[Presentation] 並行プログラム論理の証明の導出に関する諸問題2018
- Author(s)
  安部達也
- Organizer
  第 35 回記号論理と情報科学
- Data Source
  KAKENHI-PROJECT-16K21335
[Presentation] 局所的データ非競合なプログラムの観測的同値2018
- Author(s)
  安部達也
- Organizer
  第 29 回代数,論理,幾何と情報科学研究集会
- Data Source
  KAKENHI-PROJECT-16K21335
[Presentation] メモリ一貫性モデルを考慮したモデル検査のためのプログラムグラフ検査器の Haskell 実装2017
- Author(s)
  安部達也
- Organizer
  ラムダ計算と論理の早春セミナー
- Place of Presentation
  草津セミナーハウス（群馬県吾妻郡）
- Year and Date
  2017-03-16
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] メモリ一貫性モデルを考慮したモデル検査のためのプログラムグラフ検査器の Haskell 実装2017
- Author(s)
  安部達也
- Organizer
  ラムダ計算と論理の早春セミナー
- Place of Presentation
  草津セミナーハウス（群馬県吾妻郡）
- Year and Date
  2017-03-16
- Data Source
  KAKENHI-PROJECT-16K21335
[Presentation] 並行プログラム論理における観測不変量2016
- Author(s)
  安部達也
- Organizer
  理論計算機科学と圏論ワークショップ 2016
- Place of Presentation
  理化学研究所（兵庫県神戸市）
- Year and Date
  2016-03-16
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] 並行ブログラム論理における表明の表現に関する考察2016
- Author(s)
  安部達也
- Organizer
  ラムダ計算と論理の早春セミナー
- Place of Presentation
  国立大学草津セミナーハウス（群馬県吾妻郡草津町）
- Year and Date
  2016-03-19
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] 命令のリオーダリングを許すモデル検査における反復的探索2016
- Author(s)
  安部達也
- Organizer
  第 33 回記号論理と情報科学
- Place of Presentation
  名古屋大学（愛知県名古屋市）
- Year and Date
  2016-08-25
- Data Source
  KAKENHI-PROJECT-16K21335
[Presentation] メモリ一貫性モデルを考慮したプログラムの中間表現2015
- Author(s)
  安部達也
- Organizer
  通研共同プロジェクト「メタプログラムに対する論理学的アプローチ」研究集会
- Place of Presentation
  東北大学（宮城県仙台市）
- Year and Date
  2015-09-28
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] Towards a unified verification theory for various memory consistency models2015
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Organizer
  The 6th Workshop on Syntax and Semantics of Low-Level Languages
- Place of Presentation
  京都大学（京都府京都市）
- Year and Date
  2015-07-05
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] 並行ブログラム論理におけるメモリ間の順序保存性のための公理2015
- Author(s)
  安部達也
- Organizer
  証明論 2015 ・第 32 回記号論理学と情報科学
- Place of Presentation
  南山大学（愛知県名古屋市）
- Year and Date
  2015-12-14
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] メモリ一貫性モデルを考慮したソフトウェアモデル検査のためのモデル検査器生成器 McSPIN2015
- Author(s)
  安部達也
- Organizer
  第 26 回代数,論理,幾何と情報科学研究集会
- Place of Presentation
  公立鳥取環境大学（鳥取県鳥取市）
- Year and Date
  2015-08-31
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] A general model checking framework for various memory consistency models2014
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Organizer
  The 19th Workshop on High-Level Parallel Programming Models and Supportive Environments
- Place of Presentation
  Phoenix, United States
- Year and Date
  2014-05-19
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] Model checking with user-definable memory consistency models2013
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Organizer
  The 7th Conference on Partitioned Global Address Space Programming Models
- Place of Presentation
  Edinburgh, United Kingdom
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] Model checking stencil computations written in a partitioned global address space language2013
- Author(s)
  Tatsuya Abe, Toshiyuki Maeda, and Mitsuhisa Sato
- Organizer
  The 18th Workshop on High-Level Parallel Programming Models and Supportive Environments
- Place of Presentation
  Cambridge, United States
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] メモリ一貫性モデルを考慮した半自動定理証明に向けて
- Author(s)
  安部達也
- Organizer
  第 25 回代数・論理・幾何と情報科学研究集会
- Place of Presentation
  横浜
- Year and Date
  2014-08-19 – 2014-08-20
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] 形式化されたメモリ一貫性モデルにおけるプログラム検証
- Author(s)
  安部達也
- Organizer
  第 31 回記号論理学と情報科学
- Place of Presentation
  東京
- Year and Date
  2014-05-26 – 2014-05-28
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] メモリ一貫性モデルのための合成的な並行プログラム論理
- Author(s)
  安部達也
- Organizer
  理論計算機科学と圏論ワークショップ
- Place of Presentation
  鹿児島
- Year and Date
  2015-03-14 – 2015-03-15
- Data Source
  KAKENHI-PROJECT-25871113
[Presentation] Optimization of a general model checking framework for various memory consistency models
- Author(s)
  Tatsuya Abe and Toshiyuki Maeda
- Organizer
  The 8th Conference on Partitioned Global Address Space Programming Models
- Place of Presentation
  Eugene, United States
- Year and Date
  2014-10-07 – 2014-10-10
- Data Source
  KAKENHI-PROJECT-25871113

1. UGAWA Tomoharu

# of Collaborated Projects: 0 results

# of Collaborated Products: 2 results

Abe Tatsuya 安部 達也

Research Projects

Research Products

Co-Researchers

A unified theory of program verision with memory consistency models and its implementationsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

A Program Verification Theory of Memory Consistency Models on PGAS languages and its ImplementationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Journal Article] Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN2018

Author(s)

Journal Title

DOI

NAID

ISSN

Language

Data Source

[Journal Article] Local Data Race Freedom with Non-Multi-Copy Atomicity2018

Author(s)

Journal Title

DOI

Data Source

[Journal Article] A verifier of directed acyclic graphs for model checking with memory consistency models2017

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Model checking copy phases of concurrent copying garbage collection with various memory models2017

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Reordering control approaches to state explosion in model checking with memory consistency models2017

Author(s)

Journal Title

DOI

Data Source

[Journal Article] A general model checking framework for various memory consistency models2017

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Concurrent Program Logic for Relaxed Memory Consistency Models with Dependencies across Loop Iterations2017

Author(s)

Journal Title

DOI

NAID

ISSN

Language

Data Source

[Journal Article] Reducing state explosion for software model checking with relaxed memory consistency models2016

Author(s)

Journal Title

Data Source

[Journal Article] メモリモデルを考慮したメモリアクセス命令を提供する SPIN 用ライ ブラリ2016

Author(s)

Journal Title

Data Source

[Journal Article] Reducing state explosion for software model checking with relaxed memory consistency models2016

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Observation-based concurrent program logic for relaxed memory con- sistency models2016

Author(s)

Journal Title

DOI

Data Source

[Presentation] 並行プログラム論理の証明の導出に関する諸問題2018

Author(s)

Organizer

Data Source

[Presentation] 局所的データ非競合なプログラムの観測的同値2018

Abe Tatsuya 安部達也

[Journal Article] メモリモデルを考慮したメモリアクセス命令を提供する SPIN 用ライブラリ2016

[Presentation] メモリ一貫性モデルを考慮したモデル検査のためのプログラムグラフ検査器の Haskell 実装2017

[Presentation] メモリ一貫性モデルを考慮したモデル検査のためのプログラムグラフ検査器の Haskell 実装2017