Experience Developing and Deploying Concurrency Analysis at Facebook
Abstract elided by the publisher.
26,098 papers · page 438 of 1,305
New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair
Abstract elided by the publisher.
Efficiently Learning Safety Proofs from Appearance as well as Behaviours
Abstract elided by the publisher.
Invertible Linear Transforms of Numerical Abstract Domains
Abstract elided by the publisher.
Incremental Verification Using Trace Abstraction
Abstract elided by the publisher.
Volume-Based Merge Heuristics for Disjunctive Numeric Domains
Abstract elided by the publisher.
Interactive Verification of Distributed Protocols Using Decidable Logic
Abstract elided by the publisher.
Abstract Interpretation of CTL Properties
Abstract elided by the publisher.
Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction
Abstract elided by the publisher.
Improving IR-based bug localization with context-aware query reformulation
Recent findings suggest that Information Retrieval (IR)-based bug localization techniques do not perform well if the bug report lacks rich structured information (e.g., relevant program entity names). Conversely, excessive structured information (e.g., stack traces) in the bug re…
A formal verification tool for Ethereum VM bytecode
In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability log…
Salient-class location: help developers understand code change in code review
Code review involves a significant amount of human effort to understand the code change, because the information required to inspect code changes may distribute across multiple files that reviewers are not familiar with. Code changes are often organized as commits for review. In …
Detection of energy inefficiencies in Android wear watch faces
This work considers watch faces for Android Wear devices such as smartwatches. Watch faces are a popular category of apps that display current time and relevant contextual information. Our study of watch faces in an app market indicates that energy efficiency is a key concern for…
Practical AJAX race detection for JavaScript web applications
Asynchronous client-server communication is a common source of errors in JavaScript web applications. Such errors are difficult to detect using ordinary testing because of the nondeterministic scheduling of AJAX events. Existing automated event race detectors are generally too im…
Quality assurance automation in autonomous systems
Robots and autonomous systems are finding their way to interact with the public and failures in these systems could be extremely expensive, even deadly. However, low-cost software-based simulation could be a promising approach to systematically test robotics systems and prevent f…
Using finite-state models for log differencing
Much work has been published on extracting various kinds of models from logs that document the execution of running systems. In many cases, however, for example in the context of evolution, testing, or malware analysis, engineers are interested not only in a single log but in a s…
Dara: hybrid model checking of distributed systems
Building correct implementations of distributed systems continues to elude us. Solutions consist of abstract modeling languages such as TLA+, PLusCal, which specify models of systems and tools like Coq, and SPIN which verify correctness of models but require considerable amount o…
Themis: automatically testing software for discrimination
Bias in decisions made by modern software is becoming a common and serious problem. We present Themis, an automated test suite generator to measure two types of discrimination, including causal relationships between sensitive inputs and program behavior. We explain how Themis can…
Parameterized model counting for string and numeric constraints
Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present …
Towards a theory of software development expertise
Software development includes diverse tasks such as implementing new features, analyzing requirements, and fixing bugs. Being an expert in those tasks requires a certain set of skills, knowledge, and experience. Several studies investigated individual aspects of software developm…