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

共 50 条

[31] An Analysis of the Dynamic Behavior of Java']JavaScript Programs
Richards, Gregor
Lebresne, Sylvain
Burg, Brian
Vitek, Jan
ACM SIGPLAN NOTICES, 2010, 45 (06) : 1 - 12
[32] Verification of Java']Java programs with generics
Stenzel, Kurt
Grandy, Holger
Reif, Wolfgang
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2008, 5140 : 315 - 329
[33] A declarative enhancement of Java']JavaScript programs by leveraging the Java']Java metadata infrastructure
Wang, Yuchen
Cheng, Kwok Sun
Song, Myoungkyu
Tilevich, Eli
SCIENCE OF COMPUTER PROGRAMMING, 2019, 181 : 27 - 46
[34] Compliance verification of agent interaction: A logic-based software tool
Alberti, M
Gavanelli, M
Lamma, E
Chesani, F
Mello, P
Torroni, P
APPLIED ARTIFICIAL INTELLIGENCE, 2006, 20 (2-4) : 133 - 157
[35] Separating Map Variables in a Logic-Based Intermediate Verification Language
Dietsch, Daniel
Heizmann, Matthias
Hoenicke, Jochen
Nutz, Alexander
Podelski, Andreas
NETWORKED SYSTEMS, NETYS 2021, 2021, 12754 : 169 - 186
[36] HEngineering Hoare Logic-based Program Verification in K Framework
Arusoaie, Andrei
2013 15TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2013), 2014, : 177 - 184
[37] Compliance verification of agent interaction: A logic-based software tool
Alberti, Marco
Gavanelli, Marco
Lamma, Evelina
Chesani, Federico
Mello, Paola
Torroni, Paolo
Appl Artif Intell, 1600, 2-4 (133-157):
[38] SPECIFICATION AND VERIFICATION OF AGENT INTERACTION PROTOCOLS IN A LOGIC-BASED SYSTEM
Alberti, Marco
Chesani, Federico
Daolio, Davide
Gavanelli, Marco
Lamma, Evelina
Mello, Paola
Torroni, Paolo
SCALABLE COMPUTING-PRACTICE AND EXPERIENCE, 2007, 8 (01): : 1 - 13
[39] Dynamic Frames Based Verification Method for Concurrent Java']Java Programs
Mostowski, Wojciech
VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 124 - 141
[40] Constraint-based synchronization and verification of distributed Java']Java programs
Ramirez, R
Martinez, J
LOGIC PROGRAMMING, PROCEEDINGS, 2004, 3132 : 473 - 474

← 1 2 3 4 5 →