フォーマルアプローチ特集　過去の論文募集と掲載論文

第8回特集（2013年6月号）

論文募集（和文）， 論文募集（英文）

掲載論文

第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
  

第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

第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

第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

第3回特集（2008年4月号）

論文募集

掲載論文

[セキュリティ]

• 実行履歴に基づくアクセス制御の形式モデルと検証
• Task-Structured PIOAフレームワークを用いた 適応的攻撃者に対するDiffie-Hellman鍵交換の安全性解析

[データベース]

• 書き換えに基づく最適化のためのXQueryの相対コストモデル

第2回特集（2007年4月号）

論文募集

掲載論文

[基礎理論]

• 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け
• XMLデータベースにおけるスキーマ進化のための更新操作群と それらのスキーマ表現能力保存に関する性質

[ソフトウェア]

• 制約指向に基づいたUMLモデルの不整合検出・解消手法の提案

第1回特集（2006年4月号）

論文募集

掲載論文

[計算モデル]

• ステータス付き再帰的経路順序による項書換え系多重完備化手続き
• π計算に対する時間拡張と合同的性質
• 時相論理の充足可能性判定器のための性能評価法

[ハードウェア]

• 状態遷移表現への変換に基づくハードウェア/ソフトウェア協調設計の形式的検証手法
• 高位仕様記述からの非同期式回路自動合成について
• モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法

[ソフトウェア]

• 時間制約を保証するUML/OCL を用いた分散実時間アプリケーション開発手法
• モデル生成法に基づくJavaScript プログラム型検査の機械実行
• XML文書に対するアクセシビリティ・ガイドライン適合性検証

[セキュリティ]

• 第三者機関を利用したワンタイムIDシステムの設計，および様相論理による安全性検証
• UMLによるプロテクションプロファイルのモデル化とその形式的検証