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

5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011

作者： Reynolds, John C. Carnegie Mellon University United States

ISBN: (纸本)9780769545066

To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. program proving is unlike theorem proving in mathematics mathematical conjectures may give no hint as to how they could be proved, but programs are written by programmers, who must understand informally why their programs work. The job of verification is not to explore some immense search space, but to formalize the programmer's intuitions until any faults are revealed. This requires specifications and proofs that are succinct and intelligible which in turn require logics that go be yond predicate calculus (the assembly language of program proving). In this talk, I will recount and illustrate several steps, old and new, towards this goal - particularly in the treatment of arrays.

关键词： Arrays Assembly Calculus Conferences Logic arrays programming formal specification formal verification predicate calculus process algebra program logics program proving program specifications programming safety properties verification

来源：评论

学校读者我要写书评

暂无评论

Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and program logics

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2021年第ICFP期5卷 1–30页

作者： Aguirre, Alejandro Barthe, Gilles Gaboardi, Marco Garg, Deepak Katsumata, Shin-ya Sato, Tetsuya Univ Politecn Madrid Madrid Spain Aarhus Univ Aarhus Denmark MPI SP Bochum Spain IMDEA Software Inst Madrid Spain Boston Univ Boston MA 02215 USA Max Planck Inst Software Syst Saarland Informat Campus Saarbrucken Germany Natl Inst Informat Chiyoda Ku 2-1-2 Hitotsubashi Tokyo 1018430 Japan Tokyo Inst Technol Tokyo Japan

Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed lambda-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.

关键词： Probabilistic programming semantic models program logics

来源：评论

学校读者我要写书评

暂无评论

A Demonic Outcome Logic for Randomized Nondeterminism

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2025年第POPL期9卷 539-568页

作者： Zilberstein, Noam Kozen, Dexter Silva, Alexandra Tassarotti, Joseph Cornell Univ Ithaca NY 14850 USA NYU New York NY USA

programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism (for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws-including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.

关键词： program logics Probabilistic programming Demonic Nondeterminism

来源：评论

学校读者我要写书评

暂无评论

CALL-BY-NAME GRADUAL TYPE THEORY

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2020年第1期16卷

作者： New, Max S. Licata, Daniel R. Northeastern Univ Boston MA 02115 USA Wesleyan Univ Middletown CT 06459 USA

We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism. These dynamism judgments build on prior work in blame calculi and on the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality (eta) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs. This construction is a semantic analogue of the interpretation of gradual typing using contracts, and use it to build some concrete domain-theoretic models of gradual typing.

关键词： Gradual Typing Type Systems program logics Category Theory Denotational Semantics

来源：评论

学校读者我要写书评

暂无评论

Locally Abstract, Globally Concrete Semantics of Concurrent programming Languages

引用

ACM TRANSACTIONS ON programMING LANGUAGES AND SYSTEMS 2024年第1期46卷 1-58页

作者： Din, Crystal Chang Haehnle, Reiner Henrio, Ludovic Johnsen, Einar Broch Pun, Violet Ka I. Tarifa, S. Lizeth Tapia Univ Bergen Dept Informat Thormohlens Gate 55 N-5006 Bergen Norway Tech Univ Darmstadt Dept Comp Sci Hochschul Str 10 D-64289 Darmstadt Germany Univ Lyon CNRS LIP Lab EnsLInriaUCBL 46 Allee Italie F-69364 Lyon France Univ Oslo Dept Informat Postboks 1080 Blindern N-0316 Oslo Norway Western Norway Univ Appl Sci Inndalsveien 28 N-5063 Bergen Norway

Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that we enrich with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models. We also illustrate how a sound program logic and calculus can be defined for this semantics.

关键词： Denotational semantics trace semantics compositionality continuations concurrent programming languages program logics program calculus

来源：评论

学校读者我要写书评

暂无评论

Indexed Types for a Statically Safe WebAssembly

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2024年第POPL期8卷 2395-2424页

作者： Geller, Adam T. Frank, Justin Bowman, William J. Univ British Columbia Vancouver BC Canada Univ Maryland College Pk MD USA

We present Wasm-precheck, a superset of WebAssembly (Wasm) that uses indexed types to express and check simple constraints over program values. This additional static reasoning enables safely removing dynamic safety checks from Wasm, such as memory bounds checks. We implement Wasm-precheck as an extension of the Wasmtime compiler and runtime, evaluate the run-time and compile-time performance of Wasm-precheck vs Wasm configurations with explicit dynamic checks, and find an average run-time performance gain of 1.71x faster in the widely used PolyBenchC benchmark suite, for a small overhead in binary size (7.18% larger) and type-checking time (1.4% slower). We also prove type and memory safety of Wasm-precheck, prove Wasm safely embeds into Wasm-precheck ensuring backwards compatibility, prove Wasm-precheck type-erases to Wasm, and discuss design and implementation trade-offs.

关键词： WebAssembly Indexed Types program logics Optimization and Compiler Design Type Systems

来源：评论

学校读者我要写书评

暂无评论

Local Refinement Typing

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2017年第ICFP期1卷 1-27页

作者： Cosman, Benjamin Jhala, Ranjit Univ Calif San Diego La Jolla CA 92093 USA

We introduce the FUSION algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is concise as the programmer need only write signatures for (externally exported) top-level functions and places with cyclic (recursive) dependencies, after which FUSION can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented FUSION and evaluated it on the benchmarks from the LIQUIDHASKELL suite totalling about 12KLOC. FUSION checks an existing safety benchmark suite using about half as many templates as previously required and nearly 2x faster. In a new set of theorem proving benchmarks FUSION is both 10 - 50x faster and, by synthesizing the most precise types, avoids false alarms to make verification possible.

关键词： Refinement Types program logics SMT Verification

来源：评论

学校读者我要写书评

暂无评论

Modeling and Analyzing Evaluation Cost of CUDA Kernels

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2021年第POPL期5卷 1–31页

作者： Muller, Stefan K. Hoffmann, Jan IIT Chicago IL 60616 USA Carnegie Mellon Univ Pittsburgh PA 15213 USA

General-purpose programming on GPUs (GPGPU) is becoming increasingly in vogue as applications such as machine learning and scientific computing demand high throughput in vector-parallel applications. NVIDIA's CUDA toolkit seeks to make GPGPU programming accessible by allowing programmers to write GPU functions, called kernels, in a small extension of C/C++. However, due to CUDA's complex execution model, the performance characteristics of CUDA kernels are difficult to predict, especially for novice programmers. This paper introduces a novel quantitative program logic for CUDA kernels, which allows programmers to reason about both functional correctness and resource usage of CUDA kernels, paying particular attention to a set of common but CUDA-specific performance bottlenecks. The logic is proved sound with respect to a novel operational cost semantics for CUDA kernels. The semantics, logic and soundness proofs are formalized in Coq. An inference algorithm based on LP solving automatically synthesizes symbolic resource bounds by generating derivations in the logic. This algorithm is the basis of RaCuda, an end-to-end resource-analysis tool for kernels, which has been implemented using an existing resource-analysis tool for imperative programs. An experimental evaluation on a suite of CUDA benchmarks shows that the analysis is effective in aiding the detection of performance bugs in CUDA kernels.

关键词： resource-aware type system performance analysis CUDA thread-level parallelism program logics

来源：评论

学校读者我要写书评

暂无评论

Concurrent Incorrectness Separation Logic

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2022年第POPL期6卷 1–29页

作者： Raad, Azalea Berdine, Josh Dreyer, Derek O'Hearn, Peter W. Imperial Coll London London England Meta London England MPI SWS Saarbrucken Germany UCL London England

Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.

关键词： Concurrency program logics separation logic bug catching

来源：评论

学校读者我要写书评

暂无评论

Mechanized Logical Relations for Termination-Insensitive Noninterference

引用

PROCEEDINGS OF THE ACM ON programMING LANGUAGES-PACMPL 2021年第POPL期5卷 1–29页

作者： Gregersen, Simon Oddershede Bay, Johan Timany, Amin Birkedal, Lars Aarhus Univ Aarhus Denmark

We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed-but semantically sound-components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework;to capture termination-insensitivity, we develop a novel language-agnostic theory of Modal Weakest Preconditions. We formalize all of our theory and examples in the Coq proof assistant.

关键词： Logical Relations Information-Flow Control program logics Iris

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：