Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
Simple and precise static analysis of untrusted Linux kernel extensions
- Elazar Gershuni,
- Nadav Amit,
- Arie Gurfinkel,
- Nina Narodytska,
- Jorge A. Navas,
- Noam Rinetzky,
- Leonid Ryzhyk,
- Mooly Sagiv
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 1069–1084https://doi.org/10.1145/3314221.3314590Extended Berkeley Packet Filter (eBPF) is a Linux subsystem that allows safely executing untrusted user-defined extensions inside the kernel. It relies on static analysis to protect the kernel against buggy and malicious extensions. As the eBPF ...
Modularity for decidability of deductive verification with applications to distributed systems
- Marcelo Taube,
- Giuliano Losa,
- Kenneth L. McMillan,
- Oded Padon,
- Mooly Sagiv,
- Sharon Shoham,
- James R. Wilcox,
- Doug Woos
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 662–677https://doi.org/10.1145/3192366.3192414Proof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve ...
Also Published in:
ACM SIGPLAN Notices: Volume 53 Issue 4- research-articleJune 2016
Ivy: safety verification by interactive generalization
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 614–630https://doi.org/10.1145/2908080.2908118Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system --- Ivy --- for interactively verifying safety of infinite-state systems. Ivy's key principle is ...
Also Published in:
ACM SIGPLAN Notices: Volume 51 Issue 6 - research-articleJune 2015
Composing concurrency control
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 240–249https://doi.org/10.1145/2737924.2737970Concurrency control poses significant challenges when composing computations over multiple data-structures (objects) with different concurrency-control implementations. We formalize the usually desired requirements (serializability, abort-safety, ...
Also Published in:
ACM SIGPLAN Notices: Volume 50 Issue 6 - research-articleJune 2014
VeriCon: towards verifying controller programs in software-defined networks
- Thomas Ball,
- Nikolaj Bjørner,
- Aaron Gember,
- Shachar Itzhaky,
- Aleksandr Karbyshev,
- Mooly Sagiv,
- Michael Schapira,
- Asaf Valadarsky
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 282–293https://doi.org/10.1145/2594291.2594317Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" software that operates independently from the network hardware, and ...
Also Published in:
ACM SIGPLAN Notices: Volume 49 Issue 6 - research-articleJune 2013
Concurrent libraries with foresight
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 263–274https://doi.org/10.1145/2491956.2462172Linearizable libraries provide operations that appear to execute atomically. Clients, however, may need to execute a sequence of operations (a composite operation) atomically. We consider the problem of extending a linearizable library to support ...
Also Published in:
ACM SIGPLAN Notices: Volume 48 Issue 6 - research-articleJune 2012
Concurrent data representation synthesis
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 417–428https://doi.org/10.1145/2254064.2254114We describe an approach for synthesizing data representations for concurrent programs. Our compiler takes as input a program written using concurrent relations and synthesizes a representation of the relations as sets of cooperating data structures as ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6 - research-articleJune 2012
JANUS: exploiting parallelism via hindsight
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 145–156https://doi.org/10.1145/2254064.2254083This paper addresses the problem of reducing unnecessary conflicts in optimistic synchronization. Optimistic synchronization must ensure that any two concurrently executing transactions that commit are properly synchronized. Conflict detection is an ...
Also Published in:
ACM SIGPLAN Notices: Volume 47 Issue 6 - research-articleJune 2011
Precise and compact modular procedure summaries for heap manipulating programs
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 567–577https://doi.org/10.1145/1993498.1993565We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our ...
Also Published in:
ACM SIGPLAN Notices: Volume 46 Issue 6 - research-articleJune 2011
Data representation synthesis
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 38–49https://doi.org/10.1145/1993498.1993504We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and ...
Also Published in:
ACM SIGPLAN Notices: Volume 46 Issue 6 - ArticleJune 2007
Thread-modular shape analysis
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationPages 266–277https://doi.org/10.1145/1250734.1250765We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap ...
Also Published in:
ACM SIGPLAN Notices: Volume 42 Issue 6 - ArticleMay 2003
CSSV: towards a realistic tool for statically detecting all buffer overflows in C
PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementationPages 155–167https://doi.org/10.1145/781131.781149Erroneous string manipulations are a major source of software defects in C programs yielding vulnerabilities which are exploited by software viruses. We present C String Static Verifyer (CSSV), a tool that statically uncovers all string manipulation ...
Also Published in:
ACM SIGPLAN Notices: Volume 38 Issue 5 - ArticleMay 2002
Deriving specialized program analyses for certifying component-client conformance
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementationPages 83–94https://doi.org/10.1145/512529.512540We are concerned with the problem of statically certifying (verifying) whether the client of a software component conforms to the component's constraints for correct usage. We show how conformance certification can be efficiently carried out in a staged ...
Also Published in:
ACM SIGPLAN Notices: Volume 37 Issue 5 - ArticleMay 2001
Heap profiling for space-efficient Java
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementationPages 104–113https://doi.org/10.1145/378795.378820We present a heap-profiling tool for exploring the potential for space savings in Java programs. The output of the tool is used to direct rewriting of application source code in a way that allows more timely garbage collection (GC) of objects, thus ...
Also Published in:
ACM SIGPLAN Notices: Volume 36 Issue 5