Synthesizing Imperative Programs from Examples Guided by Static Analysis
Abstract elided by the publisher.
26,098 papers · page 479 of 1,305
A Gradual Interpretation of Union Types
Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to u…
Modular Demand-Driven Analysis of Semantic Difference for Program Versions
Abstract elided by the publisher.
Incremental Analysis for Probabilistic Programs
Abstract elided by the publisher.
A compiler and verifier for page access oblivious computation
Trusted hardware primitives such as Intel's SGX instructions provide applications with a protected address space, called an enclave, for trusted code and data. However, building enclaves that preserve confidentiality of sensitive data continues to be a challenge. The developer mu…
Reasons and drawbacks of using trivial npm packages: the developers' perspective
Code reuse is traditionally seen as good practice. Recent trends have pushed the idea of code reuse to an extreme, by using packages that implement simple and trivial tasks, which we call ‘trivial packages’. A recent incident where a trivial package led to the breakdown of some o…
Why do developers use trivial packages? an empirical case study on npm
Code reuse is traditionally seen as good practice. Recent trends have pushed the concept of code reuse to an extreme, by using packages that implement simple and trivial tasks, which we call `trivial packages'. A recent incident where a trivial package led to the breakdown of som…
User- and analysis-driven context aware software development in mobile computing
Mobile applications may benefit from context awareness since they incur to context changes during their execution and their success depends on the user perceived quality. Context awareness requires context monitoring and system adaptation, these two tasks are very expensive espec…
Serverless computing: economic and architectural impact
Amazon Web Services unveiled their "Lambda" platform in late 2014. Since then, each of the major cloud computing infrastructure providers has released services supporting a similar style of deployment and operation, where rather than deploying and running monolithic services, or …
Model-based privacy and security analysis with CARiSMA
We present CARiSMA, a tool that is originally designed to support model-based security analysis of IT systems. In our recent work, we added several new functionalities to CARiSMA to support the privacy of personal data. Moreover, we introduced a mechanism to assist the system des…
ARTINALI: dynamic invariant detection for cyber-physical system security
Cyber-Physical Systems (CPSes) are being widely deployed in security critical scenarios such as smart homes and medical devices. Unfortunately, the connectedness of these systems and their relative lack of security measures makes them ripe targets for attacks. Specification-based…
On evidence preservation requirements for forensic-ready systems
Forensic readiness denotes the capability of a system to support digital forensic investigations of potential, known incidents by preserving in advance data that could serve as evidence explaining how an incident occurred. Given the increasing rate at which (potentially criminal)…
Model-level, platform-independent debugging in the context of the model-driven development of real-time systems
Providing proper support for debugging models at model-level is one of the main barriers to a broader adoption of Model Driven Development (MDD). In this paper, we focus on the use of MDD for the development of real-time embedded systems (RTE). We introduce a new platform-indepen…
Reproducing concurrency failures from crash stacks
Reproducing field failures is the first essential step for understanding, localizing and removing faults. Reproducing concurrency field failures is hard due to the need of synthesizing a test code jointly with a thread interleaving that induce the failure in the presence of limit…
Where is the bug and how is it fixed? an experiment with practitioners
Research has produced many approaches to automatically locate, explain, and repair software bugs. But do these approaches relate to the way practitioners actually locate, understand, and fix bugs? To help answer this question, we have collected a dataset named DBGBENCH --- the co…
Constraint normalization and parameterized caching for quantitative program analysis
Symbolic program analysis techniques rely on satisfiability-checking constraint solvers, while quantitative program analysis techniques rely on model-counting constraint solvers. Hence, the efficiency of satisfiability checking and model counting is crucial for efficiency of mode…
The care and feeding of wild-caught mutants
Mutation testing of a test suite and a program provides a way to measure the quality of the test suite. In essence, mutation testing is a form of sensitivity testing: by running mutated versions of the program against the test suite, mutation testing measures the suite's sensitiv…
When program analysis meets mobile security: an industrial study of misusing Android internet sockets
Despite recent progress in program analysis techniques to identify vulnerabilities in Android apps, significant challenges still remain for applying these techniques to large-scale industrial environments. Modern software-security providers, such as Qihoo 360 and Pwnzen (two lead…
Cherry-picking of code commits in long-running, multi-release software
This paper presents Tartarian, a tool that supports maintenance of software with long-running, multi-release branches in distributed version control systems. When new maintenance code, such as bug fixes and code improvement, is committed into a branch, it is likely that such code…
Adaptively generating high quality fixes for atomicity violations
It is difficult to fix atomicity violations correctly. Existing gate lock algorithm (GLA) simply inserts gate locks to serialize exe-cutions, which may introduce performance bugs and deadlocks. Synthesized context-aware gate locks (by Grail) require complex source code synthesis.…