Sciweavers

APLAS
2011
ACM
12 years 11 months ago
Solving Recursion-Free Horn Clauses over LI+UIF
Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively auusing abstraction and refinement schemes that rely o...
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenk...
APLAS
2011
ACM
12 years 11 months ago
Constructing List Homomorphisms from Proofs
The well-known third list homomorphism theorem states that if a function h is both an instance of foldr and foldl, it is a list homomorphism. Plenty of previous works devoted to co...
Yun-Yan Chi, Shin-Cheng Mu
APLAS
2011
ACM
12 years 11 months ago
SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA
We present a new SPAS (ScalablePAth-Sensitive)framework for resolving points-to sets in C programs that exploits recent advances in pointer analysis. SPAS enables intraprocedural p...
Yulei Sui, Sen Ye, Jingling Xue, Pen-Chung Yew
PPNA
2011
13 years 2 months ago
Ad-hoc limited scale-free models for unstructured peer-to-peer networks
Several protocol efficiency metrics (e.g., scalability, search success rate, routing reachability and stability) depend on the capability of preserving structure even over the ch...
Durgesh Rani Kumari, Hasan Guclu, Murat Yuksel
PPL
2011
13 years 2 months ago
Mpi on millions of Cores
Petascale parallel computers with more than a million processing cores are expected to be available in a couple of years. Although MPI is the dominant programming interface today ...
Pavan Balaji, Darius Buntinas, David Goodell, Will...
POPL
2011
ACM
13 years 2 months ago
Precise reasoning for programs using containers
Containers are general-purpose data structures that provide functionality for inserting, reading, removing, and iterating over elements. Since many applications written in modern ...
Isil Dillig, Thomas Dillig, Alex Aiken
POPL
2011
ACM
13 years 2 months ago
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling pr...
Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Pe...
POPL
2011
ACM
13 years 2 months ago
Learning minimal abstractions
Percy Liang, Omer Tripp, Mayur Naik
POPL
2011
ACM
13 years 2 months ago
Mathematizing C++ concurrency
Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees ...
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewe...
POPL
2011
ACM
13 years 2 months ago
Decidable logics combining heap structures and data
We define a new logic, STRAND, that allows reasoning with heapmanipulating programs using deductive verification and SMT solvers. STRAND logic (“STRucture ANd Data” logic) f...
P. Madhusudan, Gennaro Parlato, Xiaokang Qiu