FORMAL PROGRAM VERIFICATION USING SYMBOLIC EXECUTION

被引:6
|
作者
DANNENBERG, RB [1 ]
ERNST, GW [1 ]
机构
[1] CASE WESTERN RESERVE UNIV, CASE INST TECHNOL, DEPT COMP ENGN & SCI, CLEVELAND, OH 44106 USA
关键词
D O I
10.1109/TSE.1982.234773
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
引用
收藏
页码:43 / 52
页数:10
相关论文
共 50 条
  • [1] Formal Verification of AUTOSAR Watchdog Manager Module Using Symbolic Execution
    Ahmed, Mazen
    Safar, Mona
    [J]. 2018 30TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS (ICM), 2018, : 240 - 243
  • [2] VERIFICATION OF PROTOCOLS USING SYMBOLIC EXECUTION
    BRAND, D
    JOYNER, WH
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1978, 2 (4-5): : 351 - 360
  • [3] PROGRAM VERIFICATION BY SYMBOLIC EXECUTION OF HYPERFINITE IDEAL MACHINES
    MORRIS, JM
    HOWARD, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 322 - 332
  • [4] TBFV-SE: Testing-Based Formal Verification with Symbolic Execution
    Wang, Rong
    Liu, Shaoying
    [J]. 2018 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2018), 2018, : 59 - 66
  • [5] Using dynamic symbolic execution to improve deductive verification
    Vanoverberghe, Dries
    Bjorner, Nikolaj
    de Halleux, Jonathan
    Schulte, Wolfram
    Tillmann, Nikolai
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2008, 5156 : 9 - 25
  • [6] Full contract verification for ATL using symbolic execution
    Bentley James Oakes
    Javier Troya
    Levi Lúcio
    Manuel Wimmer
    [J]. Software & Systems Modeling, 2018, 17 : 815 - 849
  • [7] USING SYMBOLIC EXECUTION FOR VERIFICATION OF ADA TASKING PROGRAMS
    DILLON, LK
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1990, 12 (04): : 643 - 669
  • [8] Interactive verification of concurrent systems using symbolic execution
    Baeumler, Simon
    Balser, Michael
    Nafz, Florian
    Reif, Wolfgang
    Schellhorn, Gerhard
    [J]. AI COMMUNICATIONS, 2010, 23 (2-3) : 285 - 307
  • [9] Full contract verification for ATL using symbolic execution
    Oakes, Bentley James
    Troya, Javier
    Lucio, Levi
    Wimmer, Manuel
    [J]. SOFTWARE AND SYSTEMS MODELING, 2018, 17 (03): : 815 - 849
  • [10] Branch Sequence Coverage Criterion for Testing-Based Formal Verification with Symbolic Execution
    Wang, Rong
    Liu, Shaoying
    [J]. 2019 COMPANION OF THE 19TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS-C 2019), 2019, : 205 - 212