Verification of Multi-thread Programs via Linear Programming

• Project/Area Number: 20700019
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: TERAUCHI Tachio 東北大学, 大学院・情報科学研究科, 助教 (70447150)
• Project Period (FY): 2008 – 2010
• Project Status: Completed (Fiscal Year 2010)
• Budget Amount: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2010: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2009: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2008: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• Keywords: ソフトウェア検証 / プログラム言語 / 型推論 / 権限計算 / 線形計画法 / 型理論

Research Abstract

We propose a software verification framework based on the formalism of fractional capabilities thatstatically (i.e., at compile time) and automatically checksthatcertain bad things (e.g., data races) never happenin concurrent programs. The key to the success is the reduction of fractional capability calculito the problem of linear programming.

Research Products

• [Journal Article] On Bounding Problems of Quantitative Information Flow (2010)
  • Author(s): Hirotoshi Yasuoka and Tachio Terauchi
  • Journal Title: In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS 2010), Lecture Notes in Computer Science Volume: 6345, Springer Pages: 357-372
  • Peer Reviewed
• [Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities (2010)
  • Author(s): Hirotoshi Yasuoka and Tachio Terauchi
  • Journal Title: In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society Pages: 15-27
  • Peer Reviewed
• [Journal Article] Dependent Types from Counterexamples (2010)
  • Author(s): Tachio Terauchi
  • Journal Title: In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010) Volume: ACM Pages: 119-130
  • Peer Reviewed
• [Journal Article] On Bounding Problems of Quantitative Information Flow (2010)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 15^<th> European Symposium on Research in Computer Security (ESORICS 2010) Volume: 6345 Pages: 357-372
  • Peer Reviewed
• [Journal Article] Quantitative Information Flow-Verification Hardness and Possibilities (2010)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 23^<rd> IEEE Computer Security Foundations Symposium (CSF 2010) Pages: 15-27
  • Peer Reviewed
• [Journal Article] Dependent types from counterexamples (2010)
  • Author(s): Tachio Terauchi
  • Journal Title: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2010) 45 Pages: 119-130
  • Peer Reviewed
• [Journal Article] Polymorphic Fractional Capabilities (2009)
  • Author(s): Hirotoshi Yasuoka and Tachio Terauchi
  • Journal Title: In Proceedings of the 16th International Static Analysis Symposium (SAS 2009), Lecture Notes in Computer Science Volume: 5673, Springer Pages: 36-51
  • Peer Reviewed
• [Journal Article] Polymorphic Fractional Capabilities (2009)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Journal Title: Proceedings of the 16th International Static Analysis Symposium(SAS 2009) 5673 Pages: 36-51
  • Peer Reviewed
• [Journal Article] A Capability Calculus for Concurrency and Determinism (2008)
  • Author(s): Tachio Terauchi, Alex Aiken
  • Journal Title: ACM Transactions on Programming Languages and Systems (TOPLAS) Volume: 30(5)
  • Peer Reviewed
• [Journal Article] Witnessing Side Effects (2008)
  • Author(s): Tachio Terauchi, Alex Aiken
  • Journal Title: ACM Transactions on Programming Languages and Systems (TOPLAS) Volume: 30(3)
  • Peer Reviewed
• [Journal Article] A Type System for Observational Determinism (2008)
  • Author(s): Tachio Terauchi
  • Journal Title: In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), IEEE Computer Society Pages: 287-300
  • Peer Reviewed
• [Journal Article] Checking Race Freedom via Linear Programming (2008)
  • Author(s): Tachio Terauchi
  • Journal Title: In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008) Volume: ACM Pages: 1-10
  • Peer Reviewed
• [Journal Article] Inferring Channel Buffer Bounds via Linear Programming (2008)
  • Author(s): Tachio Terauchiand Adam Megacz
  • Journal Title: In Proceedings of the 17th European Symposium on Programming (ESOP 2008), Lecture Notes in Computer Science Volume: 4960, Springer Pages: 284-298
  • Peer Reviewed
• [Journal Article] Inferring Channel Buffer Bounds via Linear Programming (2008)
  • Author(s): Tachio Terauchi and Adam Megacz
  • Journal Title: Proceedings of the 17th European Symposium on Programming(ESOP 2008) 4960 Pages: 284-298
  • Peer Reviewed
• [Journal Article] Checking Race Freedom via Linear Programming (2008)
  • Author(s): Tachio Terauchi
  • Journal Title: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation(PLDI 2008) Pages: 1-10
  • Peer Reviewed
• [Journal Article] A Type System for Observational Determinism (2008)
  • Author(s): Tachio Terauchi
  • Journal Title: Proceedings of the 21st IEEE Computer Security Foundations Symposium(CSF 2008) Pages: 287-300
  • Peer Reviewed
• [Presentation] Polymorphic Fractional Capabilities (2010)
  • Author(s): 安岡宏俊、寺内多智弘
  • Organizer: JSSST第12回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 香川県琴平町
  • Year and Date: 2010-03-05
• [Presentation] Polymorphic Fractional Capabilities (2010)
  • Author(s): Hirotoshi Yasuoka, Tachio Terauchi
  • Organizer: 第12回プログラミングおよびプログラミング言語ワークショップ(PPL 2010)
  • Place of Presentation: 香川県琴平
  • Year and Date: 2010-03-05
• [Presentation] Dependent Types from Counterexamples (2010)
  • Author(s): 寺内多智弘
  • Organizer: JSSST第12回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 香川県琴平町
  • Year and Date: 2010-03-04
• [Presentation] Checking Race Freedom via Linear Programming (2008)
  • Author(s): 寺内多智弘
  • Organizer: JSSST第10回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 宮城県仙台市
  • Year and Date: 2008-03-06