Search events for 'all'
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec 2019 When: Sun 23 Jun 2019 14:00 - 14:45 People: Ben Laurie
… …
Panel: Charting Your Path
PLMW @ PLDI 2019 When: Sun 23 Jun 2019 11:20 - 12:30 People: Lisa Hsu, Adrian Sampson, Emma Tosch, Caroline Trippel, Benjamin Zorn
… Researchers from all stages of their career – senior grad students, early-career researchers, and senior researchers – discuss the choices they made in plotting their careers. …
A week in the life of an MSR Researcher
PLMW @ PLDI 2019 When: Sun 23 Jun 2019 16:30 - 17:00 People: Todd Mytkowicz
… This talk uses a week from my calendar to give some perspective on what it is like to work at Microsoft Research. MSR is a unique lab that empowers me to solve hard problems all while being grounded by their applications to the needs …
Gigahorse: Thorough Smart Contract Decompilation and Security Analyses
DPA When: Sun 23 Jun 2019 12:00 - 12:30 People: Neville Grech
… contains the most complete, high-level decompiled representation of all Ethereum … several advanced high-level client analyses, including MadMax and Ethainter. All …
Towards Compiling Graph Queries in Relational Engines
DBPL 2019 When: Sun 23 Jun 2019 12:00 - 12:20 People: Ruby Tahboub, Xilun Wu, Gregory Essertel, Tiark Rompf
… The ongoing demand for graph query processing has prompted supporting graph workloads inside relational engines, after all, graphs are relations. Although supporting graph processing on the top of standard relational data management …
The K Framework
DPA When: Sun 23 Jun 2019 09:30 - 10:00 People: Sandeep Dasgupta
… is to generate all these automatically, correct-by-construction from a formal specification …
Now You See Me, Now You Don't: Querying with Hybrid Temporal Logic
DPA When: Sun 23 Jun 2019 14:00 - 14:30 People: Mistral Contrastin
… can all be used. Multimodal CTL operators allow various notions of time to be used …
Programming Abstractions for Orchestration of HPC Scientific Computing
CHIUW 2019 When: Sat 22 Jun 2019 14:00 - 15:00 People: Anshu Dubey
… Application developers are confronted with three axes of increasing complexity going forward; increasing heterogeneity in computing platforms at all levels, increasing heterogeneity in solvers and data management, and moving existing code …
Arkouda: Interactive Data Exploration Backed by Chapel
CHIUW 2019 When: Sat 22 Jun 2019 15:00 - 15:25 People: Michael Merrill, William Reus, Timothy Neumann
… Exploratory data analysis (EDA) is the prerequisite for all data science. EDA is non-negotiably interactive—by far the most popular environment for EDA is a Jupyter notebook—and, as datasets grow, increasingly computationally intensive …
Implementing Stencil Problems in Chapel: An Experience Report
CHIUW 2019 When: Sat 22 Jun 2019 11:45 - 12:10 People: Per Fuchs, Pieter Hijma, Clemens Grelck
… finish with a local-view implementation that explicitly encodes all design …
Array Processing on Steroids for the SKA Radio-Telescope
ARRAY 2019 When: Sat 22 Jun 2019 09:00 - 10:00 People: Peter Braam
… computational undertaking, requiring 200PB/sec of memory bandwidth, all dedicated to array …
Records with Rank Polymorphism
ARRAY 2019 When: Sat 22 Jun 2019 14:30 - 15:00 People: Justin Slepak, Olin Shivers, Panagiotis Manolios
… In a rank-polymorphic programming language, all functions automatically lift to operate on arbitrarily high-dimensional aggregate data. By adding records to such a language, we can support computation on data frames, a tabular data …
Modernizing Parsing Tools
SOAP When: Sat 22 Jun 2019 14:20 - 14:40 People: Steven O'Hara, Rocky Slavin
… available mechanism to parse and analyze all of the software in a unified manner …
Commit-time Incremental Analysis
SOAP When: Sat 22 Jun 2019 09:15 - 09:35 People: Paddy Krishnan, Rebecca O'Donoghue, Nicholas Allen, Yi Lu
… . For example, a backward summary-based analysis, will examine all the callers …
Know Your Analysis: How Instrumentation Aids Understanding Static Analysis
SOAP When: Sat 22 Jun 2019 09:35 - 09:55 People: Philipp Dominik Schubert, Richard Leer, Ben Hermann, Eric Bodden
… , all of which need to be obtained by wisely chosen and correctly parameterized …
Stack-Aware CompCert
DeepSpec 2019 When: Sat 22 Jun 2019 12:00 - 12:30 People: Yuting Wang
… is used uniformly for all of its languages and their verified compilation …-grained permissions to stack memory. Using this enriched memory model for all … of the full compilation chain of CompCert, including all the optimization passes …
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec 2019 When: Sat 22 Jun 2019 14:30 - 15:00 People: Mengqi Liu
… a challenge to this day. First of all, formalizing temporal properties … but also show that this new kernel enjoys temporal and spatial isolation. All …
Automated Formal Memory Consistency Verification of Hardware
DeepSpec 2019 When: Sun 23 Jun 2019 11:45 - 12:30 People: Yatin Manerkar
… correctness. However, comprehensive MCM verification requires checking across all … cases.
One component of my work, PipeProof, enables automated complete (i.e. all …
Coverage Guided, Property Based Testing
DeepSpec 2019 When: Sun 23 Jun 2019 16:15 - 16:45 People: Leonidas Lampropoulos
… a challenge to this day. First of all, formalizing temporal properties … but also show that this new kernel enjoys temporal and spatial isolation. All …
An Open, Transparent, Industry-Driven Approach to AV Safety
LCTES 2019 When: Sun 23 Jun 2019 14:10 - 14:45 People: Jack Weast
… At Intel and Mobileye, saving lives drives us. But in the world of automated driving, we believe safety is not merely an impact of AD, but the bedrock on which we all build this industry. And so we proposed Responsibility-Sensitive Safety …
Raising Binaries to LLVM IR with MCTOLL (Work in progress)
LCTES 2019 When: Sun 23 Jun 2019 16:25 - 16:30 People: S. Bharadwaj Yadavalli, Aaron Smith
… , and needs to be re-engineered all over again.
Work in progress is aimed to make …
An Empirical Comparison between Monkey Testing and Human Testing (Work in progress)
LCTES 2019 When: Sun 23 Jun 2019 16:35 - 16:40 People: Mostafa Mohammed, Haipeng Cai, Na Meng
… Android app testing is challenging and time-consuming because fully testing all feasible execution paths is always difficult. Apps are usually tested in two alternative ways: human testing vs. automated testing. Prior studies focused …
AutoPersist: An Easy-To-Use Java NVM Framework Based on Reachability
PLDI Research Papers When: Mon 24 Jun 2019 16:00 - 16:20 People: Thomas Shull, Jian Huang, Josep Torrellas
… should then automatically ensure that all the data structures reachable from … roots. AutoPersist then persists all the data structures that can be reached …
Toward Efficient Gradual Typing for Structural Types via Coercions
PLDI Research Papers When: Tue 25 Jun 2019 08:50 - 09:10 People: Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, Jeremy G. Siek
… .) but relatively few support all the criteria (Nom, Gradualtalk, Guarded … coercions eliminates all of the catastrophic slowdowns without introducing …
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
PLDI Research Papers When: Wed 26 Jun 2019 10:20 - 10:40 People: Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Roşu
… We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture …
Robustness Against Release/Acquire Semantics
PLDI Research Papers When: Mon 24 Jun 2019 10:40 - 11:00 People: Ori Lahav, Roy Margalit
… We present an algorithm for automatically checking robustness of concurrent programs against C/C++11 release/acquire semantics, namely verifying that all program behaviors under release/acquire are allowed by sequential consistency. Our …
Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs
PLDI Research Papers When: Mon 24 Jun 2019 15:00 - 15:20 People: Jieyuan Zhang, Jingling Xue
…
path-sensitive except
that it conducts a ``meet-over-all-paths …
Scalable Verification of Probabilistic Networks
PLDI Research Papers When: Mon 24 Jun 2019 14:00 - 14:20 People: Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, Alexandra Silva
… Markov chains. This view allows the
semantics of all programs to be computed …
Towards Certified Separate Compilation for Concurrent Programs
PLDI Research Papers When: Mon 24 Jun 2019 10:20 - 10:40 People: Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, Xinyu Feng
… races. All our work has been implemented in the Coq proof assistant. …
Proving Differential Privacy with Shadow Execution
PLDI Research Papers When: Tue 25 Jun 2019 10:20 - 10:40 People: Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, Danfeng Zhang
… reduces the complexity of verification: for all of the algorithms we have evaluated …
A Fast Analytical Model of Fully Associative Caches
PLDI Research Papers When: Tue 25 Jun 2019 14:20 - 14:40 People: Tobias Gysi, Tobias Grosser, Laurin Brandner, Torsten Hoefler
… explicit enumeration of all memory accesses by using symbolic counting techniques …
LoCal: A Language for Programs Operating on Serialized Data
PLDI Research Papers When: Mon 24 Jun 2019 08:45 - 09:05 People: Michael Vollmer, Chaitanya S. Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, Ryan R. Newton
… -addressed layout of all heap values. We formalize LoCal and prove type safety …
Continuously Reasoning about Programs using Differential Bayesian Inference
PLDI Research Papers When: Tue 25 Jun 2019 10:20 - 10:40 People: Kihong Heo, Mukund Raghothaman, Xujie Si, Mayur Naik
… comprising 13k–112k lines of code. Drake enables to discover all true bugs …
Argosy: Verifying Layered Storage Systems with Recovery Refinement
PLDI Research Papers When: Wed 26 Jun 2019 09:10 - 09:30 People: Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
… , and these examples are all verified in the Coq proof assistant. …
SemCluster: Clustering of Imperative Programming Assignments Based on Quantitative Semantic Features
PLDI Research Papers When: Tue 25 Jun 2019 16:00 - 16:20 People: David Mitchel Perry, Dohyeong Kim, Roopsha Samanta, Xiangyu Zhang
… , all within a reasonable amount of time. …
Huron: Hybrid False Sharing Detection and Repair
PLDI Research Papers When: Tue 25 Jun 2019 08:30 - 08:50 People: Tanvir Ahmed Khan, Yifan Zhao, Gilles Pokam, Barzan Mozafari, Baris Kasikci
… more false sharing bugs than all state-of-the-art techniques, and with a lower …
Effective Floating-Point Analysis via Weak-Distance Minimization
PLDI Research Papers When: Tue 25 Jun 2019 09:10 - 09:30 People: Zhoulai Fu, Zhendong Su
… experiments, our boundary value analysis is able to find all reachable boundary conditions …