A grand challenge proposal for formal methods: A verified stack

被引:0
|
作者
Moore, JS [1 ]
机构
[1] Univ Texas, Dept Comp Sci, Austin, TX 78712 USA
关键词
hardware verification; software verification; simulation; modeling; theorem proving; model checking;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We propose a grand challenge for the formal methods community: build and mechanically verify a practical computing system, from transistors to software. The challenge is both competitive and collaborative. It is collaborative because practical systems are too large for any one group or tool to handle in isolation: groups will have to team together. Furthermore, the vertical integration of systems at different levels of abstractions - from transistors to software - will encourage the team to adopt different tools for different levels and connect them. It is competitive because there are many systems from which to choose and different teams may form around different target systems.
引用
收藏
页码:161 / 172
页数:12
相关论文
共 50 条
  • [1] Verified software grand challenge
    Woodcock, Jim
    [J]. FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 617 - 617
  • [2] Verified software: A grand challenge
    Jones, C
    O'Hearn, P
    Woodcock, J
    [J]. COMPUTER, 2006, 39 (04) : 93 - 95
  • [3] Verified Software:: The real grand challenge
    Bharadwaj, Ramesh
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 318 - 324
  • [4] First steps in the Verified Software Grand Challenge
    Woodcock, Jim
    [J]. COMPUTER, 2006, 39 (10) : 57 - +
  • [5] First steps in the verified software grand challenge
    Woodcock, Jim
    [J]. 30th Annual IEEE/NASA Software Engineering Workshop, Proceedings, 2006, : 203 - 203
  • [6] Accessible Formal Methods for Verified Parser Development
    Li, Letitia W.
    Eakman, Greg
    Garcia, Elias J. M.
    Atman, Sam
    [J]. 2021 IEEE SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (SPW 2021), 2021, : 142 - 151
  • [7] Verified software: Theories, tools, experiments vision of a grand challenge project
    Hoare, Tony
    Misra, Jay
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 1 - 18
  • [8] Routing - A challenge to formal methods
    Reed, JN
    Sinclair, JE
    Reed, GM
    [J]. INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, : 305 - 311
  • [9] The 2016 Formal Methods for Robotics Challenge
    Raman, Vasumathi
    [J]. IEEE ROBOTICS & AUTOMATION MAGAZINE, 2016, 23 (03) : 24 - 25
  • [10] A Formally Verified NAT Stack
    Pirelli, Solal
    Zaostrovnykh, Arseniy
    Candea, George
    [J]. ACM SIGCOMM COMPUTER COMMUNICATION REVIEW, 2018, 48 (05) : 77 - 83