检索结果-内蒙古大学图书馆

Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing

作者： Aleksandar S. Dimovski Mother Teresa University Skopje Skopje Macedonia

ISBN: (纸本)9798400706295

game semantics provides fully abstract (sound and complete) models for open program fragments with undefined, non-local, identifiers (e.g. library functions). This is achieved by using the "most general" models for undefined identifiers, i.e. the most generic context in which the program fragment will be inserted. Given a safety property as an assertion, we want to find the most permissive models of undefined identifiers, i.e. the weakest safe context, that are sufficient to ensure safety of the given program *** solve this problem, we present a novel approach that uses symbolic game semantic models of open program fragments and logical abduction. By using symbolic values instead of concrete ones for integers, we represent algorithmic game semantics of program fragments with unbounded integers as finite-state symbolic automata that are amenable for automatic reasoning. Then, we reduce the problem of inferring minimal assumptions on the behaviors of undefined identifiers in order to prove safety of the given program fragment to a logical abduction task. We evaluate our approach and demonstrate its practicality via several examples.

关键词： algorithmic game semantics

来源：评论

学校读者我要写书评

暂无评论

Program verification using symbolic game semantics

引用

THEORETICAL COMPUTER SCIENCE 2014年第Part3期560卷 364-379页

作者： Dimovski, Aleksandar S. FON Univ Fac Informat Commun Tech Skopje 1000 North Macedonia

We introduce a new symbolic representation of algorithmic game semantics, and show how it can be applied for efficient verification of open (incomplete) programs. The focus is on an Algol-like programming language which contains the core ingredients of imperative and functional languages, especially on its second-order recursion-free fragment with infinite data types. We revisit the regular-language representation of game semantics of this language fragment. By using symbolic values instead of concrete ones, we generalize the standard notions of regular-language and automata representations of game semantics to those of corresponding symbolic representations. In this way programs with infinite data types, such as integers, can be expressed as finite-state symbolic-automata although the standard automata representation is infinite-state, i.e. the standard regular-language representation has infinite summations. Moreover, in this way significant reductions of the state space of game semantics models are obtained. This enables efficient verification of programs by our prototype tool based on symbolic game models, which is illustrated with several examples. (C) 2014 Elsevier B.V. All rights reserved.

关键词： algorithmic game semantics Symbolic automata Program verification Predicate abstraction

来源：评论

学校读者我要写书评

暂无评论

Verifying annotated program families using symbolic game semantics

引用

THEORETICAL COMPUTER SCIENCE 2018年 706卷 35-53页

作者： Dimovski, Aleksandar S. IT Univ Copenhagen Copenhagen Denmark

Many software systems are today built as program families. They permit users to derive a custom program (variant) by selecting suitable configuration options at compile time according to their requirements. Many such program families are safety critical. However, most existing verification techniques are designed to work on the level of single programs. Their application to program families would require to verify each variant in isolation, in a brute force fashion. This approach does not scale in practice due to the (potentially) huge number of possible variants. In this paper, we propose an efficient game semantics based approach for verification of open program families, i.e. program families with undefined components (identifiers). We use symbolic representation of algorithmic game semantics, where symbolic values for inputs are used instead of concrete ones. In this way, we can compactly represent program families with infinite integers as so-called (finite state) featured symbolic automata. Specifically designed model checking algorithms are then employed to uniformly verify safety of all programs (variants) from a family at once using a single compact model and to pinpoint those programs that are unsafe (respectively, safe). We present a prototype tool implementing this approach, and we illustrate its practicality with several examples. (C) 2017 Elsevier B.V. All rights reserved.

关键词： algorithmic game semantics Symbolic automata Program families Model checking algorithms

来源：评论

学校读者我要写书评

暂无评论

An approach to deciding the observational equivalence of Algol-like languages

引用

ANNALS OF PURE AND APPLIED LOGIC 2004年第1-3期130卷 125-171页

作者： Ong, CHL Univ Oxford Comp Lab Oxford OX1 3QD England

We prove that the observational equivalence of third-order finitary (i.e. recursion-free) Idealized Algol (IA) is decidable using game semantics. By modelling the state explicitly in our games, we show that the denotation of a term M of this fragment of IA is a compactly innocent strategy-with-state, i.e. the strategy is generated by a finite view function f(M). Given any such f(M), we construct a real-time deterministic pushdown automaton (DPDA) that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding the observational equivalence of third-order finitary IA. Restricted to second-order terms, the DPDA representation cuts down to a deterministic finite automaton;thus our approach gives a new proof of Ghica and McCusker's regular-expression characterization for this fragment. Our algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns second-order IA with full recursion: we show that observational equivalence for this fragment is undecidable. (C) 2004 Elsevier B.V. All rights reserved.

关键词： algorithmic game semantics Algol-like languages automata theory software model-checking

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：