The reference implementation of Cartesian Genetic programming (CGP) was written in the C programminglanguage. C inherently follows a procedural programming paradigm, which entails challenges in providing a reusable a...
详细信息
Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators ...
详细信息
Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such ...
详细信息
ISBN:
(纸本)9798400700507
Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol models, which is not sufficient to show that their implementations are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programminglanguage and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programminglanguages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C.
This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., sy...
详细信息
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.
A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a...
详细信息
ISBN:
(纸本)9798400700507
A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. We design a programminglanguage, Ou, aimed at easing the programmer's burden when writing efficient ZKPs, and a compiler framework, Lian, that automates the analysis and distribution of statements to a computing cluster. Lian uses programminglanguage semantics, formal methods, and combinatorial optimization to automatically partition an Ou program into efficiently sized chunks for parallel ZK-proving and/or verification. We contribute: (1) A front-end language where users can write proof statements as imperative programs in a familiar syntax;(2) A compiler architecture and implementation that automatically analyzes the program and compiles it into an optimized IR that can be lifted to a variety of ZKP constructions;and (3) A cutting algorithm, based on Pseudo-Boolean optimization and Integer Linear programming, that reorders instructions and then partitions the program into efficiently sized chunks for parallel evaluation and efficient state reconciliation.
The proceedings contain 47 papers. The topics discussed include: cache locality optimization for recursive programs;generalizations of the theory and deployment of triangular inequality for compiler-based strength red...
ISBN:
(纸本)9781450349888
The proceedings contain 47 papers. The topics discussed include: cache locality optimization for recursive programs;generalizations of the theory and deployment of triangular inequality for compiler-based strength reduction;DemoMatch: API discovery from demonstrations;similarity of binaries through re-optimization;BARRACUDA: binary-level analysis of runtime races in CUDA programs;bringing the web up to speed with WebAssembly;proactive and adaptive energy-aware programming with mixed typechecking;simple, fast, and safe manual memory management;efficient and precise points-to analysis: modeling the heap by merging equivalent automata;static deadlock detection for asynchronous c# programs;achieving high coverage for floating-point code via unconstrained programming;skeletal program enumeration for rigorous compiler testing;decomposition instead of self-composition for proving the absence of timing channels;automatic program inversion using symbolic transducers;rigorous analysis of software countermeasures against cache attacks;component-based synthesis of table consolidation and transformation tasks from examples;and network configuration synthesis with abstract topologies.
ProbZelus is a synchronous probabilistic language for the design of reactive probabilistic models in interaction with an environment. Reactive inference methods continuously learn distributions over the unobserved par...
详细信息
ISBN:
(纸本)9781450392662
ProbZelus is a synchronous probabilistic language for the design of reactive probabilistic models in interaction with an environment. Reactive inference methods continuously learn distributions over the unobserved parameters of the model from statistical observations. Unfortunately, this inference problem is in general intractable. Monte Carlo inference techniques thus rely on many independent executions to compute accurate approximations. These methods are expensive but can be parallelized. We propose to use JAX to parallelize ProbZelus reactive inference engine. JAX is a recent library to compile Python code which can then be executed on massively parallel architectures such as GPUs or TPUs. In this paper, we describe a new reactive inference engine implemented in JAX and the new associated JAX backend for ProbZelus. We show on existing benchmarks that our new parallel implementation outperforms the original sequential implementation for a high number of particles.
Protein language models have enabled breakthrough approaches to protein structure prediction, function annotation, and drug discovery. A primary limitation to the widespread adoption of these powerful models is the hi...
详细信息
ISBN:
(纸本)9781450392051
Protein language models have enabled breakthrough approaches to protein structure prediction, function annotation, and drug discovery. A primary limitation to the widespread adoption of these powerful models is the high computational cost associated with the training and inference of these models, especially at longer sequence lengths. We present the architecture, microarchitecture, and hardware implementation of a protein design and discovery accelerator, ProSE (Protein Systolic Engine). ProSE has a collection of custom heterogeneous systolic arrays and special functions that process transfer learning model inferences efficiently. The architecture marries SIMD-style computations with systolic array architectures, optimizing coarse-grained operation sequences across model layers to achieve efficiency without sacrificing generality. ProSE performs Protein BERT inference at up to 6.9x speedup and 48x power efficiency (performance/Watt) compared to one NVIDIA A100 GPU. ProSE achieves up to 5.5 x (12.7x) speedup and 173x (249x) power efficiency compared to TPUv3 (TPUv2).
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.
暂无评论