Towards Logic-Based Verification of Java']JavaScript Programs

被引：1

作者：

Santos, Jose Fragoso ^{[1
]}

Gardner, Philippa ^{[1
]}

Maksimovic, Petar ^{[1
,2
]}

Naudziuniene, Daiva ^{[1
]}

机构：

[1] Imperial Coll London, London, England

[2] Serbian Acad Arts & Sci, Math Inst, Belgrade, Serbia

来源：

AUTOMATED DEDUCTION - CADE 26 | 2017年 / 10395卷

基金：

英国工程与自然科学研究理事会;

关键词：

D O I：

10.1007/978-3-319-63046-5_2

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe JaVerT, our semiautomatic toolchain for JavaScript verification.

引用

页码：8 / 25

页数：18

共 26 条

[1] Andreasen E, 2014, OOPSLA
[2] Berdine Josh, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P178, DOI 10.1007/978-3-642-22110-1_15
[3] Berdine J, 2006, LECT NOTES COMPUT SC, V4111, P115
[4] A Trusted Mechanised Java']JavaScript Specification
Bodin, Martin
Chargueraud, Arthur
Filaretti, Daniele
Gardner, Philippa
Maffeis, Sergio
Naudziuniene, Daiva
Schmitt, Alan
Smith, Gareth
[J]. ACM SIGPLAN NOTICES, 2014, 49 (01) : 87 - 100
[5] Cadar C., 2008, Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08, (USA), P209
[6] Calcagno C., 2009, POPL
[7] Moving Fast with Software Verification
Calcagno, Cristiano
Distefano, Dino
Dubreil, Jeremy
Gabi, Dominik
Hooimeijer, Pieter
Luca, Martino
O'Hearn, Peter
Papakonstantinou, Irene
Purbrick, Jim
Rodriguez, Dulma
[J]. NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 3 - 11
[8] Distefano D., 2008, OOPSLA
[9] ECMAScript Committee, 2011, TECHNICAL REPORT
[10] ECMAScript Committee, 2017, TEST262 TEST SUIT

← 1 2 3 →