The proceedings contain 87 papers. The topics discussed include: incremental whole-program analysis in datalog with lattices;revamping hardware persistency models: view-based and axiomatic persistency models for intel...
ISBN:
(纸本)9781450383912
The proceedings contain 87 papers. The topics discussed include: incremental whole-program analysis in datalog with lattices;revamping hardware persistency models: view-based and axiomatic persistency models for intel-x86 and armv8;repairing serializability bugs in distributed database programs via automated schema refactoring;Gleipnir: toward practical error analysis for quantum programs;transfinite iris: resolving an existential dilemma of step-indexed separation logic;Perceus: garbage free reference counting with reuse;unleashing the hidden power of compiler optimization on binary code difference: an empirical study;RefinedC: automating the foundational verification of C code with refined ownership types;and wire sorts: a language abstraction for safe hardware composition.
The proceedings contain 46 papers. The topics discussed include: exploring and improving code completion for test code;on the generalizability of deep learning-based code completion across programminglanguage version...
ISBN:
(纸本)9798400705861
The proceedings contain 46 papers. The topics discussed include: exploring and improving code completion for test code;on the generalizability of deep learning-based code completion across programminglanguage versions;ESGen: commit message generation based on edit sequence of code change;capturing and understanding the drift between design, implementation, and documentation;towards summarizing code snippets using pre-trained transformers;improving AST-level code completion with graph retrieval and multi-field attention;HyperCRX: a browser extension for insights into GitHub projects and developers;innovating coding: evaluating the impact of innovative thinking in programming;and MESIA: understanding and leveraging supplementary nature of method-level comments for automatic comment generation.
Macro systems are powerful language extension tools for Architecture Description languages (ADLs). Their generative power in combination with the simplicity of specification languages allows for a substantial reductio...
详细信息
ISBN:
(纸本)9798400704062
Macro systems are powerful language extension tools for Architecture Description languages (ADLs). Their generative power in combination with the simplicity of specification languages allows for a substantial reduction of repetitive specification sections. This paper explores how the introduction of function- and record types in a template-based macro system impacts the specification of ADLs. We present design andimplementation of a pattern-based syntax macro system for the Vienna Architecture Description language (VADL). The macro system is directly integrated into the language and is analyzed at parse time using a context-sensitive predLL(*) parser. The usefulness of the macro system is illustrated by some typical macro application design patterns. The effectiveness is shown by a detailed evaluation of the Instruction Set Architecture (ISA) specification of five different processor architectures. The observed specification reduction can be up to 90 times, leading to improved maintainability, readability and runtime performance of the specifications.
Stan is a probabilistic programminglanguage that is popular in the statistics community, with a high-level syntax for expressing probabilistic models. Stan differs by nature from generative probabilistic programming ...
详细信息
ISBN:
(纸本)9781450383912
Stan is a probabilistic programminglanguage that is popular in the statistics community, with a high-level syntax for expressing probabilistic models. Stan differs by nature from generative probabilistic programminglanguages like Church, Anglican, or Pyro. This paper presents a comprehensive compilation scheme to compile any Stan model to a generative language and proves its correctness. We use our compilation scheme to build two new backends for the Stanc3 compiler targeting Pyro and NumPyro. Experimental results show that the NumPyro backend yields a 2.3x speedup compared to Stan in geometric mean over 26 benchmarks. Building on Pyro we extend Stan with support for explicit variational inference guides and deep probabilistic models. That way, users familiar with Stan get access to new features without having to learn a fundamentally new language.
We present the Sum-Product Probabilistic language (SPPL), a new probabilistic programminglanguage that automatically delivers exact solutions to a broad range of probabilistic inference queries. SPPL translates proba...
详细信息
ISBN:
(纸本)9781450383912
We present the Sum-Product Probabilistic language (SPPL), a new probabilistic programminglanguage that automatically delivers exact solutions to a broad range of probabilistic inference queries. SPPL translates probabilistic programs into sum-product expressions, a new symbolic representation and associated semantic domain that extends standard sum-product networks to support mixed-type distributions, numeric transformations, logical formulas, and pointwise and set-valued constraints. We formalize SPPL via a novel translation strategy from probabilistic programs to sum-product expressions and give sound exact algorithms for conditioning on and computing probabilities of events. SPPL imposes a collection of restrictions on probabilistic programs to ensure they can be translated into sum-product expressions, which allow the system to leverage new techniques for improving the scalability of translation and inference by automatically exploiting probabilistic structure. We implement a prototype of SPPL with a modular architecture and evaluate it on benchmarks the system targets, showing that it obtains up to 3500x speedups over state-of-the-art symbolic systems on tasks such as verifying the fairness of decision tree classifiers, smoothing hidden Markov models, conditioning transformed random variables, and computing rare event probabilities.
Datalog is becoming increasingly popular as a standard tool for a variety of use cases. Modern Datalog engines can achieve high performance by specializing data structures for relational operations. For example, the D...
详细信息
ISBN:
(纸本)9781450383912
Datalog is becoming increasingly popular as a standard tool for a variety of use cases. Modern Datalog engines can achieve high performance by specializing data structures for relational operations. For example, the Datalog engine Souffle achieves high performance with a synthesizer that specializes data structures for relations. However, the synthesizer cannot always be deployed, and a fast interpreter is required. This work introduces the design andimplementation of the Souffle Tree Interpreter (STI). Key for the performance of the STI is the support for fast operations on relations. We obtain fast operations by de-specializing data structures so that they can work in a virtual execution environment. Our new interpreter achieves a competitive performance slowdown between 1.32 and 5.67x when compared to synthesized code. If compile time overheads of the synthesizer are also considered, the interpreter can be 6.46x faster on average for the first run.
Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU de...
详细信息
ISBN:
(纸本)9781450383912
Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale. Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task. CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort.
Program synthesis tasks are commonly specified via input-output examples. Existing enumerative techniques for such tasks are primarily guided by program syntax and only make indirect use of the examples. We identify a...
详细信息
ISBN:
(纸本)9781450383912
Program synthesis tasks are commonly specified via input-output examples. Existing enumerative techniques for such tasks are primarily guided by program syntax and only make indirect use of the examples. We identify a class of synthesis algorithms for programming-by-examples, which we call Example-Guided Synthesis (EGS), that exploits latent structure in the provided examples while generating candidate programs. We present an instance of EGS for the synthesis of relational queries and evaluate it on 86 tasks from three application domains: knowledge discovery, program analysis, and database querying. Our evaluation shows that EGS outperforms state-of-the-art synthesizers based on enumerative search, constraint solving, and hybrid techniques in terms of synthesis time, quality of synthesized programs, and ability to prove unrealizability.
In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current sup...
详细信息
ISBN:
(纸本)9781450383912
In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.
Web applications often handle large amounts of sensitive user data. Modern secure web frameworks protect this data by (1) using declarative languages to specify security policies alongside database schemas and (2) aut...
详细信息
ISBN:
(纸本)9781450383912
Web applications often handle large amounts of sensitive user data. Modern secure web frameworks protect this data by (1) using declarative languages to specify security policies alongside database schemas and (2) automatically enforcing these policies at runtime. Unfortunately, these frameworks do not handle the very common situation in which the schemas or the policies need to evolve over time-and updates to schemas and policies need to be performed in a carefully coordinated way. Mistakes during schema or policy migrations can unintentionally leak sensitive data or introduce privilege escalation bugs. In this work, we present a domain-specific language (Scooter) for expressing schema and policy migrations, and an associated SMT-based verifier (Sidecar) which ensures that migrations are secure as the application evolves. We describe the design of Scooter and Sidecar and show that our framework can be used to express realistic schemas, policies, and migrations, without giving up on runtime or verification performance.
暂无评论