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

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification language

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1510-1534页

作者： Parthasarathy, Gaurav Dardinier, Thibault Bonneau, Benjamin Muller, Peter Summers, Alexander J. Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland Univ Grenoble Alpes CNRS Grenoble INP VERIMAG Grenoble France Univ British Columbia Vancouver BC Canada

Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation, not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.

关键词： Software Verification Intermediate Verification languages Formal Semantics Proof Certification

来源：评论

学校读者我要写书评

暂无评论

The JastAdd Extensible Java Compiler 07

The JastAdd Extensible Java Compiler

引用

22nd International conference on Object-Oriented programming, Systems, languages and Applications

作者： Ekman, Torbjorn Hedin, Gorel Univ Oxford Programming Tools Grp Oxford England Lund Univ Dept Comp Sci S-22100 Lund Sweden

ISBN: (纸本)9781595937865

The JastAdd Extensible Java Compiler is a high quality Java compiler that is easy to extend in order to build static analysis tools for Java, and to extend Java with new language constructs. It is built modularly, with a Java 1.4 compiler that is extended to a Java 5 compiler. Example applications that are built as extensions include an alternative backend that generates Jimple, an extension of Java with AspectJ constructs, and the implementation of a pluggable type system for non-null checking and inference. The system is implemented using JastAdd, a declarative Java-like language. We describe the compiler architecture, the major design ideas for building and extending the compiler, in particular, for dealing with complex extensions that affect name and type analysis. Our extensible compiler compares very favorably concerning quality, speed and size with other extensible Java compiler frameworks. It also compares favorably in quality and size compared with traditional non-extensible Java compilers, and it runs within a factor of three compared to javac.

关键词： design languages OOP compilers extensibility declarative frameworks modularity Java

来源：评论

学校读者我要写书评

暂无评论

Backtracking without trailing in CLP (RLin) 94

Backtracking without trailing in CLP (RLin)

引用

proceedings of the acm sigplan'94 conference on programming language design and implementation (PLDI)

作者： Van Hentenryck, Pascal Ramachandran, Viswanath Brown Univ Providence United States

ISBN: (纸本)089791662X

Constraint logic programming (CLP) is a generalization of logic programming where unification is replaced by constraint solving as the basic operation of the language. The combination of constraint solving and nondeterminism (approximated by backtracking) makes these languages appealing for a variety of combinatorial search problems. Existing CLP languages support backtracking by generalizing traditional Prolog implementations: modifications to the constraint system are trailed and restored on backtracking. Although simple and efficient, trailing may be very demanding in memory space, since the constraint system may potentially be saved at each choice point. This paper proposes a fundamentally new implementation scheme for backtracking in CLP languages over linear (rational or real) arithmetic. The new scheme, called semantic backtracking, does not use trailing but rather exploits the semantics of the constraints to undo the effect of newly added constraints. Semantic backtracking reduces the space complexity by an order of magnitude compared to implementations based on trailing and makes space complexity essentially independent of the number of choice points. In addition, semantic backtracking introduces negligible space and time overhead on deterministic programs. The price for this improvement is an increase in backtracking time, although constraint-solving time may actually decrease. The scheme has been implemented as part of a complete CLP system CLP (RLin) and compared analytically and experimentally with an optimized trailing implementation. Experimental results indicate that semantic backtracking produces significant reduction in memory space, while keeping the time overhead reasonably small.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

Recollections about the development of pascal 2

Recollections about the development of pascal

引用

2nd acm sigplan conference on History of programming languages, HOPL 1993

作者： Wirth, N. Institut für Computer systeme E7H Zürich ZürichCH-8092 Switzerland

ISBN: (纸本)0897915704

Pascal was defined in 1970 and, after a slow start, becane one of the most widely used languages n introductoiy programming courses. This a/tide first summarises the events leading to Pascal's design and implementation, and then proceeds with a discussion of some of the anguage's merits and deficiencies. In the last part, developments that followed its release are recounted. Its influence chiefly derived from its being a vehicle for structured programming and a basis for further development of languages and for experiments in program verification.

关键词： Structured programming

来源：评论

学校读者我要写书评

暂无评论

Automatic verification of pointer programs using monadic second-order logic

Automatic verification of pointer programs using monadic sec...

引用

proceedings of the 1997 acm SIGPLAM conference on programming language design and implementation, PLDI

作者： Jensen, Jakob L. Jorgensen, Michael E. Klarlund, Nils Schwartzbach, Michael I. Univ of Aarhus Aarhus Denmark

We present a technique for automatic verification of pointer programs based on a decision procedure for the monadic second-order logic on finite strings. We are concerned with a while-fragment of Pascal, which includes recursively-defined pointer structures but excludes pointer arithmetic. We define a logic of stores with interesting basic predicates such as pointer equality, tests for nil pointers, and garbage cells, as well as reachability along pointers. We present a complete decision procedure for Hoare triples based on this logic over loop-free code. Combined with explicit loop invariants, the decision procedure allows us to answer surprisingly detailed questions about small but non-trivial programs. If a program fails to satisfy a certain property, then we can automatically supply an initial store that provides a counterexample. Our technique has been fully and efficiently implemented for linear linked lists, and it extends in principle to tree structures. The resulting system can be used to verify extensive properties of smaller pointer programs and could be particularly useful in a teaching environment.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Integrated design

Integrated design

引用

1973 acm sigplan - SIGOPS Interface Meeting: programming languages - Operating Systems

作者： Habermann, A.N. University of Newcastle Upon Tyne United Kingdom

Matters of design, analysis and documentation of a programming System are frequently ordered sequentially in time and distributed over independent groups of people. It is argued that, instead, these three aspects should be integrated into one production effort in which documentation is the primary issue. The language that is used for implementation must not dominate the description of the system because a system should not be defined and understood in terms of its implementation. Using such a language throughout documentation and design is on the one hand too restrictive because the language is bound to lack expressive power, but on the other hand it is too demanding because it forces to go into details that may be irrelevant for a description at hand. © 1973 Association for Computing Machinery. All rights reserved.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Improving performance by branch reordering 98

Improving performance by branch reordering

引用

proceedings of the 1998 Annual acm sigplan conference on programming language design and implementation, PLDI

作者： Yang, Minghui Uh, Gang-Ryung Whalley, David B. Florida State Univ Tallahassee FL United States

ISBN: (纸本)9780897919876

The conditional branch has long been considered an expensive operation. The relative cost of conditional branches has increased as recently designed machines are now relying on deeper pipelines and higher multiple issue. Reducing the number of conditional branches executed can often result in a substantial performance benefit. This paper describes a code-improving transformation to reorder sequences of conditional branches. First, sequences of branches that can be reordered are detected in the control flow. Second, profiling information is collected to predict the probability that each branch will transfer control out of the sequence. Third, the cost of performing each conditional branch is estimated. Fourth, the most beneficial ordering of the branches based on the estimated probability and cost is selected. The most beneficial ordering often included the insertion of additional conditional branches that did not previously exist in the sequence. Finally, the control flow is restructured to reflect the new ordering. The results of applying the transformation were significant reductions in the dynamic number of instructions and branches, as well as decreases in execution time.

关键词： Computer systems programming

来源：评论

学校读者我要写书评

暂无评论

Modular Hardware design of Pipelined Circuits with Hazards

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 28-51页

作者： Jang, Minseong Rhee, Jungin Lee, Woojin Zhao, Shuangshuang Kang, Jeehoon Korea Adv Inst Sci & Technol Daejeon South Korea

Modular design is critical in reducing hardware designer's cognitive load and development cost. However, it is challenging to modularize high-performance pipelined circuits with structural, data, and control hazards because their resolution-stalling, and bypassing, and discard-and-restarting-introduce cross-stage dependencies. The dependencies could potentially mandate monolithic control logic and create combinational loops, hindering modular design. An effective method to modularize pipelined circuits is valid-ready interfaces, but they apply to a relatively simple form of pipelined circuits only with structural hazards. We propose hazard interfaces, a generalization of valid-ready interfaces that can modularize pipelined circuits not only with structural but also with data and control hazards. The key idea is enveloping the cross-stage dependencies within interfaces. We also design combinators for hazard interfaces in the style of map-reduce that facilitate decomposition of control logic. We implement a compiler (to synthesizable Verilog) for a prototype language supporting hazard interfaces and combinators, and design a sound and efficient type checker that proves the absence of combinational loops. With case studies on 5-stage RISC-V CPU core and 100 Gbps Ethernet NIC, we demonstrate that hazard interfaces indeed facilitate modular design while incurring no noticeable cost in performance, power, and area over reference designs in Chisel and Verilog.

关键词： hardware description language functional programming pipelining hazard combinator

来源：评论

学校读者我要写书评

暂无评论

Slicing Probabilistic Programs 14

Slicing Probabilistic Programs

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Hur, Chung-Kil Nori, Aditya V. Rajamani, Sriram K. Samuel, Selva Seoul Natl Univ Seoul 151 South Korea

ISBN: (纸本)9781450327848

Probabilistic programs use familiar notation of programming languages to specify probabilistic models. Suppose we are interested in estimating the distribution of the return expression r of a probabilistic program P. We are interested in slicing the probabilistic program P and obtaining a simpler program SLI (P) which retains only those parts of P that are relevant to estimating r, and elides those parts of P that are not relevant to estimating r. We desire that the SLI transformation be both correct and efficient. By correct, we mean that P and SLI (P) have identical estimates on r. By efficient, we mean that estimation over SLI (P) be as fast as possible. We show that the usual notion of program slicing, which traverses control and data dependencies backward from the return expression r, is unsatisfactory for probabilistic programs, since it produces incorrect slices on some programs and sub-optimal ones on others. Our key insight is that in addition to the usual notions of control dependence and data dependence that are used to slice non-probabilistic programs, a new kind of dependence called observe dependence arises naturally due to observe statements in probabilistic programs. We propose a new definition of SLI (P) which is both correct and efficient for probabilistic programs, by including observe dependence in addition to control and data dependences for computing slices. We prove correctness mathematically, and we demonstrate efficiency empirically. We show that by applying the SLI transformation as a pre-pass, we can improve the efficiency of probabilistic inference, not only in our own inference tool R2, but also in other systems for performing inference such as Church and Infer. NET.

关键词： Probabilistic programming Program Slicing Bayesian Reasoning

来源：评论

学校读者我要写书评

暂无评论

Advanced programming language design in enterprise software - A lambda-calculus theorist wanders into a datacenter 07

Advanced programming language design in enterprise software ...

引用

34th acm sigplan-SIGACT Symposium on Principles of programming languages

作者： Murthy, Chet IBM Research

ISBN: (纸本)9781595935755

Enterprise software systems automate the business processes of most nontrivial organizations in the world economy. These systems are immensely complex, and their function is critical to our living standards and everyday lives. Their design, implementation, and maintenance occupies many thousands of programmers and engineers, who work in what are aptly called the "COBOL dungeons"(1) of the IT sector. These systems have persisted, growing by accretion - some for decades;there are enterprise systems in existence today whose original and even subsequent authors are retired or deceased. Such extraordinarly old, multi-layered systems might appear to be the last place to apply avante-garde techniques, but in fact, they are extremely promising candidates, and for reasons directly connected to their history and structure. In this talk we take a tour of several deployed enterprise software systems, and demonstrate that the appropriate application of methods from functional programming can and does in fact yield dramatic performance improvements and thus commercial advantage in the design and implementation of enterprise software. This concrete application is an instance of a general plan for the application of advanced programming language design and analysis methods, to the problem of improving enterprise software. It is the thesis of this talk that to a great extent, it is in enterprise software that advanced PL techniques can find their most advantageous application. This talk literally breaks no new ground in PL research: every technique discussed is nearly two decades old, and our goal is to introduce PL researchers to what we feel is an ideal target for their work.

关键词： languages transaction processing enterprise software functional languages

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：