The proceedings contain 68 papers. The topics discussed include: modular information flow through ownership;ANOSY: approximated knowledge synthesis with refinement types for declassification;hardening attack surfaces ...
ISBN:
(纸本)9781450392655
The proceedings contain 68 papers. The topics discussed include: modular information flow through ownership;ANOSY: approximated knowledge synthesis with refinement types for declassification;hardening attack surfaces with formally proven binary format parsers;turning manual concurrent memory reclamation into automatic reference counting;low-latency, high-throughput garbage collection;mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacenters;visualization question answering using introspective program synthesis;synthesizing analytical SQL queries from computation demonstration;sequential reasoning for optimizing compilers under weak memory concurrency;and can reactive synthesis and syntax-guided synthesis be friends?.
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 77 papers. The topics discussed include: data-driven inference of representation invariants;type error feedback via analytic program repair;synthesizing structured CAD models with equality satu...
ISBN:
(纸本)9781450376136
The proceedings contain 77 papers. The topics discussed include: data-driven inference of representation invariants;type error feedback via analytic program repair;synthesizing structured CAD models with equality saturation and inverse transformations;compiler and runtime support for continuation marks;from folklore to fact: comparing implementations of stacks and continuations;learning nonlinear loop invariants with gated continuous logic networks;blended, precise semantic program embeddings;and BlankIt library debloating: getting what you want instead of cutting what you don't.
The proceedings contain 55 papers. The topics discussed include: BLeak: automatically debugging memory leaks in web applications;putting in all the stops: execution control for JavaScript;persistency for synchronizati...
ISBN:
(纸本)9781450356985
The proceedings contain 55 papers. The topics discussed include: BLeak: automatically debugging memory leaks in web applications;putting in all the stops: execution control for JavaScript;persistency for synchronization-free regions;write-rationing garbage collection for hybrid memories;mapping spiking neural networks onto a manycore neuromorphic architecture;static serializability analysis for causal consistency;Cuba: interprocedural context-unbounded analysis of concurrent programs;advanced automata-based algorithms for program termination checking;HHVM JIT: a profile-guided, region-based compiler for PHP and Hack;EffectiveSan: type and memory error detection using dynamically typed C/C++;calling-to-reference context translation via constraint-guided CFL-reachability;the semantics of transactions and weak memory in x86, power, ARM, and C++;MixT: a language for mixing consistency in geodistributed transactions;finding root causes of floating point error;to-many or to-one? all-in-one! efficient purely functional multi-maps with type-heterogeneous hash-tries;spatial: a language and compiler for application accelerators;enhancing computation-to-core assignment with physical location information;and SWOOP: so ware-hardware co-design for non-speculative, execute-ahead, in-order cores.
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.
The proceedings contain 48 papers. The topics discussed include: into the depths of C: elaborating the de facto standards;data-driven precondition inference with learned features;Cartesian Hoare logic for verifying k-...
ISBN:
(纸本)9781450342612
The proceedings contain 48 papers. The topics discussed include: into the depths of C: elaborating the de facto standards;data-driven precondition inference with learned features;Cartesian Hoare logic for verifying k-safety properties;verifying bit-manipulations of floating-point;coverage-directed differential testing of JVM implementations;lightweight computation tree tracing for lazy functional languages;effective padding of multidimensional arrays to avoid cache conflict misses;input responsiveness: using canary inputs to dynamically steer approximation;configuration synthesis for programmable analog devices with Arco;from datalog to flix: a declarative language for fixed points on lattices;latte: a language, compiler, and runtime for elegant and efficient deep neural networks;on the complexity and performance of parsing with derivatives;and toward compositional verification of interruptible OS kernels and device drivers.
The proceedings contain 59 papers. The topics discussed include: automatic error elimination by horizontal code transfer across multiple applications;mechanized verification of fine-grained concurrent programs;algorit...
ISBN:
(纸本)9781450334686
The proceedings contain 59 papers. The topics discussed include: automatic error elimination by horizontal code transfer across multiple applications;mechanized verification of fine-grained concurrent programs;algorithmic debugging of real-world Haskell programs: deriving dependencies from the cost centre stack;light: replay via tightly bounded recording;provably correct peephole optimizations with alive;automatically improving accuracy for floating point expressions;diagnosing type errors with class;verification of producer-consumer synchronization in GPU programs;verification of a cryptographic primitive: SHA-256;asynchronous programming, analysis and testing with state machines;laminarIR: compile-time queues for structured streams;optimizing off-chip accesses in multicores;improving compiler scalability: optimizing large programs at small price;verifying read-copy-update in a logic for weak memory;and stateless model checking concurrent programs with maximal causality reduction.
Educational robots serve multiple purposes, including language learning, social skills development for students with autism, and improving communication skills. This research emphasizes the role of educational profess...
详细信息
ISBN:
(纸本)9798400708244
Educational robots serve multiple purposes, including language learning, social skills development for students with autism, and improving communication skills. This research emphasizes the role of educational professionals in designing robotic learning activities, highlighting their understanding of pedagogy and student needs. Two language instructors co-designed programming workshops which aimed to teach them how to program the social robot NAO. They implemented robotic language learning activities that were used by 35 students in Finnish language courses. The results of this research suggested that hands-on programming workshops are an effective way to learn robot programming. Maintaining motivation during the sessions is facilitated by setting clear and concrete goals, monitoring progress, acquiring new knowledge, and following a precise schedule. The instructors faced challenges such as unexpected responses from the robots, the initial complexity of the programming software, and apprehensions about programming based on prior knowledge of text-based programminglanguages.
This article presents the design and development of a dataflow programminglanguage called DFC2 (DataFlow C, version 2) based on the dataflow programming model. The DFC2 compiler is responsible for converting the DFC2...
详细信息
ISBN:
(纸本)9798400708428
This article presents the design and development of a dataflow programminglanguage called DFC2 (DataFlow C, version 2) based on the dataflow programming model. The DFC2 compiler is responsible for converting the DFC2 language into C++ language, which is then compiled into an executable file by the C++ compiler. DFC2 is designed to be user-friendly and easy to use by adhering to the traditional imperative programminglanguage model. It also allows for the reuse of existing C language code to reduce development costs. DFC2 distinguishes between graph functions, which are automatically parallelized, and func functions, which are not, giving users greater control over the level of parallelism. Users can describe dataflow graphs at both the inter-function and intra-function levels. This article also implements an optimization framework for the DFC2 compiler and analyzes the optimization results. It demonstrates that with the introduction of conditional constant propagation and dead code elimination, it is possible to reduce execution time by up to 30% in the best-case scenario and an average of approximately 6%.
暂无评论