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

26th International Symposium on Formal Methods (FM)

作者： Beckert, Bernhard Bubel, Richard Drodt, Daniel Haehnle, Reiner Lanzinger, Florian Pfeifer, Wolfram Ulbrich, Mattias Weigl, Alexander Karlsruhe Inst Technol Karlsruhe Germany Tech Univ Darmstadt Darmstadt Germany

ISBN: (纸本)9783031711763;9783031711770

The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

关键词： program verification Deductive verification Dynamic Logic Java Modeling Language

来源：评论

学校读者我要写书评

暂无评论

Semantics-based generation of verification conditions via program specialization

引用

SCIENCE OF COMPUTER programMING 2017年 147卷 78-108页

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G dAnnunzio DEC Viale Pindaro 42 I-65127 Pescara Italy Univ Roma Tor Vergata DICII Via Politecn 1 I-00133 Rome Italy CNR IASI Via Taurini 19 I-00185 Rome Italy

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it generates the verification conditions by specializing, using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics. We define a multi-step operational semantics for a fragment of the C language and compare the verification conditions obtained by using this semantics with those obtained by using a more traditional small-step semantics. The flexibility of the approach is further demonstrated by showing that it is possible to easily take into account alternative operational semantics definitions for modeling additional language features. We have proved that the verification condition generation takes a number of transformation steps that is linear with respect to the size of the imperative program to be verified. Also the size of the verification conditions is linear with respect to the size of the imperative program. Besides the theoretical computational complexity analysis, we also provide an experimental evaluation of the method by generating verification conditions using the multi-step and the small-step semantics for a few hundreds of programs taken from various publicly available benchmarks, and by checking the satisfiability of these verification conditions by using state-of-the-art Horn clause solvers. These experiments show that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice. (C) 2016 Elsevier B.V. All rights reserved.

关键词： Horn clauses program verification program specialization Semantics of programming languages Software model checking

来源：评论

学校读者我要写书评

暂无评论

Formalization of Differential Privacy in Isabelle/HOL 25

Formalization of Differential Privacy in Isabelle/HOL

引用

14th Conference on Certified programs and Proofs

作者： Sato, Tetsuya Minamide, Yasuhiko Inst Sci Tokyo Tokyo Japan

ISBN: (纸本)9798400713477

Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism.

关键词： Differential Privacy Isabelle/HOL proof assistant program verification

来源：评论

学校读者我要写书评

暂无评论

Type-Based verification of Connectivity Constraints in Lattice Surgery 22nd

Type-Based Verification of Connectivity Constraints in Latti...

引用

22nd Asian Symposium on programming Languages and Systems

作者： Wakizaka, Ryo Suzuki, Yasunari Igarashi, Atsushi Kyoto Univ Grad Sch Informat Kyoto Japan NTT Comp & Data Sci Labs Musashino Tokyo 1808585 Japan

ISBN: (纸本)9789819789429;9789819789436

Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present Q(LS), a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.

关键词： fault-tolerant quantum computation lattice surgery program verification type systems

来源：评论

学校读者我要写书评

暂无评论

Formal verification of a C-like memory model and its uses for verifying program transformations

引用

JOURNAL OF AUTOMATED REASONING 2008年第1期41卷 1-31页

作者： Leroy, Xavier Blazy, Sandrine INRIA Paris Rocquencourt F-78153 Le Chesnay France ENSIIE F-91025 Evry France

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler.

关键词： memory model C program verification compilation compiler correctness the Coq proof assistant

来源：评论

学校读者我要写书评

暂无评论

Modeling the control of a flexible manufacturing cell for automatic verification and control program generation

引用

INTERNATIONAL JOURNAL OF FLEXIBLE MANUFACTURING SYSTEMS 2006年第3期18卷 191-208页

作者： Richardsson, Johan Fabian, Martin Volvo Car Corp Gothenburg Sweden Chalmers S-41296 Gothenburg Sweden

Shortened product life-cycles decrease the output rate of manufacturing systems. Offline verification of the control systems promises to increase the output. However, to make offline verification possible some major improvements of the current development process of manufacturing systems are needed. Information handling and development of control programs based on information reuse are two of the most important improvement areas. This paper presents the results of the modeling of a real manufacturing cell according to a previously presented method for offline verification and program generation based on information reuse.

关键词： information reuse control program verification program generation manufacturing cell

来源：评论

学校读者我要写书评

暂无评论

Modeling the control of a flexible manufacturing cell for automatic verification and control program generation

Modeling the control of a flexible manufacturing cell for au...

引用

3rd International Conference on Reconfigurable Manufacturing

作者： Richardsson, Johan Fabian, Martin Volvo Car Corp Gothenburg Sweden Chalmers S-41296 Gothenburg Sweden

关键词： information reuse control program verification program generation manufacturing cell

来源：评论

学校读者我要写书评

暂无评论

Semantics-based generation of verification conditions by program specialization 15

Semantics-based generation of verification conditions by pro...

引用

17th International Symposium on Principles and Practice of Declarative programming (PPDP)

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G dAnnunzio DEC Chieti Italy Univ Roma Tor Vergata DICII Rome Italy CNR IASI Rome Italy

ISBN: (纸本)9781450335164

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it specializes, by using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics. We define a multi-step operational semantics for a fragment of the C language and compare the verification conditions obtained by using this semantics with those obtained by using a more traditional small-step semantics. The flexibility of the approach is further demonstrated by showing that it is possible to easily take into account alternative operational semantics definitions for modeling new language features. Finally, we provide an experimental evaluation of the method by generating verification conditions using the multi-step and the small-step semantics for a few hundreds of programs taken from various publicly available benchmarks, and by checking the satisfiability of these verification conditions by using state-of-the-art Horn clause solvers. These experiments show that automated verification of programs from a formal definition of the operational semantics is indeed feasible in practice.

关键词： Software model checking program verification program specialization semantics of programming languages verification conditions constraint logic programming Horn clauses

来源：评论

学校读者我要写书评

暂无评论

Full Regular Temporal Property verification as Dynamic program Execution 17

Full Regular Temporal Property Verification as Dynamic Progr...

引用

IEEE/ACM 39th International Conference on Software Engineering Companion (ICSE-C)

作者： Wang, Meng Tian, Cong Duan, Zhenhua ICTT & ISN Lab Xian 710071 Shaanxi Peoples R China

ISBN: (纸本)9781538615898

verification of programs in code-level has attracted more and more attentions and considerable progress has been made in this area. The early research is limited to the verification of safety properties [1], [2], [3]. To do so, assertions are required to be instrumented in the program to be verified in advance, and the reachability of error labels is checked afterwards. In this way, safety properties can be verified. However, verification of other temporal properties such as liveness cannot be supported. Model checking temporal properties without executing code [4], [5], [6], [7] considers all possible behaviors, which makes a small program have a very large state-space. Thus, it is difficult to apply the approach to verifying programs in large scale. In addition, the approach is poor in accuracy and often produces unsound results. Runtime verification is pursued to check whether one or a few execution traces satisfy a given property by monitoring the execution of a system [8], [9]. Although it avoids the state-explosion problem, extracting information from a running system and sending them to monitors may generate a large runtime overhead. In a word, the techniques available are far more from mature in the field of temporal property verification of programs in code-level.

关键词： Dynamic program Execution time characteristic Legal Executions dynamic verification program verification program EXECUTION running system

来源：评论

学校读者我要写书评

暂无评论

Deductive verification of solidity smart contracts with SSCalc

引用

SCIENCE OF COMPUTER programMING 2025年 243卷

作者： Marmsoler, Diego Thornton, Billy Univ Exeter Innovat Ctr Dept Comp Sci Exeter EX4 4RN England

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we verify a theorem which guarantees that all instances of an arbitrary contract type satisfy a corresponding invariant. The theorem can be used to verify invariants for Solidity smart contracts. This is demonstrated by a case study in which we use our approach to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

关键词： Smart contracts Solidity program verification Isabelle/Solidity

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：