title: Exploiting Efficient Mapping and Pipelined Execution for Accelerating SpMV on Tensor Cores

authors:
Kaige Zhang
Hailong Yang
Xin You
Tianyu Feng
Yufan Xu
Zhongzhi Luan
Yi Liu
Depei Qian

abstract: Sparse matrix-vector multiplication (SpMV) is a fundamental operation in scientific computing, machine learning, and graph analytics, demanding efficient execution on modern hardware. Recent advances in hardware accelerators, such as Tensor Cores, have significantly improved the performance of many compute-intensive workloads. However, effectively utilizing Tensor Cores for SpMV remains challenging due to its irregular sparsity patterns and the mismatch between SpMV’s computational characteristics and constrained architecture design, leading to suboptimal performance and underutilization of Tensor Cores. In this paper, we systematically analyze the state-of-the-art SpMV optimizations on Tensor Cores, identify key performance bottlenecks, and propose Drawloom, a Tensor-Core-aware framework for SpMV with efficient Tensor Core mapping and optimized pipeline execution. Drawloom leverages a redesigned Tensor Core mapping strategy with a zig-zag chained sparse storage format, as well as a multi-stage register pipeline to better exploit hardware parallelism. Our evaluation on SuiteSparse dataset demonstrates that Drawloom outperforms cuSPARSE by 2.71×/1.90× (in FP16), 2.95×/2.39× (in FP32), and 2.47×/1.54× (in FP64) on A100 and H100 GPUs, respectively. Compared to the state-of-the-art SpMV implementations, Drawloom achieves a performance speedup of 1.26×/1.18× (in FP16) and 1.49×/1.56× (in FP64) on A100 and H100 GPUs, respectively.


venue: ppopp

title: HelixPipe: Efficient Distributed Training of Long Sequence Transformers with Attention Parallel Pipeline Parallelism

authors:
Geng Zhang
Shenggan Cheng
Xuanlei Zhao
Ziming Liu
Yang You

abstract: As transformer sequence lengths grow, existing pipeline parallelisms incur suboptimal performance due to the quadratic attention computation and the substantial memory overhead. To relieve these challenges, we propose HelixPipe, a novel pipeline parallelism for long sequence transformer training. First, HelixPipe introduces attention parallel partition, which schedules attention computations of different micro batches across different pipeline stages in parallel, reducing pipeline bubbles. Second, it employs a two-fold first-in-last-out micro batch schedule to balance memory usage and overlap communication with computation. Additionally, HelixPipe utilizes recomputation without attention and chunked MLP to mitigate fragmentation and enable longer sequences. Experiments demonstrate that HelixPipe gains increasing advantages with longer sequence lengths, and outperforms existing methods in throughput and scalability across varying pipeline sizes, model sizes, and cluster configurations. Notably, it achieves a 26% speedup over baseline methods when training a 7B model with 128k sequence length on 64 H20 GPUs. Code is available at https://github.com/zxgx/Megatron-LM.


title: Faster and Cheaper: Pushing the Sequence Alignment Throughput with Commercial CPUs

authors:
Zhonghai Zhang
Yewen Li
Ke Meng
Chunming Zhang
Guangming Tan

abstract: This paper proposes FastAlign, a faster, cheaper, and practical end-to-end solution for sequence alignment using commercial CPUs. It introduces two key innovations: a multi-stage seeding algorithm that improves search performance while maintaining low memory consumption, and an intra-query parallel seed-extension algorithm that eliminates redundancy and increases SIMD utilization. Evaluation results show that FastAlign achieves 2.27× ∼ 3.28× throughput speedup and 2.54× ∼ 5.65× cost reduction compared to state-of-the-art CPU and GPU baselines while guaranteeing 100% identical output to the de facto software BWA-MEM. FastAlign is open-sourced at https://github.com/zzhofict/BWA-FastAlign.git.


title: RoMeo: Mitigating Dual-dimensional Outliers with Rotated Mixed Precision Quantization

authors:
Qihao Zhang
Mingliang Tang
Mingshu Zhai
Kinman Lei
Jidong Zhai

abstract:
Mixed precision quantization has been adopted to accelerate large language models (LLMs) serving by leveraging high-throughput low-precision compute units in GPUs while preserving outliers in higher precision to maintain model accuracy. However, existing methods focus on mitigating single-dimensional channel-wise outliers, leading to model accuracy degradation when scaled to 4-bit precision.

In this paper, we present an algorithm-system co-design to effectively handle dual-dimensional outliers across both channel and token dimensions in LLMs. We introduce a novel rotation-based mixed precision quantization algorithm that suppresses and migrates channel-wise outliers to the token dimension. Based on this algorithm, we propose RoMeo, an efficient LLM serving system designed to overcome the unique system challenges posed by sparse computation pattern and dynamic outlier detection inherent in token-wise outlier handling. Extensive evaluations across various LLMs demonstrate that RoMeo improves quantized model accuracy by up to 5.17% compared to state-of-the-art methods QuaRot and MixQ, while maintaining efficiency comparable to uniform precision quantizations, achieving up to 2.10 × end-to-end speedup over half-precision baseline. RoMeo is available at https://github.com/thu-pacman/RoMeo.


title: PIM-zd-tree: A Fast Space-Partitioning Index Leveraging Processing-in-Memory

authors:
Yiwei Zhao
Hongbo Kang
Ziyang Men
Yan Gu
Guy E. Blelloch
Laxman Dhulipala
Charles McGuffey
Phillip B. Gibbons

abstract:
Space-partitioning indexes are widely used for managing multi-dimensional data, but their throughput is often memory-bottlenecked. Processing-in-memory (PIM), an emerging architectural paradigm, mitigates memory bottlenecks by embedding processing cores directly within memory modules, allowing computation to be offloaded to these PIM cores.

In this paper, we present PIM-zd-tree, the first space-partitioning index specifically designed for real-world PIM systems. PIM-zd-tree employs a tunable multi-layer structure, with each layer adopting distinct data layouts, partitioning schemes, and caching strategies. Its design is theoretically grounded to achieve load balance, minimal memory-channel communication, and low space overhead. To bridge theory and practice, we incorporate implementation techniques such as practical chunking and lazy counters. Evaluation on a real-world PIM system shows that PIM-zd-tree’s throughput is up to 4.25× and 99× higher than two state-of-the-art shared-memory baselines.


venue: sas

title: Constraint-Based Type Inference and Parametric Polymorphism


title: Directional Type Checking of Logic Programs

authors:
Alexander Aiken
T. K. Lakshman


title: Boolean Functions for Dependency Analysis: Algebraic Properties and Efficient Representation

authors:
Tania Armstrong
Kim Marriott
Peter Schachte
Harald Søndergaard


title: Stackability in the Simply-Typed Call-by-Value Lambda Calculus

authors:
Anindya Banerjee
David A. Schmidt


title: A Systematic Construction of Abstract Domains

authors:
Dmitri Boulanger
Maurice Bruynooghe


title: Deriving Polymorphic Type Dependencies for Logic Programs Using Multiple Incarnations of Prop

authors:
Michael Codish
Bart Demoen


title: Fast Strictness Analysis Via Symbolic Fixpoint Iteration


title: Estimating the Computational Cost of Logic Programs

authors:
Saumya K. Debray
Pedro López-García
Manuel V. Hermenegildo
Nai-Wei Lin

abstract: Information about the computational cost of programs is potentially useful for a variety of purposes, including selecting among different algorithms, guiding program transformations, in granularity control and mapping decisions in parallelizing compilers, and query optimization in deductive databases. Cost analysis of logic programs is complicated by nondeterminism: on the one hand, procedures can return multiple solutions, making it necessary to estimate the number of solutions in order to give nontrivial upper bound cost estimates; on the other hand, the possibility of failure has to be taken into account while estimating lower bounds. Here we discuss techniques to address these problems to some extent.


title: Uniqueness and Completeness Analysis of Array Comprehensions

authors:
David A. Garza-Salazar
A. P. Wim Böhm


title: The Costs and Benefits of Abstract Interpretation-driven Prolog Optimization


title: Generating Transformers for Deforestation and Supercompilation

authors:
Robert Glück
Jesper Jørgensen


title: Generalized Boxings, Congruences and Partial Inlining


title: Extracting Non-Strict Independent And-Parallelism Using Sharing and Freeness Information

authors:
Daniel Cabeza Gras
Manuel V. Hermenegildo

abstract: Logic programming systems which exploit and-parallelism among non-deterministic goals rely on notions of independence among those goals in order to ensure certain efficiency properties. “Non-strict” independence (NSI) is a more relaxed notion than the traditional notion of “strict” independence (SI) which still ensures the relevant efficiency properties and can allow considerable more parallelism than SI. However, all compilation technology developed to date has been based on SI, because of the intrinsic complexity of exploiting NSI. This paper fills this gap by developing a technique for compile-time detection of NSI. It also proposes algorithms for combined compile-time/run-time detection, presenting novel run-time checks for this type of parallelism. The approach is based on the knowledge of certain properties regarding the run-time instantiations of program variables —sharing and freeness— for which compile-time technology is available, with new approaches being currently proposed.


title: About Synchronous Programming and Abstract Interpretation


title: Verification of Linear Hybrid Systems by Means of Convex Approximations

authors:
Nicolas Halbwachs
Yann-Eric Proy
Pascal Raymond


title: A Type-based Framework for Program Analysis

authors:
Chris Hankin
Daniel Le Métayer


title: Mode Analysis of Functional Logic Programs

authors:
Michael Hanus
Frank Zartmann


title: From Processor Timing Specifications to Static Intruction Scheduling

authors:
Ed Harcourt
Jon Mauney
Todd A. Cook


title: Iterative Fixed Point Computation for Type-Based Strictness Analysis


title: Efficient Strictness Analysis of Haskell

authors:
Kristian Damm Jensen
Peter Hjæresen
Mads Rosendahl


title: Finding Fixpoints in Finite Function Spaces Using Neddedness Analysis and Chaotic Iteration


title: Mechanical Elimination of Commutative Redundancy

authors:
Hessam Khoshnevisan
Mohamad Afshar


title: Extended Analysis of Data Fields

authors:
Björn Lisper
Jean-Francois Collard


title: Abstract Interpretation Using TDGs


title: Efficient On-the-fly Analysis of Program Behavior and Static Cache Simulation

authors:
Frank Mueller
David B. Whalley


title: Strictness and Totality Analysis


title: Selective Thunkification

authors:
Paul Steckler
Mitchell Wand


title: Efficient FixPoint Computation

authors:
Bart Vergauwen
J. Wauman
Johan Lewi


title: Compile-time Detection of Uncaught Exceptions in Standard ML Programs


title: Generation of Efficient Interprocedural Analyzers with PAG

authors:
Martin Alt
Florian Martin


title: Optimality in Abstractions of Model Checking

authors:
Rance Cleaveland
S. Purushothaman Iyer
Daniel Yankelevich


title: Determining Storage Properties of Sequential and Concurrent Programs with Assignment and Structured Data


title: Partitioning Non-strict Functional Languages for Multi-threaded Code Generation


title: Complementation in Abstract Interpretation

authors:
Agostino Cortesi
Gilberto Filé
Roberto Giacobazzi
Catuscia Palamidessi
Francesco Ranzato


title: Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time

authors:
Dirk Dussart
Fritz Henglein
Christian Mossin


title: Optimizing Lazy Functional Programs Using Flow Inference


title: GENA - A Tool for Generating Prolog Analyzers from Specifications


title: Termination Analysis for Functional Programs using Term Orderings


title: A Type-based Analysis for Stack Allocation in Functional Languages


title: Control-Flow Analysis and Type Systems


title: Effective Flow Analysis for Avoiding Run-Time Checks

authors:
Suresh Jagannathan
Andrew K. Wright


title: Static Analysis of Communication for Asynchronous Concurrent Programming Languages

authors:
Naoki Kobayashi
Motoki Nakade
Akinori Yonezawa


title: Efficient Closure Utilisation by Higher-Order Inheritance Analysis


title: System F and Abstract Interpretation


title: Call-By-Name CPS-Translation as a Binding-Time Improvement

authors:
Kristian Nielsen
Morten Heine Sørensen


title: IGOR: A Tool for Developing Prolog Dataflow Analyzers

authors:
Magnus Nordin
Thomas Lindgren
Håkan Millroth


title: Trust in the lambda-Calculus

authors:
Jens Palsberg
Peter Ørbæk


title: LSign Reordered

authors:
Viswanath Ramachandran
Pascal Van Hentenryck


title: Unification-Free Execution of Well-Moded and Well-Typed Prolog Programs

authors:
M. R. K. Krishna Rao
R. K. Shyamasundar


title: Abstract Reduction Using a Tableau Calculus

authors:
Manfred Schmidt-Schauß
Sven Eric Panitz
Marko Schütz


title: Natural-Semantics-Based Abstract Interpretation (Preliminary Version)


title: Bigloo: A Portable and Optimizing Compiler for Strict Functional Languages

authors:
Manuel Serrano
Pierre Weis


title: Beyond Prototype Implementations: Polymorphic Projection Analysis for Glasgow Haskell


title: Region Inference for Higher-Order Functional Languages


title: Binding-Time Analysis and Strictness Analysis by Abstract Interpretation


title: An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract)

authors:
Pierre Wolper
Bernard Boigelot


title: Constraint-Based Program Analysis (Abstract)


title: Generalized Dominators for Structured Programs

authors:
Stephen Alstrup
Peter W. Lauridsen
Mikkel Thorup


title: Cache Behavior Prediction by Abstract Interpretation

authors:
Martin Alt
Christian Ferdinand
Florian Martin
Reinhard Wilhelm


title: Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language

authors:
Peter Holst Andersen
Carsten Kehler Holst


title: Proving Correctness of Constraint Logic Programs with Dynamic Scheduling

authors:
Frank S. de Boer
Maurizio Gabbrielli
Catuscia Palamidessi


title: Understanding Mobile Agents via a Non-Interleaving Semantics for Facile

authors:
Roberta Borgia
Pierpaolo Degano
Corrado Priami
Lone Leth Thomsen
Bent Thomsen


title: Termination Analysis for Partial Functions

authors:
Jürgen Brauburger
Jürgen Giesl


title: A Freeness and Sharing Analysis of Logic Programs Based on a Pre-interpretation

authors:
Maurice Bruynooghe
Bart Demoen
Dmitri Boulanger
Marc Denecker
Anne Mulkers


title: Refinement Types for Program Analysis

authors:
Mario Coppo
Ferruccio Damiani
Paola Giannini


title: A Comparison of Three Occur-Check Analysers

authors:
Lobel Crnogorac
Andrew D. Kelly
Harald Søndergaard


title: Analysis of the Equality Relations for the Program Terms


title: An Even Faster Solver for General Systems of Equations

authors:
Christian Fecht
Helmut Seidl


title: Inferring Program Specifications in Polynomial-Time


title: STAN: A Static Analyzer for CLP(R) Based on Abstract Interpretation


title: Two Applications of an Incremental Analysis Engine for (Constraint) Logic Programs

authors:
Andrew D. Kelly
Kim Marriott
Harald Søndergaard
Peter J. Stuckey


title: Automated Modular Termination Proofs for Real Prolog Programs

authors:
Martin Müller
Thomas Glaß
Karl Stroetmann


title: PAN - The Prolog Analyzer


title: Semantics-Directed Program Analysis: A Tool-Maker's Perspective


title: Data-Flow-Based Virtual Function Resolution

authors:
Hemant D. Pande
Barbara G. Ryder


title: Compiling Laziness Using Projections


title: Optimized Algorithms for Incremental Analysis of Logic Programs

authors:
Germán Puebla
Manuel V. Hermenegildo

abstract: Global analysis of logic programs can be performed effectively by the use of one of several existing efficient algorithms. However, the traditional global analysis scheme in which all the program code is known in advance and no previous analysis information is available is unsatisfactory in many situations. Incremental analysis of logic programs has been shown to be feasible and much more efficient in certain contexts than traditional (non-incremental) global analysis. However, incremental analysis poses additional requirements on the fixpoint algorithm used. In this work we identify these requirements, present an important class of strategies meeting the requirements, present sufficient a priori conditions for such strategies, and propose, implement, and evaluate experimentally a novel algorithm for incremental analysis based on these ideas. The experimental results show that the proposed algorithm performs very efficiently in the incremental case while being comparable to (and, in some cases, considerably better than) other state-of-the-art analysis algorithms even for the non-incremental case. We argue that our discussions, results, and experiments also shed light on some of the many tradeoffs involved in the design of algorithms for logic program analysis.


title: Tractable Constraints in Finite Semilattices

authors:
Jakob Rehof
Torben Æ. Mogensen


title: Uniformity for the Decidability of Hybrid Automata

authors:
Olivier F. Roux
Vlad Rusu


title: A Backward Slicing Algorithm for Prolog

authors:
Stéphane Schoenig
Mireille Ducassé


title: Combining Slicing and Constraint Solving for Validation of Measurement Software


title: Property-Oriented Expansion


title: Subtyping Constrained Types

authors:
Valery Trifonov
Scott F. Smith


title: Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs


title: Set-Sharing is Redundant for Pair-Sharing

authors:
Roberto Bagnara
Patricia M. Hill
Enea Zaffanella


title: Abstract Interpretation from Improving WAM Code

authors:
Dante Baldan
Gilberto Filé


title: True Concurrency via Abstract Interpretation

authors:
Chiara Bodei
Corrado Priami


title: The Power of QDDs (Extended Abstract)

authors:
Bernard Boigelot
Patrice Godefroid
Bernard Willems
Pierre Wolper


title: Automatic Termination Analysis for Partial Functions Using Polynomial Orderings


title: On the Desirable Link Between Theory and Practice in Abstract Interpretation (Extended Abstract)

authors:
Baudouin Le Charlier
Pierre Flener


title: An Algebraic Approach to Sharing Analysis of Logic Programs

authors:
Michael Codish
Vitaly Lagoon
Francisco Bueno


title: Attribute Grammars and Functional Programming Deforestation

authors:
Loïc Correnson
Étienne Duris
Didier Parigot
Gilles Roussel


title: Abstract Interpretation Based Static Analysis Parameterized by Semantics


title: Semantic Analyzer of Modula-Programs

authors:
Pavel G. Emelianov
Danil E. Baburin


title: Program Analysis Using Mixed Term and Set Constraints

authors:
Manuel Fähndrich
Alexander Aiken


title: Satisfying Subtype Inequalities in Polynomial Space


title: Static Analyses of Congruence Properties on Rational Numbers (Extended Abstract)


title: Can Abstract Interpretation Become a Mainstream Compiler Technology? (Abstract)


title: Effective Specialization of Realistic Programs via Use Sensitivity

authors:
Luke Hornof
Charles Consel
Jacques Noyé


title: Type-Based Analysis of Communication for Concurrent Programming Languages

authors:
Atsushi Igarashi
Naoki Kobayashi


title: Type-Directed Flow Analysis for Typed Intermediate Languages

authors:
Suresh Jagannathan
Stephen Weeks
Andrew K. Wright


title: Combining Abstract Interpretation and Partial Evaluation (Brief Overview)


title: Static Analysis of Interaction Nets for Distributed Implementations


title: Abstract Interpretation: A Theory of Approximate Computation


title: Exact Flow Analysis


title: TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language

authors:
Sven Eric Panitz
Manfred Schmidt-Schauß


title: On Sparse Evaluation Representations


title: Practical Compile-Time Analysis


title: Logical Optimality of Groundness Analysis


title: The Effects of the Precision of Pointer Analysis

authors:
Marc Shapiro
Susan Horwitz


title: Termination Analysis for Mercury

authors:
Chris Speirs
Zoltan Somogyi
Harald Søndergaard


title: Set-Based Analysis for Logic Programming and Tree Automata

authors:
Jean-Marc Talbot
Sophie Tison
Philippe Devienne


title: Data Dependence as Abstract Interpretations


title: Coalescing Conditional Branches into Efficient Indirect Jumps

authors:
Gang-Ryung Uh
David B. Whalley


title: Fast and Effective Procedure Inlining

authors:
Oscar Waddell
R. Kent Dybvig


title: Towards a Cost-Effective Estimation of Uncaught Exceptions in SML Programs

authors:
Kwangkeun Yi
Sukyoung Ryu


title: Denotational Abstract Interpretation of Functional Logic Programs


title: Improving Control in Functional Logic Program Specialization

authors:
Elvira Albert
María Alpuente
Moreno Falaschi
Pascual Julián Iranzo
Germán Vidal


title: Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation

authors:
Chiara Bodei
Pierpaolo Degano
Corrado Priami


title: Directional Type Inference for Logic Programs

authors:
Witold Charatonik
Andreas Podelski


title: Finite Subtype Inference with Explicit Polymorphism


title: Analysis of Normal Logic Programs

authors:
François Fages
Roberta Gori


title: A Tutorial on Domain Theory in Abstract Interpretation


title: Building Complete Abstract Interpretations in a Linear Logic-based Setting

authors:
Roberto Giacobazzi
Francesco Ranzato
Francesca Scozzari


title: Deriving Analysers by Folding/Unfolding of Natural Semantics and a Case Study: Slicing


title: A New Solution to the Hidden Copy Problem

authors:
Deepak Goyal
Robert Paige


title: On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines

authors:
Masami Hagiya
Akihiko Tozawa


title: Refining Static Analyses by Trace-Based Partitioning Using Control Flow

authors:
Maria Handjieva
Stanislav Tzolovski


title: The Correctness of Set-Sharing

authors:
Patricia M. Hill
Roberto Bagnara
Enea Zaffanella


title: Assessing the Effects of Flow-Sensitivity on Pointer Alias Analyses

authors:
Michael Hind
Anthony Pioli


title: Certifying, Optimizing Compilation (Abstract)


title: On the Power of Homeomorphic Embedding for Online Termination


title: A Symbolic Semantics for Abstract Model Checking


title: Analysis of Imperative Programs through Analysis of Constraint Logic Programs

authors:
Julio C. Peralta
John P. Gallagher
Hüseyin Saglam


title: Bidirectional Data Flow Analysis in Code Motion: Myth and Reality


title: Enabling Sparse Constant Propagation of Array Elements via Array SSA Form

authors:
Vivek Sarkar
Kathleen Knobe


title: Program Analysis as Model Checking of Abstract Interpretations

authors:
David A. Schmidt
Bernhard Steffen


title: Sparse Jacobian Computation in Automatic Differentiation by Static Program Analysis

authors:
Mohamed Tadjouddine
F. Eyssette
C. Faure


title: Automatic Determination of Communication Topologies in Mobile Systems


title: A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs


title: Static Analyses for Eliminating Unnecessary Synchronization from Java Programs

authors:
Jonathan Aldrich
Craig Chambers
Emin Gün Sirer
Susan J. Eggers


title: Binding-Time Analysis for Both Static and Dynamic Expressions


title: Polyhedral Analysis for Synchronous Languages

authors:
Frédéric Besson
Thomas P. Jensen
Jean-Pierre Talpin


title: State Space Reduction Based on Live Variables Analysis

authors:
Marius Bozga
Jean-Claude Fernandez
Lucian Ghirvu


title: Abstract Animator for Temporal Specifications: Application to TLA

authors:
Dominique Cansell
Dominique Méry


title: Equational Semantics

authors:
Loïc Correnson
Étienne Duris
Didier Parigot
Gilles Roussel


title: Abstract Interpretation of Mobile Ambients

authors:
René Rydhof Hansen
Jacob Grydholt Jensen
Flemming Nielson
Hanne Riis Nielson


title: A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives

authors:
John Hatcliff
James C. Corbett
Matthew B. Dwyer
Stefan Sokolowski
Hongjun Zheng


title: Freeness Analysis Through Linear Refinement

authors:
Patricia M. Hill
Fausto Spoto


title: Dynamic Partitioning in Analyses of Numerical Properties

authors:
Bertrand Jeannet
Nicolas Halbwachs
Pascal Raymond


title: A New Class of Functions for Abstract Interpretation

authors:
Jörg Köller
Markus Mohnen


title: Eliminating Dead Code on Recursive Data

authors:
Yanhong A. Liu
Scott D. Stoller


title: Binary Decision Graphs


title: On the Complexity Analysis of Static Analyses


title: Abstracting Cryptographic Protocols with Tree Automata


title: Model-Checking: A Tutorial Introduction

authors:
Markus Müller-Olm
David A. Schmidt
Bernhard Steffen


title: Detecting Equalities of Variables: Combining Efficiency with Precision

authors:
Oliver Rüthing
Jens Knoop
Bernhard Steffen


title: Tutorial: Techniques to Improve the Scalability and Precision of Data Flow Analysis


title: Translating Out of Static Single Assignment Form

authors:
Vugranam C. Sreedhar
Roy Dz-Ching Ju
David M. Gillies
Vatsa Santhanam


title: Partial Dead Code Elimination Using Extended Value Graph

authors:
Munehiro Takimoto
Kenichi Harada


title: Safety versus Secrecy


title: Static Analysis of Mega-Programs


title: Decomposing Non-redundant Sharing by Complementation

authors:
Enea Zaffanella
Patricia M. Hill
Roberto Bagnara


title: Abstract Interpretation Based Semantics of Sequent Calculi

authors:
Gianluca Amato
Giorgio Levi


title: A Transformational Approach for Generating Non-linear Invariants

authors:
Saddek Bensalem
Marius Bozga
Jean-Claude Fernandez
Lucian Ghirvu
Yassine Lakhnech


title: Deriving Parallel Codes via Invariants

authors:
Wei-Ngan Chin
Siau-Cheng Khoo
Zhenjiang Hu
Masato Takeichi


title: Safety of Strictness Analysis via Term Graph Rewriting

authors:
David Clark
Chris Hankin
Sebastian Hunt


title: Checking Cleanness in Linked Lists

authors:
Nurit Dor
Michael Rodeh
Shmuel Sagiv


title: Confidentiality Analysis of Mobile Systems

abstract: We propose an abstract interpretation-based analysis for automatically detecting all potential interactions between the agents of a part of a mobile system, without much knowledge about the rest of it.


title: Unified Analysis of Array and Object References in Strongly Typed Languages

authors:
Stephen J. Fink
Kathleen Knobe
Vivek Sarkar


title: Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C

authors:
Jeffrey S. Foster
Manuel Fähndrich
Alexander Aiken


title: Efficient Inference of Static Types for Java Bytecode

authors:
Etienne M. Gagnon
Laurie J. Hendren
Guillaume Marceau


title: Abstract Interpretation of Game Properties

authors:
Thomas A. Henzinger
Rupak Majumdar
Freddy Y. C. Mang
Jean-François Raskin


title: Enforcing Design Constraints with Object Logic


title: FULLDOC: A Full Reporting Debugger for Optimized Code

authors:
Clara Jaramillo
Rajiv Gupta
Mary Lou Soffa


title: Partial Redundancy Elimination on Predicated Code

authors:
Jens Knoop
Jean-Francois Collard
Roy Dz-Ching Ju


title: TVLA: A System for Implementing Static Analyses

authors:
Tal Lev-Ami
Shmuel Sagiv


title: Tree Schemata and Fair Termination


title: Abstract Interpretation of Probabilistic Semantics


title: Code Specialization Based on Value Profiles

authors:
Robert Muth
Scott A. Watterson
Saumya K. Debray


title: Model Checking as Constraint Solving


title: Flattening Is an Improvement

authors:
James Riely
Jan F. Prins


title: Model Checking Guided Abstraction and Analysis


title: Abstract Domains for Sharing Analysis by Optimal Semantics


title: Concurrency Analysis for Java

authors:
Cristian Ungureanu
Suresh Jagannathan


title: Finite-Tree Analysis for Constraint Logic-Based Languages

authors:
Roberto Bagnara
Roberta Gori
Patricia M. Hill
Enea Zaffanella


title: Communication and Parallelism Introduction and Elimination in Imperative Concurrent Programs

authors:
Miquel Bertran
Francesc-Xavier Babot
August Climent
Miquel Nicolau


title: Abstracting Cryptographic Protocols by Prolog Rules


title: Analyzing Fair Parametric Extended Automata

authors:
Ahmed Bouajjani
Aurore Collomb-Annichini
Yassine Lakhnech
Mihaela Sighireanu


title: Estimating the Impact of Scalable Pointer Analysis on Optimization

authors:
Manuvir Das
Ben Liblit
Manuel Fähndrich
Jakob Rehof


title: Cleanness Checking of String Manipulations in C Programs via Integer Analysis


title: Abstract Interpretation-Based Static Analysis of Mobile Ambients

abstract:
We use Abstract Interpretation to automatically prove safety properties of mobile ambients with name communications. We introduce a non-standard semantics in order to distinguish different recursive instances of agents. This allows us to specify explicitly both the link between agents and the ambient names they have declared, and the link between agents and the ambients they have activated.

Then we derive from this non-standard semantics an abstract semantics which focuses on interactions between agents. This abstract semantics describes non uniformly which agents can be launched in which ambients and which ambient names can be communicated to which agents. Such a description is required to prove security properties such as noninterference or confinement for instance.


title: Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking

authors:
Roberto Giacobazzi
Elisa Quintarelli


title: Effective Strictness Analysis with HORN Constraints

authors:
Kevin Glynn
Peter J. Stuckey
Martin Sulzmann


title: A Type and Effect Analysis of Security Protocols

authors:
Andrew D. Gordon
Alan Jeffrey


title: Static Analyses of the Precision of Floating-Point Operations


title: Using Slicing to Identify Duplication in Source Code

authors:
Raghavan Komondoor
Susan Horwitz


title: Applications of Extended Static Checking


title: An Abstract Interpretation Framework for Analysing Mobile Ambients

authors:
Francesca Levi
Sergio Maffeis


title: Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses

authors:
Donglin Liang
Mary Jean Harrold


title: Solving Regular Tree Grammar Based Constraints

authors:
Yanhong A. Liu
Ning Li
Scott D. Stoller


title: Parameterizing a Groundness Analysis of Logic Programs


title: Applying Static Analysis Techniques for Inferring Termination Conditions of Logic Programs

authors:
Frédéric Mesnard
Ulrich Neumerkel


title: An Abstract Analysis of the Probabilistic Termination of Programs


title: Security-Typed Languages and Distributed Computation


title: A Behavioral Module System for the Pi-Calculus

authors:
Sriram K. Rajamani
Jakob Rehof


title: Analysis of Multithreaded Programs


title: Language-Based Security: What's Needed and Why


title: Soft Scheduling for Hardware

authors:
Richard Sharp
Alan Mycroft


title: Embedding Chaos

authors:
Natalia Sidorova
Martin Steffen


title: Watchpoint Semantics: A Tool for Compositional and Focussed Static Analyses


title: Static Analysis and Software Assurance


title: Parametric Optimization of Open Real-Time Systems

authors:
Farn Wang
Hsu-Chun Yen


title: Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis

authors:
Stephen Adams
Thomas Ball
Manuvir Das
Sorin Lerner
Sriram K. Rajamani
Mark Seigle
Westley Weimer


title: Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library

authors:
Roberto Bagnara
Elisa Ricci
Enea Zaffanella
Patricia M. Hill


title: From Secrecy to Authenticity in Security Protocols


title: Reuse of Results in Termination Analysis of Typed Logic Programs

authors:
Maurice Bruynooghe
Michael Codish
Samir Genaim
Wim Vanhoof


title: An Improved Constraint-Based System for the Verification of Security Protocols

authors:
Ricardo Corin
Sandro Etalle


title: An Algebraic Approach to the Static Analysis of Concurrent Software


title: Representation Analysis for Coercion Placement


title: Refinement of LTL Formulas for Abstract Model Checking

authors:
María-del-Mar Gallardo
Pedro Merino
Ernesto Pimentel


title: States vs. Traces in Model Checking by Abstract Interpretation

authors:
Roberto Giacobazzi
Francesco Ranzato


title: Open Modeling in Multi-stakeholder Distributed Systems: Research and Tool Challenges


title: Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation


title: Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes


title: Pipeline Modeling for Timing Analysis

authors:
Marc Langenbach
Stephan Thesing
Reinhold Heckmann


title: Finiteness Analysis in Polynomial Time


title: Backward Type Inference Generalises Type Checking

authors:
Lunjin Lu
Andy King


title: Compactly Representing First-Order Structures for Static Analysis

authors:
Roman Manevich
G. Ramalingam
John Field
Deepak Goyal
Shmuel Sagiv


title: Static Analysis of the Numerical Stability of Loops


title: Semantics for Abstract Interpretation-Based Static Analyzes of Temporal Properties


title: Detecting Optimal Termination Conditions of Logic Programs

authors:
Frédéric Mesnard
Étienne Payet
Ulrich Neumerkel


title: A Few Graph-Based Relational Numerical Abstract Domains

abstract: This article presents the systematic design of a class of relational numerical abstract domains from non-relational ones. Constructed domains represent sets of invariants of the form (vj - vi ? C), where vj and vi are two variables, and C lives in an abstraction of P(Z), P(Q), or P(R). We will call this family of domains weakly relational domains. The underlying concept allowing this construction is an extension of potential graphs and shortest-path closure algorithms in exotic-like algebras.Example constructions are given in order to retrieve well-known domains as well as new ones. Such domains can then be used in the Abstract Interpretation framework in order to design various static analyses. A major benefit of this construction is its modularity, allowing to quickly implement new abstract domains from existing ones.


title: Polynomial Constants Are Decidable

authors:
Markus Müller-Olm
Helmut Seidl


title: Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi

authors:
Flemming Nielson
Hanne Riis Nielson
Helmut Seidl


title: Analysing Approximate Confinement under Uniform Attacks

authors:
Alessandra Di Pierro
Chris Hankin
Herbert Wiklicky


title: Modular Control Flow Analysis for Libraries


title: Making Abstract Model Checking Strongly Preserving

authors:
Francesco Ranzato
Francesco Tapparo


title: Static Program Analysis via 3-Valued Logic


title: Improving the Precision of Equality-Based Dataflow Analyses


title: Securing Communication in a Concurrent Language

authors:
Andrei Sabelfeld
Heiko Mantel


title: On Termination of Logic Programs with Floating Point Computations

authors:
Alexander Serebrenik
Danny De Schreye


title: More Precise Yet Efficient Type Inference for Logic Programs

authors:
Claudio Vaucheret
Francisco Bueno

abstract: Type analyses of logic programs which aim at inferring the types of the program being analyzed are presented in a unified abstract interpretation-based framework. This covers most classical abstract interpretation-based type analyzers for logic programs, built on either top-down or bottom-up interpretation of the program. In this setting, we discuss the widening operator, arguably a crucial one.We present a new widening which is more precise than those previously proposed. Practical results with our analysis domain are also presented, showing that it also allows for efficient analysis.


title: Guaranteed Optimization: Proving Nullspace Properties of Compilers

authors:
Todd L. Veldhuizen
Andrew Lumsdaine


title: Nonuniform Alias Analysis of Recursive Data Structures and Arrays


title: An Efficient Inclusion-Based Points-To Analysis for Strictly-Typed Languages

authors:
John Whaley
Monica S. Lam


title: Automated Verification of Concurrent Linked Lists with Counters

authors:
Tuba Yavuz-Kahveci
Tevfik Bultan


title: Security Typings by Abstract Interpretation


title: Computer-Assisted Verification of a Protocol for Certified Email

authors:
Martín Abadi
Bruno Blanchet


title: Precise Widening Operators for Convex Polyhedra

authors:
Roberto Bagnara
Patricia M. Hill
Elisa Ricci
Enea Zaffanella


title: A Logic for Analyzing Abstractions of Graph Transformation Systems

authors:
Paolo Baldan
Barbara König
Bernhard König


title: Modular Class Analysis with DATALOG

authors:
Frédéric Besson
Thomas P. Jensen


title: Checking Interference with Fractional Permissions


title: Message Analysis for Concurrent Languages

authors:
Richard Carlsson
Konstantinos Sagonas
Jesper Wilhelmsson


title: Stack Size Analysis for Interrupt-Driven Programs

authors:
Krishnendu Chatterjee
Di Ma
Rupak Majumdar
Tian Zhao
Thomas A. Henzinger
Jens Palsberg


title: Code Compaction of Matching Single-Entry Multiple-Exit Regions

authors:
Wen-Ke Chen
Bengu Li
Rajiv Gupta


title: Static Analysis of Accessed Regions in Recursive Data Structures

authors:
Stephen Chong
Radu Rugina


title: Precise Analysis of String Expressions

authors:
Aske Simon Christensen
Anders Møller
Michael I. Schwartzbach

abstract: We perform static analysis of Java programs to answer a simple question: which values may occur as results of string expressions? The answers are summarized for each expression by a regular language that is guaranteed to contain all possible values. We present several applications of this analysis, including statically checking the syntax of dynamically generated expressions, such as SQL queries. Our analysis constructs flow graphs from class files and generates a context-free grammar with a nonterminal for each string expression. The language of this grammar is then widened into a regular language through a variant of an algorithm previously used for speech recognition. The collection of resulting regular languages is compactly represented as a special kind of multi-level automaton from which individual answers may be extracted. If a program error is detected, examples of invalid strings are automatically produced. We present extensive benchmarks demonstrating that the analysis is efficient and produces results of useful precision.


title: Typestate Verification: Abstraction Techniques and Complexity Results

authors:
John Field
Deepak Goyal
G. Ramalingam
Eran Yahav


title: Client-Driven Pointer Analysis

authors:
Samuel Z. Guyer
Calvin Lin


title: Cartesian Factoring of Polyhedra in Linear Relation Analysis

authors:
Nicolas Halbwachs
David Merchat
Catherine Parent-Vigouroux


title: Program Development Using Abstract Interpretation (And The Ciao System Preprocessor)

authors:
Manuel V. Hermenegildo
Germán Puebla
Francisco Bueno
Pedro López-García


title: Z-Ranking: Using Statistical Analysis to Counter the Impact of Static Analysis Approximations

authors:
Ted Kremenek
Dawson R. Engler


title: Existential Heap Abstraction Entailment Is Undecidable

authors:
Viktor Kuncak
Martin C. Rinard


title: Inserting Safe Memory Reuse Commands into ML-Like Programs

authors:
Oukseh Lee
Hongseok Yang
Kwangkeun Yi


title: Type Systems for Distributed Data Sharing

authors:
Ben Liblit
Alex Aiken
Katherine A. Yelick


title: Class-Level Modular Analysis for Object Oriented Languages


title: Craig Interpolation and Reachability Analysis


title: Selective Tail Call Elimination


title: Abstract Interpretation of Programs as Markov Decision Processes


title: Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis

authors:
Thomas W. Reps
Stefan Schwoon
Somesh Jha


title: Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management

authors:
Ran Shaham
Eran Yahav
Elliot K. Kolodner
Shmuel Sagiv


title: Instantaneous Termination in Pure Esterel

authors:
Olivier Tardieu
Robert de Simone


title: Continuation-Based Partial Evaluation without Continuations


title: Loop Transformations for Reducing Data Space Requirements of Resource-Constrained Applications

authors:
Priya Unnikrishnan
Guangyu Chen
Mahmut T. Kandemir
Mustafa Karaköy
Ibrahim Kolcu


title: Information Flow Analysis in Logical Form

authors:
Torben Amtoft
Anindya Banerjee


title: The Blast Query Language for Software Verification

authors:
Dirk Beyer
Adam Chlipala
Thomas A. Henzinger
Ranjit Jhala
Rupak Majumdar


title: On Logics of Aliasing

authors:
Marius Bozga
Radu Iosif
Yassine Lakhnech


title: The Octahedron Abstract Domain

authors:
Robert Clarisó
Jordi Cortadella

abstract: An interesting area in static analysis is the study of numerical properties. Complex properties can be analyzed using abstract interpretation, provided that an adequate abstract domain is defined. Each domain can represent and manipulate a family of properties, providing a different trade-off between the precision and complexity of the analysis. The contribution of this paper is a new numerical abstract domain called octahedron that represents constraints of the form (@?x"[email protected]?x"j>=k). The implementation of octahedra is based on a new kind of decision diagram called Octahedron Decision Diagrams (OhDD).


title: Approximating the Algebraic Relational Semantics of Imperative Programs


title: Type Inference Against Races

authors:
Cormac Flanagan
Stephen N. Freund


title: A Polynomial-Time Algorithm for Global Value Numbering

authors:
Sumit Gulwani
George C. Necula


title: Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions


title: Static Analysis of Gated Data Dependence Graphs

authors:
Charles Hymans
Eben Upton


title: A Relational Approach to Interprocedural Shape Analysis

authors:
Bertrand Jeannet
Alexey Loginov
Thomas W. Reps
Shmuel Sagiv


title: Generalized Records and Spatial Conjunction in Role Logic

abstract: Role logic is a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-variable logic with counting and is therefore decidable.


title: Partially Disjunctive Heap Abstraction

authors:
Roman Manevich
Shmuel Sagiv
Ganesan Ramalingam
John Field


title: Towards Declarative Programming for Web Services


title: Spatial Analysis of BioAmbients

authors:
Hanne Riis Nielson
Flemming Nielson
Henrik Pilegaard


title: Bottom-Up and Top-Down Context-Sensitive Summary-Based Pointer Analysis

authors:
Erik M. Nystrom
Hong-Seok Kim
Wen-mei W. Hwu


title: Non-termination Inference for Constraint Logic Programs

authors:
Étienne Payet
Frédéric Mesnard


title: Completeness Refinement in Abstract Symbolic Trajectory Evaluation


title: An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants

authors:
Enric Rodríguez-Carbonell
Deepak Kapur


title: Shape Analysis Quantitative Shape Analysis


title: Constraint-Based Linear-Relations Analysis

authors:
Sriram Sankaranarayanan
Henny B. Sipma
Zohar Manna


title: Closed and Logical Relations for Over- and Under-Approximation of Powersets


title: Injecting Life with Computers


title: Program Generators and the Tools to Make Them


title: Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language

authors:
Qi Sun
Anindya Banerjee
David A. Naumann


title: Abstract Interpretation of Combinational Asynchronous Circuits

authors:
Sarah Thompson
Alan Mycroft


title: A Scalable Nonuniform Pointer Analysis for Embedded Programs


title: Pointer-Range Analysis

authors:
Suan Hsi Yong
Susan Horwitz


title: Algorithmic Game Semantics and Static Analysis


title: Widening Operators for Weakly-Relational Numeric Abstractions

authors:
Roberto Bagnara
Patricia M. Hill
Elena Mazzi
Enea Zaffanella


title: Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra

authors:
Roberto Bagnara
Enric Rodríguez-Carbonell
Enea Zaffanella


title: Inference of Well-Typings for Logic Programs with Application to Termination Analysis

authors:
Maurice Bruynooghe
John P. Gallagher
Wouter Van Humbeeck


title: Memory Space Conscious Loop Iteration Duplication for Reliable Execution

authors:
Guilin Chen
Mahmut T. Kandemir
Mustafa Karaköy


title: Memory Usage Verification for OO Programs

authors:
Wei-Ngan Chin
Huu Hai Nguyen
Shengchao Qin
Martin C. Rinard

abstract: We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that operate on these data structures. Key components of this type system include type assertions that use symbolic Presburger arithmetic expressions to capture data structure sizes, the effect of methods on the data structures that they manipulate, and the amount of memory that methods allocate and deallocate. For each method, we conservatively capture the amount of memory required to execute the method as a function of the sizes of the method's inputs. The safety guarantee is that the method will never attempt to use more memory than its type expressions specify. We have implemented a type checker to verify memory usages of OO programs. Our experience is that the type system can precisely and effectively capture memory bounds for a wide range of programs.


title: Abstraction Refinement for Termination

authors:
Byron Cook
Andreas Podelski
Andrey Rybalchenko


title: Data-Abstraction Refinement: A Game Semantic Approach

authors:
Aleksandar S. Dimovski
Dan R. Ghica
Ranko Lazic


title: Locality-Based Abstractions

authors:
Javier Esparza
Pierre Ganty
Stefan Schwoon


title: Type-Safe Optimisation of Plugin Architectures

authors:
Neal Glew
Jens Palsberg
Christian Grothoff


title: From Typed Process Calculi to Source-Based Security


title: Using Dependent Types to Certify the Safety of Assembly Code

authors:
Matthew Harren
George C. Necula


title: The PER Model of Abstract Non-interference

authors:
Sebastian Hunt
Isabella Mastroeni


title: A Relational Abstraction for Functions

authors:
Bertrand Jeannet
Denis Gopan
Thomas W. Reps


title: Taming False Alarms from a Domain-Unaware C Analyzer by a Bayesian Statistical Post Analysis

authors:
Yungbum Jung
Jaehwang Kim
Jaeho Shin
Kwangkeun Yi


title: Banshee: A Scalable Constraint-Based Analysis Toolkit

authors:
John Kodumal
Alex Aiken


title: A Generic Framework for Interprocedural Analysis of Numerical Properties

authors:
Markus Müller-Olm
Helmut Seidl


title: Finding Basic Block and Variable Correspondence

authors:
Iman Narasamdya
Andrei Voronkov


title: Boolean Heaps

authors:
Andreas Podelski
Thomas Wies


title: Interprocedural Shape Analysis for Cutpoint-Free Programs

authors:
Noam Rinetzky
Mooly Sagiv
Eran Yahav


title: Understanding the Origin of Alarms in Astrée


title: Pair-Sharing Analysis of Object-Oriented Programs

authors:
Stefano Secci
Fausto Spoto


title: Exploiting Sparsity in Polyhedral Analysis

authors:
Axel Simon
Andy King


title: Secure Information Flow as a Safety Problem

authors:
Tachio Terauchi
Alex Aiken


title: Static Analysis of String Manipulations in Critical Embedded C Programs

authors:
Xavier Allamigeon
Wenceslas Godard
Charles Hymans


title: Beyond Iteration Vectors: Instancewise Relational Abstract Domains

authors:
Pierre Amiranoff
Albert Cohen
Paul Feautrier


title: Specialized 3-Valued Logic Shape Analysis Using Structure-Based Refinement and Loose Embedding


title: Cryptographically-Masked Flows

authors:
Aslan Askarov
Daniel Hedin
Andrei Sabelfeld


title: Recency-Abstraction for Heap-Allocated Storage

authors:
Gogul Balakrishnan
Thomas W. Reps


title: Certificate Translation for Optimizing Compilers

authors:
Gilles Barthe
Benjamin Grégoire
César Kunz
Tamara Rezk


title: Proving the Properties of Communicating Imperfectly-Clocked Synchronous Systems


title: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

authors:
Ahmed Bouajjani
Peter Habermehl
Adam Rogalewicz
Tomás Vojnar


title: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

authors:
Cristiano Calcagno
Dino Distefano
Peter W. O'Hearn
Hongseok Yang


title: Analysis of Low-Level Code Using Cooperating Decompilers

authors:
Bor-Yuh Evan Chang
Matthew Harren
George C. Necula


title: Parametric and Termination-Sensitive Control Dependence

authors:
Feng Chen
Grigore Rosu


title: Unleashing the Power of Static Analysis


title: Path-Sensitive Dataflow Analysis with Iterative Refinement

authors:
Dinakar Dhurjati
Manuvir Das
Yue Yang


title: Combining Widening and Acceleration in Linear Relation Analysis

authors:
Laure Gonnord
Nicolas Halbwachs


title: Interprocedural Shape Analysis with Separated Heap Abstractions

authors:
Alexey Gotsman
Josh Berdine
Byron Cook


title: Static Analysis of Numerical Algorithms

authors:
Eric Goubault
Sylvie Putot


title: Catching and Identifying Bugs in Register Allocation

authors:
Yuqiang Huang
Bruce R. Childers
Mary Lou Soffa


title: Structural Invariants

authors:
Ranjit Jhala
Rupak Majumdar
Ru-Gang Xu


title: Static Analysis for Java Servlets and JSP

authors:
Christian Kirkegaard
Anders Møller

abstract: We present an approach for statically reasoning about the behavior of Web applications that are developed using Java Servlets and JSP. Specifically, we attack the problems of guaranteeing that all output is well-formed and valid XML and ensuring consistency of XHTML form fields and session state. Our approach builds on a collection of program analysis techniques developed earlier in the JWIG and Xact projects, combined with work on balanced context-free grammars. Together, this provides the necessary foundation concerning reasoning about output streams and application control flow.


title: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm

authors:
Alexey Loginov
Thomas W. Reps
Mooly Sagiv


title: Separation Logic and Program Analysis


title: Memory Leak Analysis by Contradiction

authors:
Maksim Orlovich
Radu Rugina


title: Existential Label Flow Inference Via CFL Reachability

authors:
Polyvios Pratikakis
Jeffrey S. Foster
Michael Hicks


title: Abstract Interpretation with Specialized Definitions

authors:
Germán Puebla
Elvira Albert
Manuel V. Hermenegildo

abstract: The relationship between abstract interpretation and partial evaluation has received considerable attention and (partial) integrations have been proposed starting from both the partial evaluation and abstract interpretation perspectives. In this work we present what we argue is the first generic algorithm for efficient and precise integration of abstract interpretation and partial evaluation from an abstract interpretation perspective. Taking as starting point state-of-the-art algorithms for context-sensitive, polyvariant abstract interpretation and (abstract) partial evaluation of logic programs, we present an algorithm which combines the best of both worlds. Key ingredients include the accurate success propagation inherent to abstract interpretation and the powerful program transformations achievable by partial deduction. In our algorithm, the calls which appear in the analysis graph are not analyzed w.r.t. the original definition of the procedure but w.r.t. specialized definitions of these procedures. Such specialized definitions are obtained by applying both unfolding and abstract executability. Also, our framework is parametric w.r.t. different control strategies and abstract domains. Different combinations of these parameters correspond to existing algorithms for program analysis and specialization. Our approach efficiently computes strictly more precise results than those achievable by each of the individual techniques. The algorithm is one of the key components of CiaoPP, the analysis and specialization system of the Ciao compiler.


title: Static Analysis in Disjunctive Numerical Domains

authors:
Sriram Sankaranarayanan
Franjo Ivancic
Ilya Shlyakhter
Aarti Gupta


title: Underapproximating Predicate Transformers


title: Shape Analysis for Low-Level Code


title: A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware

authors:
Francesco Banterle
Roberto Giacobazzi


title: Static Analysis of Dynamic Communication Systems by Partner Abstraction

authors:
Jörg Bauer
Reinhard Wilhelm


title: Formalised Inductive Reasoning in the Logic of Bunched Implications


title: Footprint Analysis: A Shape Analysis That Discovers Preconditions

authors:
Cristiano Calcagno
Dino Distefano
Peter W. O'Hearn
Hongseok Yang


title: Modular Safety Checking for Fine-Grained Concurrency

authors:
Cristiano Calcagno
Matthew J. Parkinson
Viktor Vafeiadis


title: Shape Analysis with Structural Invariant Checkers

authors:
Bor-Yuh Evan Chang
Xavier Rival
George C. Necula


title: A Compilation Model for Aspect-Oriented Polymorphically Typed Functional Languages

authors:
Kung Chen
Shu-Chun Weng
Meng Wang
Siau-Cheng Khoo
Chung-Hsin Chen


title: Fixpoint-Guided Abstraction Refinements

authors:
Patrick Cousot
Pierre Ganty
Jean-François Raskin


title: Astrée: From Research to Industry

authors:
David Delmas
Jean Souyris


title: Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification

authors:
Tristan Le Gall
Bertrand Jeannet


title: Guided Static Analysis

authors:
Denis Gopan
Thomas W. Reps


title: Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic

authors:
Eric Goubault
Sylvie Putot


title: Exploiting Pointer and Location Equivalence to Optimize Pointer Analysis

authors:
Ben Hardekopf
Calvin Lin


title: Hierarchical Pointer Analysis for Distributed Programs

authors:
Amir Kamil
Katherine A. Yelick


title: Abstract Error Projection

authors:
Akash Lal
Nicholas Kidd
Thomas W. Reps
Tayssir Touili


title: Accelerated Data-Flow Analysis

authors:
Jérôme Leroux
Grégoire Sutre

abstract: Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.


title: Arithmetic Strengthening for Shape Analysis

authors:
Stephen Magill
Josh Berdine
Edmund M. Clarke
Byron Cook


title: Precise Thread-Modular Verification

authors:
Alexander Malkis
Andreas Podelski
Andrey Rybalchenko


title: Semantics-Based Transformation of Arithmetic Expressions


title: Optimal Abstraction on Real-Valued Programs


title: Programming Language Design and Analysis Motivated by Hardware Evolution


title: A Framework for End-to-End Verification and Evaluation of Register Allocators

authors:
V. Krishna Nandivada
Fernando Magno Quintão Pereira
Jens Palsberg


title: Magic-Sets Transformation for the Analysis of Java Bytecode

authors:
Étienne Payet
Fausto Spoto


title: Program Analysis Using Symbolic Ranges

authors:
Sriram Sankaranarayanan
Franjo Ivancic
Aarti Gupta


title: Compositional Verification and 3-Valued Abstractions Join Forces

authors:
Sharon Shoham
Orna Grumberg


title: Taming the Wrapping of Integer Arithmetic

authors:
Axel Simon
Andy King


title: Refactoring Using Type Constraints


title: A New Algorithm for Identifying Loops in Decompilation

authors:
Tao Wei
Jian Mao
Wei Zou
Yu Chen


title: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis

authors:
Elvira Albert
Puri Arenas
Samir Genaim
Germán Puebla

abstract: The classical approach to automatic cost analysis consists of two phases. Given a program and some measure of cost, we first produce recurrence relations(RRs) which capture the cost of our program in terms of the size of its input data. Second, we convert such RRs into closed form(i.e., without recurrences). Whereas the first phase has received considerable attention, with a number of cost analyses available for a variety of programming languages, the second phase has received comparatively little attention. In this paper we first study the features of RRs generated by automatic cost analysis and discuss why existing computer algebra systems are not appropriate for automatically obtaining closed form solutions nor upper bounds of them. Then we present, to our knowledge, the first practical framework for the fully automatic generation of reasonably accurate upper bounds of RRs originating from cost analysis of a wide range of programs. It is based on the inference of ranking functionsand loop invariantsand on partial evaluation.


title: Inferring Min and Max Invariants Using Max-Plus Polyhedra

authors:
Xavier Allamigeon
Stephane Gaubert
Eric Goubault


title: SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement

authors:
Gogul Balakrishnan
Sriram Sankaranarayanan
Franjo Ivancic
Ou Wei
Aarti Gupta


title: Relational Analysis of Correlation

authors:
Jörg Bauer
Flemming Nielson
Hanne Riis Nielson
Henrik Pilegaard


title: On Polymorphic Recursion, Type Systems, and Abstract Interpretation

authors:
Marco Comini
Ferruccio Damiani
Samuel Vrech


title: Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

authors:
Christopher L. Conway
Dennis Dams
Kedar S. Namjoshi
Clark W. Barrett


title: Transforming Abstract Interpretations by Abstract Interpretation

authors:
Roberto Giacobazzi
Isabella Mastroeni


title: Flow Analysis, Linearity, and PTIME

authors:
David Van Horn
Harry G. Mairson

abstract:
Flow analysis is a ubiquitous and much-studied component of compiler technology--and its variations abound. Amongst the most well known is Shivers' 0CFA; however, the best known algorithm for 0CFA requires time cubic in the size of the analyzed program and is unlikely to be improved. Consequently, several analyses have been designed to approximate 0CFA by trading precision for faster computation. Henglein's simple closure analysis, for example, forfeits the notion of directionality in flows and enjoys an "almost linear" time algorithm. But in making trade-offs between precision and complexity, what has been given up and what has been gained? Where do these analyses differ and where do they coincide?

We identify a core language--the linear i¾?-calculus--where 0CFA, simple closure analysis, and many other known approximations or restrictions to 0CFA are rendered identical. Moreover, for this core language, analysis corresponds with (instrumented) evaluation. Because analysis faithfully captures evaluation, and because the linear i¾?-calculus is complete for ptime , we derive ptime -completeness results for all of these analyses.


title: Language Strength Reduction

authors:
Nicholas Kidd
Akash Lal
Thomas W. Reps


title: Solving Multiple Dataflow Queries Using WPDSs

authors:
Akash Lal
Thomas W. Reps


title: Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors

authors:
Peter Lammich
Markus Müller-Olm


title: Convex Hull of Arithmetic Automata

abstract: Arithmetic automata recognize infinite words of digits denoting decompositions of real and integer vectors. These automata are known expressive and efficient enough to represent the whole set of solutions of complex linear constraints combining both integral and real variables. In this paper, the closed convex hull of arithmetic automata is proved rational polyhedral. Moreover an algorithm computing the linear constraints defining these convex set is provided. Such an algorithm is useful for effectively extracting geometrical properties of the whole set of solutions of complex constraints symbolically represented by arithmetic automata.


title: Reflections on the Role of Static Analysis in Cooperative Bug Isolation


title: Heap Decomposition for Concurrent Shape Analysis

authors:
Roman Manevich
Tal Lev-Ami
Mooly Sagiv
Ganesan Ramalingam
Josh Berdine


title: A Calculational Approach to Control-Flow Analysis by Abstract Interpretation

authors:
Jan Midtgaard
Thomas P. Jensen


title: Modal Abstractions of Concurrent Behaviour

authors:
Sebastian Nanz
Flemming Nielson
Hanne Riis Nielson


title: Quantum Entanglement Analysis Based on Abstract Interpretation

abstract: Entanglement is a non local property of quantum states which has no classical counterpart and plays a decisive role in quantum information theory. Several protocols, like the teleportation, are based on quantum entangled states. Moreover, any quantum algorithm which does not create entanglement can be efficiently simulated on a classical computer. The exact role of the entanglement is nevertheless not well understood. Since an exact analysis of entanglement evolution induces an exponential slowdown, we consider approximative analysis based on the framework of abstract interpretation. In this paper, a concrete quantum semantics based on superoperators is associated with a simple quantum programming language. The representation of entanglement, i.e. the design of the abstract domain is a key issue. A representation of entanglement as a partition of the memory is chosen. An abstract semantics is introduced, and the soundness of the approximation is proven.


title: Reasoning about Control Flow in the Presence of Transient Faults

authors:
Frances Perry
David Walker


title: Field Flow Sensitive Pointer and Escape Analysis for Java Using Heap Array SSA

authors:
Prakash Prabhu
Priti Shankar


title: Hiding Software Watermarks in Loop Structures

authors:
Mila Dalla Preda
Roberto Giacobazzi
Enrico Visentini


title: Protocol Inference Using Static Path Profiles

authors:
Murali Krishna Ramanathan
Koushik Sen
Ananth Grama
Suresh Jagannathan


title: Typing Linear Constraints for Moding CLP() Programs

authors:
Salvatore Ruggieri
Frédéric Mesnard


title: Analysing All Polynomial Equations in

authors:
Helmut Seidl
Andrea Flexeder
Michael Petter


title: Splitting the Control Flow with Boolean Flags


title: Algorithmic Program Synthesis with Partial Programs and Decision Procedures


title: Proving the Correctness of the Implementation of a Control-Command Algorithm


title: Increasing the Scope and Resolution of Interprocedural Static Single Assignment

authors:
Silvian Calman
Jianwen Zhu


title: Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships

authors:
Liqian Chen
Antoine Miné
Ji Wang
Patrick Cousot


title: Abstract Parsing: Static Analysis of Dynamically Generated String Output Using LR-Parsing Technology

authors:
Kyung-Goo Doh
Hyunha Kim
David A. Schmidt


title: Creating Transformations for Matrix Obfuscation

authors:
Stephen Drape
Irina Voiculescu


title: Invariant Checking for Programs with Procedure Calls

authors:
Guillem Godoy
Ashish Tiwari


title: Abstract Interpretation of FIFO Replacement

authors:
Daniel Grund
Jan Reineke


title: Bottom-Up Shape Analysis

authors:
Bhargav S. Gulavani
Supratik Chakraborty
Ganesan Ramalingam
Aditya V. Nori


title: Refinement of Trace Abstraction

authors:
Matthias Heizmann
Jochen Hoenicke
Andreas Podelski


title: Automatic Parallelization and Optimization of Programs by Proof Rewriting

abstract: We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating proof trees and a rewrite system on proof trees.


title: Type Analysis for JavaScript

authors:
Simon Holm Jensen
Anders Møller
Peter Thiemann


title: A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination

authors:
David Niedzielski
Jeffery von Ronne
Andreas Gampe
Kleanthis Psarris


title: Algorithmic Verification of Systems Software Using SMT Solvers


title: Abstract Interpretation from a Topological Perspective


title: Abstraction Refinement for Quantified Array Assertions

authors:
Mohamed Nassim Seghir
Andreas Podelski
Thomas Wies


title: Region Analysis for Race Detection

authors:
Helmut Seidl
Vesal Vojdani


title: Optimizing Pointer Analysis Using Bisimilarity


title: The Complexity of Andersen's Analysis in Practice

authors:
Manu Sridharan
Stephen J. Fink


title: Inter-program Properties

authors:
Andrei Voronkov
Iman Narasamdya


title: The Causal Graph Revisited for Directed Model Checking

authors:
Martin Wehrle
Malte Helmert


title: Inferring Dataflow Properties of User Defined Table Processors

authors:
Songtao Xia
Manuel Fähndrich
Francesco Logozzo


title: Polymorphic Fractional Capabilities

authors:
Hirotoshi Yasuoka
Tachio Terauchi


title: From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis

authors:
Elvira Albert
Puri Arenas
Samir Genaim
German Puebla
Diana V. Ramírez-Deantes

abstract: Static analysis which takes into account the value of data stored in the heap is typically considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields (or fields for short), i.e., they are field-insensitive. In this paper, we propose locality conditions for soundly converting fields into local variables. This way, field-insensitive analysis over the transformed program can infer information on the original fields. Our notion of locality is context-sensitive and can be applied both to numeric and reference fields. We propose then a polyvariant transformation which actually converts object fields meeting the locality condition into variables and which is able to generate multiple versions of code when this leads to increasing the amount of fields which satisfy the locality conditions. We have implemented our analysis within a termination analyzer for Java bytecode.


title: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

authors:
Christophe Alias
Alain Darte
Paul Feautrier
Laure Gonnord


title: Deriving Numerical Abstract Domains via Principal Component Analysis

authors:
Gianluca Amato
Maurizio Parton
Francesca Scozzari


title: Concurrent Separation Logic for Pipelined Parallelization

authors:
Christian J. Bell
Andrew W. Appel
David Walker


title: Automatic Abstraction for Intervals Using Boolean Formulae

authors:
Jörg Brauer
Andy King


title: Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables

abstract: The design of embedded control systems is mainly done with model-based tools such as Matlab/Simulink. Numerical simulation is the central technique of development and verification of such tools. Floatingpoint arithmetic, which is well-known to only provide approximated results, is omnipresent in this activity. In order to validate the behaviors of numerical simulations using abstract interpretation-based static analysis, we present, theoretically and with experiments, a new partially relational abstract domain dedicated to floating-point variables. It comes from interval expansion of non-linear functions using slopes and it is able to mimic all the behaviors of the floating-point arithmetic. Hence it is adapted to prove the absence of run-time errors or to analyze the numerical precision of embedded control systems.


title: A Shape Analysis for Non-linear Data Structures

authors:
Renato Cherini
Lucas Rearte
Javier O. Blanco


title: Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis

authors:
Isil Dillig
Thomas Dillig
Alex Aiken


title: Time of Time


title: Static Verification for Code Contracts


title: Compositional Bitvector Analysis for Concurrent Programs with Nested Locks

authors:
Azadeh Farzan
Zachary Kincaid


title: Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely

authors:
Thomas Martin Gawlitza
Helmut Seidl


title: Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework - In Memory of Amir Pnueli


title: Boxes: A Symbolic Abstract Domain of Boxes

authors:
Arie Gurfinkel
Sagar Chaki


title: Alternation for Termination

authors:
William R. Harris
Akash Lal
Aditya V. Nori
Sriram K. Rajamani


title: Size-Change Termination and Transition Invariants

authors:
Matthias Heizmann
Neil D. Jones
Andreas Podelski


title: Verifying a Local Generic Solver in Coq

authors:
Martin Hofmann
Aleksandr Karbyshev
Helmut Seidl


title: Interprocedural Analysis with Lazy Propagation

authors:
Simon Holm Jensen
Anders Møller
Peter Thiemann


title: Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods

authors:
Joost-Pieter Katoen
Annabelle McIver
Larissa Meinicke
Carroll C. Morgan


title: Using Static Analysis in Space: Why Doing so?


title: Thread-Modular Counterexample-Guided Abstraction Refinement

authors:
Alexander Malkis
Andreas Podelski
Andrey Rybalchenko


title: Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods

authors:
Nadir Matringe
Arnaldo Vieira Moura
Rachid Rebiha


title: Statically Inferring Complex Heap, Array, and Numeric Invariants

authors:
Bill McCloskey
Thomas W. Reps
Mooly Sagiv


title: Abstract Interpreters for Free


title: Points-to Analysis as a System of Linear Equations

authors:
Rupesh Nasre
Ramaswamy Govindarajan


title: Modelling Metamorphism by Abstract Interpretation

authors:
Mila Dalla Preda
Roberto Giacobazzi
Saumya K. Debray
Kevin Coogan
Gregg M. Townsend


title: Strictness Meets Data Flow

authors:
Tom Schrijvers
Alan Mycroft


title: Automatic Verification of Determinism for Structured Parallel Programs

authors:
Martin T. Vechev
Eran Yahav
Raghavan Raman
Vivek Sarkar


title: An Abstraction-Refinement Framework for Trigger Querying

authors:
Guy Avni
Orna Kupferman


title: The Flow-Insensitive Precision of Andersen's Analysis in Practice

authors:
Sam Blackshear
Bor-Yuh Evan Chang
Sriram Sankaranarayanan
Manu Sridharan


title: On Sequentializing Concurrent Programs

authors:
Ahmed Bouajjani
Michael Emmi
Gennaro Parlato

abstract: We propose a general framework for compositional under-approximate concurrent program analyses by reduction to sequential program analyses--so-called sequentializations. We notice the existing sequentializations--based on bounding the number of execution contexts, execution rounds, or delays from a deterministic task-schedule--rely on three key features for scalable concurrent program analyses: (i) reduction to the sequential program model, (ii) compositional reasoning to avoid expensive task-product constructions, and (iii) parameterized exploration bounds. To understand how those sequentializations can be unified and generalized, we define a general framework which preserves their key features, and in which those sequentializations are particular instances. We also identify a most general instance which considers more executions, by composing the rounds of different tasks in any order, restricted only by the unavoidable program and task-creation causality orders. In fact, we show this general instance is fundamentally more powerful by identifying an infinite family of state-reachability problems (to states g1, g2, ...) which can be answered precisely with a fixed exploration bound, whereas the existing sequentializations require an increasing bound k to reach each gk. Our framework applies to a general class of shared-memory concurrent programs, with dynamic task-creation and arbitrary preemption.


title: Software Verification Using k-Induction

authors:
Alastair F. Donaldson
Leopold Haller
Daniel Kroening
Philipp Rümmer


title: Abstract Domains of Affine Relations

authors:
Matt Elder
Junghee Lim
Tushar Sharma
Tycho Andersen
Thomas W. Reps


title: Probabilistic Abstractions with Arbitrary Domains

authors:
Javier Esparza
Andreas Gaiser

abstract: Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently introduced by Gulavani et al., that can use arbitrary abstract domains and widening operators (in the sense of Abstract Interpretation). We show how suitable widening operators can deduce loop invariants difficult to find for predicate abstraction, and propose refinement techniques.


title: Formal Model Reduction

abstract: Modelers of molecular signaling networks must cope with the combinatorial explosion of protein states generated by post-translational modifications and complex formations. Rule-based models provide a powerful alternative to approaches that require an explicit enumeration of all possible molecular species of a system [1,2]. Such models consist of formal rules stipulating the (partial) contexts for specific protein-protein interactions to occur. The behavior of the models can be formally described by stochastic or differential semantics. Yet, the naive computation of these semantics does not scale to large systems, because it does not exploit the lower resolution at which rules specify interactions.


title: Side-Effect Analysis of Assembly Code

authors:
Andrea Flexeder
Michael Petter
Helmut Seidl


title: Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation

authors:
Patrice Godefroid
Shuvendu K. Lahiri
Cindy Rubio-González


title: The Complexity of Abduction for Separated Heap Abstractions

authors:
Nikos Gorogiannis
Max I. Kanovich
Peter W. O'Hearn


title: An Efficient Static Trace Simplification Technique for Debugging Concurrent Programs

authors:
Jeff Huang
Charles Zhang


title: Astrée: Design and Experience


title: Directed Symbolic Execution

authors:
Kin-Keung Ma
Yit Phang Khoo
Jeffrey S. Foster
Michael Hicks


title: Purity Analysis: An Abstract Interpretation Formulation

authors:
Ravichandhran Madhavan
Ganesan Ramalingam
Kapil Vaswani


title: Efficient Decision Procedures for Heaps Using STRAND

authors:
P. Madhusudan
Xiaokang Qiu


title: Widening and Interpolation


title: Invisible Invariants and Abstract Interpretation

authors:
Kenneth L. McMillan
Lenore D. Zuck


title: A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs

authors:
Matthew Might
David Van Horn

abstract: We develop a framework for computing two foundational analyses for concurrent higher-order programs: (control-)flow analysis (CFA) and may-happen-in-parallel analysis (MHP). We pay special attention to the unique challenges posed by the unrestricted mixture of first-class continuations and dynamically spawned threads. To set the stage, we formulate a concrete model of concurrent higher-order programs: the P(CEK*)S machine. We find that the systematic abstract interpretation of this machine is capable of computing both flow and MHP analyses. Yet, a closer examination finds that the precision for MHP is poor. As a remedy, we adapt a shape analytic technique--singleton abstraction--to dynamically spawned threads (as opposed to objects in the heap). We then show that if MHP analysis is not of interest, we can substantially accelerate the computation of flow analysis alone by collapsing thread interleavings with a second layer of abstraction.


title: Probabilistically Accurate Program Transformations

authors:
Sasa Misailovic
Daniel M. Roy
Martin C. Rinard

abstract:
The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces.

Our new approach produces probabilistic guarantees of the form P(|D| ≥ B) ≤ e, e ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and e is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.


title: Program Analysis for Web Security


title: Using Bounded Model Checking to Focus Fixpoint Iterations

authors:
David Monniaux
Laure Gonnord

abstract:
Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths.

In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.


title: Program Analysis and Machine Learning: A Win-Win Deal

authors:
Aditya V. Nori
Sriram K. Rajamani


title: Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

authors:
Peter Schrammel
Bertrand Jeannet


title: Satisfiability Modulo Recursive Programs

authors:
Philippe Suter
Ali Sinan Köksal
Viktor Kuncak


title: Verifying Fence Elimination Optimisations

authors:
Viktor Vafeiadis
Francesco Zappa Nardelli


title: Transitive Closures of Affine Integer Tuple Relations and Their Overapproximations

authors:
Sven Verdoolaege
Albert Cohen
Anna Beletska


title: Bound Analysis of Imperative Programs with the Size-Change Abstraction

authors:
Florian Zuleger
Sumit Gulwani
Moritz Sinn
Helmut Veith


title: Automatic Fence Insertion in Integer Programs via Predicate Abstraction

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Carl Leonardsson
Ahmed Rezine


title: Craig Interpretation

authors:
Aws Albarghouthi
Arie Gurfinkel
Marsha Chechik


title: On the Limits of the Classical Approach to Cost Analysis

authors:
Diego Esteban Alonso-Blas
Samir Genaim


title: Computer-Aided Cryptographic Proofs

authors:
Gilles Barthe
Benjamin Grégoire
Santiago Zanella-Béguelin


title: Loop Leaping with Closures

authors:
Sebastian Biallas
Jörg Brauer
Andy King
Stefan Kowalewski


title: Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases

authors:
David Cachera
Thomas P. Jensen
Arnaud Jobin
Florent Kirchner


title: Control Flow Analysis for the Join Calculus

authors:
Peter Calvert
Alan Mycroft


title: Termination Proofs for Linear Simple Loops

authors:
Hong Yi Chen
Shaked Flur
Supratik Mukhopadhyay


title: An Abstract Domain to Infer Types over Zones in Spreadsheets

authors:
Tie Cheng
Xavier Rival


title: Satisfiability Solvers Are Static Analysers

authors:
Vijay Victor D'Silva
Leopold Haller
Daniel Kroening


title: A Voyage to the Deep-Heap


title: Finding Non-terminating Executions in Distributed Asynchronous Programs

authors:
Michael Emmi
Akash Lal


title: Making Abstract Interpretation Incomplete: Modeling the Potency of Obfuscation

authors:
Roberto Giacobazzi
Isabella Mastroeni


title: Symbolic Learning of Component Interfaces

authors:
Dimitra Giannakopoulou
Zvonimir Rakamaric
Vishwanath Raman


title: Modular Static Analysis with Zonotopes

authors:
Eric Goubault
Sylvie Putot
Franck Védrine


title: When the Decreasing Sequence Fails

authors:
Nicolas Halbwachs
Julien Henry


title: Succinct Representations for Abstract Interpretation - Combined Analysis Algorithms and Experimental Evaluation

authors:
Julien Henry
David Monniaux
Matthieu Moy

abstract:
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and sparse representations of paths and sets of paths avoid this pitfall.

We improve previously proposed techniques for guided static analysis and the generation of disjunctive invariants by combining them with techniques for succinct representations of paths and symbolic representations for transitions based on static single assignment.

Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages.


title: Polyhedral Analysis Using Parametric Objectives

authors:
Jacob M. Howe
Andy King


title: A New Abstract Domain for the Representation of Mathematically Equivalent Expressions

authors:
Arnault Ioualalen
Matthieu Martel


title: Path-Sensitive Backward Slicing

authors:
Joxan Jaffar
Vijayaraghavan Murali
Jorge A. Navas
Andrew E. Santosa


title: Liveness-Based Pointer Analysis

authors:
Uday P. Khedker
Alan Mycroft
Prashant Singh Rawat


title: Semantics and Analyses for JavaScript and the Web


title: Binary Reachability Analysis of Higher Order Functional Programs

authors:
Ruslán Ledesma-Garza
Andrey Rybalchenko


title: Efficient May Happen in Parallel Analysis for Async-Finish Parallelism

authors:
Jonathan K. Lee
Jens Palsberg
Rupak Majumdar
Hong Hong


title: Modular Heap Analysis for Higher-Order Programs

authors:
Ravichandhran Madhavan
G. Ramalingam
Kapil Vaswani


title: A Structural Soundness Proof for Shivers's Escape Technique - A Case for Galois Connections

authors:
Jan Midtgaard
Michael D. Adams
Matthew Might


title: Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version)

authors:
Alejandro Sánchez
Sriram Sankaranarayanan
César Sánchez
Bor-Yuh Evan Chang


title: Bilateral Algorithms for Symbolic Abstraction

authors:
Aditya V. Thakur
Matt Elder
Thomas W. Reps


title: A Generalization of Stålmarck's Method

authors:
Aditya V. Thakur
Thomas W. Reps


title: Verification as Learning Geometric Concepts

authors:
Rahul Sharma
Saurabh Gupta
Bharath Hariharan
Alex Aiken
Aditya V. Nori


title: Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists

authors:
Pranav Garg
P. Madhusudan
Gennaro Parlato

abstract: We propose a new approach to heap analysis through an abstract domain of automata, called automatic shapes. Automatic shapes are modeled after a particular version of quantified data automata on skinny trees (QSDAs), that allows to define universally quantified properties of programs manipulating acyclic heaps with a single pointer field, including data-structures such singly-linked lists. To ensure convergence of the abstract fixed-point computation, we introduce a subclass of QSDAs called elastic QSDAs, which forms an abstract domain. We evaluate our approach on several list manipulating programs and we show that the proposed domain is powerful enough to prove a large class of these programs correct.


title: Localizing Widening and Narrowing

authors:
Gianluca Amato
Francesca Scozzari


title: On Solving Universally Quantified Horn Clauses

authors:
Nikolaj S. Bjørner
Kenneth L. McMillan
Andrey Rybalchenko


title: Formal Verification of a C Value Analysis Based on Abstract Interpretation

authors:
Sandrine Blazy
Vincent Laporte
André Maroneze
David Pichardie

abstract: Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone.


title: Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL

authors:
Martin Brain
Vijay Victor D'Silva
Alberto Griggio
Leopold Haller
Daniel Kroening


title: Automatic Verification of Erlang-Style Concurrency

authors:
Emanuele D'Osualdo
Jonathan Kochems
C.-H. Luke Ong

abstract: This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce λ Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of λ Actor programs called Actor Communicating System (ACS) which has a natural interpretation as a vector addition system, for which some verification problems are decidable. We give a parametric abstract interpretation framework for λ Actor and use it to build a polytime computable, flow-based, abstract semantics of λ Actor programs, which we then use to bootstrap the ACS construction, thus deriving a more accurate abstract model of the input program.


title: Predicate Abstraction for Relaxed Memory Models

authors:
Andrei Marian Dan
Yuri Meshman
Martin T. Vechev
Eran Yahav


title: Local Shape Analysis for Overlaid Data Structures

authors:
Cezara Dragoi
Constantin Enea
Mihaela Sighireanu


title: Byte-Precise Verification of Low-Level List Manipulation

authors:
Kamil Dudka
Petr Peringer
Tomás Vojnar


title: Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra

authors:
Alexis Fouilhé
David Monniaux
Michaël Périn

abstract: Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations.


title: Abstract Interpretation over Non-lattice Abstract Domains

authors:
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey


title: Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT


title: Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing

authors:
Hyunha Kim
Kyung-Goo Doh
David A. Schmidt


title: Precise Slicing in Imperative Programs via Term-Rewriting and Abstract Interpretation


title: Contextual Locking for Dynamic Pushdown Networks

authors:
Peter Lammich
Markus Müller-Olm
Helmut Seidl
Alexander Wenner


title: Static Provenance Verification for Message Passing Programs

authors:
Rupak Majumdar
Roland Meyer
Zilong Wang


title: Witnessing Program Transformations

authors:
Kedar S. Namjoshi
Lenore D. Zuck


title: Abstract Semantic Differencing for Numerical Programs

authors:
Nimrod Partush
Eran Yahav


title: Symbolic Automata for Static Specification Mining

authors:
Hila Peleg
Sharon Shoham
Eran Yahav
Hongseok Yang


title: Automatic Synthesis of Deterministic Concurrency

authors:
Veselin Raychev
Martin T. Vechev
Eran Yahav


title: From Concrete Examples to Heap Manipulating Programs


title: Static Analysis in the Continuously Changing World


title: The Abstract Domain of Segmented Ranking Functions


title: Concise Analysis Using Implication Algebras for Task-Local Memory Optimisation

authors:
Leo White
Alan Mycroft


title: Block Me If You Can! - Context-Sensitive Parameterized Verification

authors:
Parosh Aziz Abdulla
Frédéric Haziza
Lukás Holík


title: Peak Cost Analysis of Distributed Systems

authors:
Elvira Albert
Jesús Correas Fernández
Guillermo Román-Díez


title: Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction

authors:
Alexey Bakhirkin
Josh Berdine
Nir Piterman

abstract: We propose a novel approach for computing weakest liberal safe preconditions of programs. The standard approaches, which call for either underapproximation of a greatest fixed point, or complementation of a least fixed point, are often difficult to apply successfully. Our approach relies on a different decomposition of the weakest precondition of loops. We exchange the greatest fixed point for the computation of a least fixed point above a recurrent set, instead of the bottom element. Convergence is achieved using over-approximation, while in order to maintain soundness we use an under-approximating logical subtraction operation. Unlike general complementation, subtraction more easily allows for increased precision in case its arguments are related. The approach is not restricted to a specific abstract domain and we use it to analyze programs using the abstract domains of intervals and of 3-valued structures


title: SawjaCard: A Static Analysis Tool for Certifying Java Card Applications

authors:
Frédéric Besson
Thomas P. Jensen
Pierre Vittet


title: Cyclic Abduction of Inductively Defined Safety and Termination Preconditions

authors:
James Brotherston
Nikos Gorogiannis


title: Expectation Invariants for Probabilistic Program Loops as Fixed Points

authors:
Aleksandar Chakarov
Sriram Sankaranarayanan


title: Verifying Recursive Programs Using Intraprocedural Analyzers

authors:
Yu-Fang Chen
Chiao Hsieh
Ming-Hsien Tsai
Bow-Yaw Wang
Farn Wang


title: An Abstract Domain to Infer Octagonal Constraints with Absolute Value

authors:
Liqian Chen
Jiangchao Liu
Antoine Miné
Deepak Kapur
Ji Wang


title: Automatic Analysis of Open Objects in Dynamic Language Programs

authors:
Arlen Cox
Bor-Yuh Evan Chang
Xavier Rival


title: Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations

authors:
Khalil Ghorbal
Andrew Sogokon
André Platzer


title: On Program Equivalence with Reductions

authors:
Guillaume Iooss
Christophe Alias
Sanjay V. Rajopadhye


title: A Progress Bar for Static Analyzers

authors:
Woosuk Lee
Hakjoo Oh
Kwangkeun Yi


title: Sparse Dataflow Analysis with Pointers and Reachability

authors:
Magnus Madsen
Anders Møller


title: Reactivity of Cooperative Systems - Application to ReactiveML

authors:
Louis Mandel
Cédric Pasteur


title: Synthesis of Memory Fences via Refinement Propagation

authors:
Yuri Meshman
Andrei Marian Dan
Martin T. Vechev
Eran Yahav


title: Speeding Up Logico-Numerical Strategy Iteration

authors:
David Monniaux
Peter Schrammel


title: Cost-Aware Automatic Program Repair

authors:
Roopsha Samanta
Oswaldo Olivo
E. Allen Emerson

abstract: We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.


title: An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

authors:
Antoine Toubhans
Bor-Yuh Evan Chang
Xavier Rival


title: A Decision Tree Abstract Domain for Proving Conditional Termination

authors:
Caterina Urban
Antoine Miné


title: Region-Based Selective Flow-Sensitive Pointer Analysis

authors:
Sen Ye
Yulei Sui
Jingling Xue


title: Property-based Polynomial Invariant Generation Using Sums-of-Squares Optimization

authors:
Assalé Adjé
Pierre-Loïc Garoche
Victor Magron

abstract: While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains.


title: Parallel Cost Analysis of Distributed Systems

authors:
Elvira Albert
Jesús Correas
Einar Broch Johnsen
Guillermo Román-Díez


title: May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization

authors:
Elvira Albert
Samir Genaim
Pablo Gordillo


title: Static Analysis of Non-interference in Expressive Low-Level Languages

authors:
Peter Aldous
Matthew Might


title: A Forward Analysis for Recurrent Sets

authors:
Alexey Bakhirkin
Josh Berdine
Nir Piterman

abstract: Non-termination of structured imperative programs is primarily due to infinite loops. An important class of non-terminating loop behaviors can be characterized using the notion of recurrent sets. A recurrent set is a set of states from which execution of the loop cannot or might not escape. Existing analyses that infer recurrent sets to our knowledge rely on one of: the combination of forward and backward analyses, quantifier elimination, or SMT-solvers. We propose a purely forward abstract interpretation–based analysis that can be used together with a possibly complicated abstract domain where none of the above is readily available. The analysis searches for a recurrent set of every individual loop in a program by building a graph of abstract states and analyzing it in a novel way. The graph is searched for a witness of a recurrent set that takes the form of what we call a recurrent component which is somewhat similar to the notion of an end component in a Markov decision process.


title: Safety Verification and Refutation by k-Invariants and k-Induction

authors:
Martin Brain
Saurabh Joshi
Daniel Kroening
Peter Schrammel

abstract: Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have to learn and use one technique to find potential problems but then need an entirely different one to show that they have been fixed. This paper presents a single, unified algorithm kIkI, which strictly generalises abstract interpretation, bounded model checking and k-induction. This not only combines the strengths of these techniques but allows them to interact and reinforce each other, giving a `single-tool' approach to verification.


title: Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis

authors:
Ghila Castelnuovo
Mayur Naik
Noam Rinetzky
Mooly Sagiv
Hongseok Yang


title: Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration

authors:
Dario Cattaruzza
Alessandro Abate
Peter Schrammel
Daniel Kroening

abstract: Linear Time Invariant (LTI) systems are ubiquitous in software systems and control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variables is needed. To tackle this general problem, we use abstract acceleration, a method for unbounded-time polyhedral reachability analysis for linear systems. Existing variants of the method are restricted to closed systems, i.e., dynamical models without inputs or non-determinism. In this paper, we present an extension of abstract acceleration to linear loops with inputs, which correspond to discrete-time LTI control systems, and further study the interaction with guard conditions. The new method relies on a relaxation of the solution of the linear dynamical equation that leads to a precise over-approximation of the set of reachable states, which are evaluated using support functions. In order to increase scalability, we use floating-point computations and ensure soundness by interval arithmetic. Our experiments show that performance increases by several orders of magnitude over alternative approaches in the literature. In turn, this tremendous speedup allows us to improve on precision by computing more expensive abstractions. We outperform state-of-the-art tools for unbounded-time analysis of LTI system with inputs in speed as well as in precision.


title: A Binary Decision Tree Abstract Domain Functor

authors:
Junjie Chen
Patrick Cousot


title: SJS: A Type System for JavaScript with Fixed Object Layout

authors:
Wontae Choi
Satish Chandra
George C. Necula
Koushik Sen


title: Synthesizing Heap Manipulations via Integer Linear Programming

authors:
Anshul Garg
Subhajit Roy


title: Refinement Type Inference via Horn Constraint Optimization

authors:
Kodai Hashimoto
Hiroshi Unno

abstract: We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.e., Pareto optimal) refinement types with respect to a user-specified preference order. The flexible optimization of refinement types enabled by the proposed method paves the way for interesting applications, such as inferring most-general characterization of inputs for which a given program satisfies (or violates) a given safety (or termination) property. Our method reduces such a type optimization problem to a Horn constraint optimization problem by using a new refinement type system that can flexibly reason about non-determinism in programs. Our method then solves the constraint optimization problem by repeatedly improving a current solution until convergence via template-based invariant generation. We have implemented a prototype inference system based on our method, and obtained promising results in preliminary experiments.


title: Static Analysis with Set-Closure in Secrecy

authors:
Woosuk Lee
Hyunsook Hong
Kwangkeun Yi
Jung Hee Cheon


title: Shape Analysis for Unstructured Sharing

authors:
Huisong Li
Xavier Rival
Bor-Yuh Evan Chang