フォーマルアプローチ特集 過去の掲載論文
第1回掲載論文（2006年4月号）
[計算モデル]
ステータス付き再帰的経路順序による項書換え系多重完備化手続き
π計算に対する時間拡張と合同的性質
時相論理の充足可能性判定器のための性能評価法
[ソフトウェア]
時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法
モデル生成法に基づくJavaScriptプログラム型検査の機械実行
XML文書に対するアクセシビリティ・ガイドライン適合性検証
[セキュリティ]
第三者機関を利用したワンタイムIDシステムの設計，および様相論理による安全性検証
UMLによるプロテクションプロファイルのモデル化とその形式的検証
第2回掲載論文（2007年4月号）
[基礎理論]
単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け
XMLデータベースにおけるスキーマ進化のための更新操作群とそれらのスキーマ表現能力保存に関する性質
[ソフトウェア]
制約指向に基づいたUMLモデルの不整合検出・解消手法の提案
第3回掲載論文（2008年4月号）
[セキュリティ]
実行履歴に基づくアクセス制御の形式モデルと検証
Task-Structured PIOAフレームワークを用いた適応的攻撃者に対するDiffie-Hellman鍵交換の安全性解析
[データベース]
書き換えに基づく最適化のためのXQueryの相対コストモデル
第4回掲載論文・和文（2009年5月号）
[モデル検査]
【招待論文】時間オートマトンのモデル検査
[セキュリティ]
【招待論文】汎用的結合可能性による暗号システムの安全性証明
記号論的暗号解析を用いた Oblivious Transfer プロトコルの解析
第4回掲載論文・英文（2009年5月号）
[Hardware verification]
Word-level equivalence checking in bit-level accuracy with identical datapath
A unified framework for equivalence verification of datapath oriented applications
[Foundation]
Pre- and post-conditions expressed in variants of the modal mu-calculus
[Model checking]
Probabilistic model checking of the one-dimensional ising model
[Software testing]
Generating test cases from proof scores in the OTS/CafeOBJ method
[Security]
Comparison of the expressive power of language-based access control models
Verification of the security against inference attacks on XML databases
第5回掲載論文（2010年5月号）
[Term rewriting systems]
Multi-context rewriting induction with termination checkers
Decidability of termination and innermost termination for term rewriting systems with right-shallow dependency pairs
[Program transformation]
Program transformation templates for tupling based on term rewriting
[Formal Specification]
Towards reliable e-government systems with the OTS/CafeOBJ method
[Program Analysis]
Over-approximated control flow graph construction on pure Esterel
[Model Checking]
An abstraction refinement technique for timed automata based on counterexample-guided abstraction refinement loop
[Software Testing]
Computer algebra system as test generation system
第6回掲載論文（2011年5月号）
[Model Checking]
An SMT-based Approach to Bounded Model Checking of Designs in State Transition Matrix
Probabilistic Symmetry Reduction for a System with Ring Buffer
[System Analysis]
QoS Analysis of Real-time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Techniques
and Simulation
[Specification Translation]
Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
[Software Development Methodology]
Modeling, Verification and Testing of Web Applications Using Model Checker
第7回掲載論文（2012年5月号）
[Formal Methods]
Formal Verification of Effectiveness of Control Activities in Business Processes
Refactoring Problem of Acyclic Extended Free Choice Workflow Nets to Acyclic Well-Structured Workflow Nets
[Model Checking]
Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras
[Database Security]
Decidability of the Security against Inference Attacks using a Functional Dependency on XML Databases
[System Analysis]
Stochastic Power Minimization of Real-Time Tasks with Probabilistic Computations under Discrete Clock Frequencies
第8回掲載論文（2013年6月号）
An Algorithm for Allocating User Requests to Licenses in the OMA DRM System
Deciding Schema k-Secrecy for XML Databases
More Precise Analysis of Dynamically Generated String Expressions in Web Applications with Input Validation
第9回掲載論文（2014年6月号）
[Formal Verification]
Bisimilarity Control of Nondeterministic Discrete Event Systems under Event and State Observations
A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System
TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
[Formal Construction]
An Approach for Synthesizing Intelligible State Machine Models from Choreography Using Petri Nets
Protocol Inheritance Preserving Soundizability Problem and Its Polynomial Time Procedure for Acyclic Free Choice Workflow Nets
第10回掲載論文（2015年6月号）