venue: aplas

title: Principles of Inverse Computation in a Functional Language

authors:
Sergei M. Abramov
Robert Glück


title: Kima - An Automated Error Correction System for Concurrent Logic Programs

authors:
Yasuhiro Ajiro
Kazunori Ueda


title: Deriving Pre-Conditions for Array Bound Check Elimination

authors:
Wei-Ngan Chin
Siau-Cheng Khoo
Dana N. Xu


title: Generic Validation of Structural Content with Parametric Modules


title: Automatic Generation of Very Efficient Programs by Generalized Partial Computation

authors:
Yoshihiko Futamura
Zenjiro Konishi
Robert Glück


title: Conditional Analysis and Verification

authors:
Nevin Heintze
Joxan Jaffar
Razvan Voicu


title: An Open Environment for Cooperative Equational Solving

authors:
Tetsuo Ida
Mircea Marin


title: Partial CPS Transformation Using Static Annotation

authors:
Jungtaek Kim
Kwangkeun Yi


title: A Generalization of Hybrid Let-Polymorphic Type Inference Algorithms

authors:
Oukseh Lee
Kwangkeun Yi


title: A New Criterion for Safe Program Transformations


title: On Building Trees with Minimum Height, Relationally


title: A Note on Algebraic Structure of Tree Decomposition of Graphs


title: Logical Analysis of Assembly Language


title: Light Logic and Resource Bounded Computation


title: Proving Syntactic Properties of Exceptions in an Ordered Logical Framework

authors:
Jeff Polakow
Kwangkeun Yi


title: A Declarative Approach to Concurrency in Java

authors:
Rafael Ramírez
Andrew E. Santosa


title: A Note on Model Checkers Reuse and Validation

authors:
Nikolay V. Shilov
Kwangkeun Yi


title: Abstraction of Link Structures by Regular Expressions and Abstract Model Checking of Concurrent Garbage Collection

authors:
Koichi Takahashi
Masami Hagiya


title: Berlioz: Compiling Oz to Java Bytecode


title: Linearity Analysis of Concurrent Logic Programs


title: An Efficient Algorithm for Scheduling Instructions with Deadline Constraints on ILP Machines

authors:
Hui Wu
Joxan Jaffar


title: Mining Optimized Ranges

authors:
Haiyan Zhao
Zhenjiang Hu
Masato Takeichi


title: A Differential Evaluation of Fixpoint Iterations


title: Efficient Interpretation of Chart Pattern Language

authors:
Saswat Anand
Siau-Cheng Khoo


title: Exploring Dataflow in Legacy Systems

authors:
Mikhail A. Bulyonkov
N. N. Filatkina


title: Computability and Complexity Results for a Spatial Assertion Language for Data Structures

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


title: Estimating Exception-Induced Control Flow for Java

authors:
Byeong-Mo Chang
Jang-Wu Jo


title: Higher-Order Polymorphic Sized Types for Safety Checks


title: A Type System for the Push-Enter Model

authors:
Kwanghoon Choi
Taisook Han


title: On Modular Transformations of Structural Content

authors:
Tyng-Ruey Chuang
Jan-Li Lin


title: Analysis of Secure Information Flow by Model-Checking

authors:
Kyung-Goo Doh
Seung Cheol Shin


title: Simple Type Inference for Structural Polymorphism


title: Jones Optimality and the Strength of Program Specializers


title: Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus


title: An Accumulative Parallel Skeleton for All

authors:
Zhenjiang Hu
Hideya Iwasaki
Masato Takeichi


title: Resource Usage Analysis

authors:
Atsushi Igarashi
Naoki Kobayashi


title: Dynamic Control Operators in Type Theory


title: Optimizing Compilation of Concurrent Logic Programs Directed by Interface Analysis

authors:
Norio Kato
Kazunori Ueda


title: Collaborative Constraint Functional Logic Programming in an Open Environment

authors:
Norio Kobayashi
Mircea Marin
Tetsuo Ida


title: An Effect System Combining Alias and Liveness for Explicit Memory Reuse


title: Verifying the CPS Transformation in Isabelle/HOL

authors:
Yasuhiko Minamide
Koji Okuma


title: Functional Quantum Programming

authors:
Shin-Cheng Mu
Richard S. Bird


title: Static Monotonicity Analysis for lambda-Definable Functions. over Lattices

authors:
Andrzej S. Murawski
Kwangkeun Yi


title: Abstract Interpretation over Infinite Abstract Domains (Tentative Report)


title: Proof-Directed Compilation for Inter-operable Languages


title: VM lambda: a Functional Calculus for Scientific Discovery

authors:
Eijiro Sumii
Hideo Bannai


title: Resource-Passing Concurrent Programming


title: Efficient Model-Checking of Timed Automata with Clock-Restriction Diagram


title: Developing the Generic Path Algorithmic Program and its Instantiations Using PAR Method


title: Abstract A* Algorithm and Its Application to Linearly Priced Timed Automata

authors:
Mitsuharu Yamamoto
Masami Hagiya


title: A Compositional Framework for Querying Optimized Ranges

authors:
Haiyan Zhao
Zhenjiang Hu
Masato Takeichi


title: Extending Sized Type with Collection Analysis

authors:
Wei-Ngan Chin
Siau-Cheng Khoo
Dana N. Xu


title: Data Flow Analysis of Secure Information-Flow

authors:
Kyung-Goo Doh
Seung Cheol Shin
Kwangkeun Yi


title: An Improved Differential Fixpoint Iteration Method for Program Analysis

authors:
Hyunjun Eo
Kwangkeun Yi


title: On Quasi-Open Bisimulation


title: Relaxing the Value Restriction


title: An Automatic Program Inverter for Lisp: Potential and Limitations

authors:
Robert Glück
Masahiko Kawabe


title: Specification based on Backus-Naur Formalism and Programming Language

authors:
Guoyong
Peimin Deng
Jiali Feng


title: Flattening Transformation for Efficient Segmented Computation - Segmented Diffusion Theorem


title: Recursion Removal from Recursive Programs with One Descent Function

authors:
Yusuke Ichikawa
Zenjiro Konishi
Yoshihiko Futamura


title: Functional Logic Origami Programming


title: Pruning Unnecessary Computations using Improving Sequences


title: Shrinkable Polymorphic Variants


title: Fusion Transformation on Functional Programs of Regular Expression Types

authors:
Kazuhiko Kakehi
Zhenjiang Hu
Masato Takeichi


title: Type-Based Information Analysis for Low-Level Languages

authors:
Naoki Kobayashi
Keita Shirane


title: Inserting Safe Memory Re-use Commands into ML-like Programs

authors:
Oukseh Lee
Hongseok Yang
Kwangkeun Yi


title: What Is the Right Logical Framework for Evolution of Knowledge


title: An Approach for Assessing Software Coupling


title: Folds with Dependent Types


title: Bisimulation for Higher-Order Pi-calculus

authors:
Xinxin Liu
Yongjian Li


title: Implementation of Parallel Tree Skeletons on Distributed Systems

authors:
Kiminori Matsuzaki
Zhenjiang Hu
Masato Takeichi


title: An Optimal Staging Algorithm

authors:
Takuma Murakami
Zhenjiang Hu
Masato Takeichi


title: Deforesting in Accumulating Parameters via Type-Directed Transformations


title: Algebraic construction of graphs with bounded tree width and its applications - Catamorphic Approach to Program Analyses

authors:
Mizuhito Ogawa
Zhenjiang Hu
Isao Sasano
Masato Takeichi


title: An Interoperable Calculus for External Object Access

authors:
Atsushi Ohori
Kiyoshi Yamatodani


title: COPLA* - a Middleware for Distributed Databases

authors:
Javier Esparza Peidro
Antonio Calero Monteagudo
Jordi Bataller
Francesc D. Muñoz-Escoí
Hendrik Decker
José M. Bernabéu-Aubán


title: An Overview of the Chameleon System


title: Association Computation for Information Access

authors:
Akihiko Takano
Shingo Nishioka
Osamu Imaichi
Yoshiki Niwa


title: Programming with Logical Links


title: A Type-Based Approach to Parallelization (preliminary report)

authors:
Dana N. Xu
Siau-Cheng Khoo
Wei-Ngan Chin
Zhenjiang Hu


title: Static Extensionality Checking for Lambda-Definable Functions Over Lattices

authors:
Kwangkeun Yi
Hyunjun Eo


title: Yicho - A System for Programming Program Calculations

authors:
Tetsuo Yokoyama
Zhenjiang Hu
Masato Takeichi


title: A Differential Fixpoint Evaluation Framework for Non-distributive Systems

authors:
Joonseon Ahn
Yong Jin Kwon


title: Affine-Based Size-Change Termination

authors:
Hugh Anderson
Siau-Cheng Khoo


title: The Semantic Layers of Timber

authors:
Magnus Carlsson
Johan Nordlander
Dick Kieburtz


title: Observing Asymmetry and Mismatch

authors:
Xiaoju Dong
Yuxi Fu


title: Extensional Polymorphism by Flow Graph Dispatching


title: Term Graph Rewriting for the pi-Calculus


title: Controlling and Optimizing the Usage of One Resource

authors:
Antoine Galland
Mathieu Baudet


title: A Program Inverter for a Functional Language with Equality and Constructors

authors:
Robert Glück
Masahiko Kawabe


title: Model Checking: From Hardware to Software


title: Continutation Semantics for Parallel Haskell Dialects

authors:
Mercedes Hidalgo-Herrero
Yolanda Ortega-Mallén


title: Constraint Functional Logic Programming for Origami Construction

authors:
Tetsuo Ida
Mircea Marin
Hidekazu Takahashi


title: Scrap Your Boilerplate

authors:
Simon L. Peyton Jones
Ralf Lämmel


title: Register Allocation Based on a Reference Flow Analysis

authors:
Dae-Hwan Kim
Hyuk-Jae Lee


title: Useless Code Elimination and Programm Slicing for the Pi-Calculus


title: Translating a Continuous-Time Temporal Logic into Timed Automata

authors:
Guangyuan Li
Zhisong Tang


title: Expressive Synchronization Types for Inheritance in the Join Calculus

authors:
Qin Ma
Luc Maranget


title: Resource Usage Verification

authors:
Kim Marriott
Peter J. Stuckey
Martin Sulzmann


title: Dataflow Pointcut in Aspect-Oriented Programming

authors:
Hidehiko Masuhara
Kazunori Kawauchi


title: Rebuilding a Tree from Its Traversals: A Case Study of Program Inversion

authors:
Shin-Cheng Mu
Richard S. Bird


title: Correctness of a Higher-Order Removal Transformation through a Relational Reasoning


title: Executing Verified Compiler Specification

authors:
Koji Okuma
Yasuhiko Minamide


title: Automatic Construction of Hoare Proofs from Abstract Interpretation Results

authors:
Sunae Seo
Hongseok Yang
Kwangkeun Yi


title: Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Constraint Solver


title: Lazy Stack Copying and Stack Copy Sharing for the Efficient Implementation of Continuations

authors:
Tomoharu Ugawa
Nobuhisa Minagawa
Tsuneyasu Komiya
Masahiro Yasugi
Taiichi Yuasa


title: Using Locality of Flow in Dataflow Analyses


title: On a Method of Global Optimization


title: A Typeful and Tagless Representation for XML Documents

authors:
Dengping Zhu
Hongwei Xi


title: A Concurrent System of Multi-ported Processes with Causal Dependency


title: Automatic Generation of Editors for Higher-Order Data Structures

authors:
Peter Achten
Marko C. J. D. van Eekelen
Rinus Plasmeijer
Arjen van Weelden


title: D-Fusion: A Distinctive Fusion Calculus

authors:
Michele Boreale
Maria Grazia Buscemi
Ugo Montanari


title: A Uniform Reduction Equivalence for Process Calculi


title: A Type Theory for Krivine-Style Evaluation and Compilation

authors:
Kwanghoon Choi
Atsushi Ohori


title: Pointcuts as Functional Queries

authors:
Michael Eichberg
Mira Mezini
Klaus Ostermann


title: Network Fusion

authors:
Pascal Fradet
Stéphane Hong Tuan Ha


title: Build, Augment and Destroy, Universally

authors:
Neil Ghani
Tarmo Uustalu
Varmo Vene


title: Free S-Monoids: A Higher-Order Syntax with Metavariables


title: A Relational Model for Object-Oriented Designs

authors:
Jifeng He
Zhiming Liu
Xiaoshan Li
Shengchao Qin

abstract: This paper develops a mathematical characterisation of object-oriented concepts by defining an observation-oriented semantics for an object-oriented language (OOL) with a rich variety of features including subtypes, visibility, inheritance, dynamic binding and polymorphism. The language is expressive enough for the specification of object-oriented designs and programs. We also propose a calculus based on this model to support both structural and behavioural refinement of object-oriented designs. We take the approach of the development of the design calculus based on the standard predicate logic in Hoare and He’s Unifying Theories of Programming (UTP). We also consider object reference in terms of object identity as values and mutually dependent methods.


title: Formal Design and Verification of Real-Time Embedded Software

authors:
Pao-Ann Hsiung
Shang-Wei Lin


title: A CLP Approach to Modelling Systems


title: McJava - A Design and Implementation of Java with Mixin-Types

authors:
Tetsuo Kamina
Tetsuo Tamai


title: A MATLAB-Based Code Generator for Sparse Matrix Computations

authors:
Hideyuki Kawabata
Mutsumi Suzuki
Toshiaki Kitamura


title: Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type

authors:
Koichi Kodama
Kohei Suenaga
Naoki Kobayashi


title: Detecting Software Defects in Telecom Applications Through Lightweight Static Analysis: A War Story

authors:
Tobias Lindahl
Konstantinos Sagonas


title: An Implementation of Subtyping Among Regular Expression Types

authors:
Kenny Zhuo Ming Lu
Martin Sulzmann


title: Controlled Declassification Based on Intransitive Noninterference

authors:
Heiko Mantel
David Sands


title: An Algebraic Approach to Bi-directional Updating

authors:
Shin-Cheng Mu
Zhenjiang Hu
Masato Takeichi


title: Region-Based Memory Management for a Dynamically-Typed Language

authors:
Akihito Nagata
Naoki Kobayashi
Akinori Yonezawa


title: An Implementation Scheme for XML Transformation Languages Through Derivation of Stream Processors


title: A Functional Language for Logarithmic Space


title: Protocol Specialization

authors:
Matthias Neubauer
Peter Thiemann


title: The Scala Experiment - Can We Provide Better Language Support for Component Systems?


title: Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk)


title: History Effects and Verification

authors:
Christian Skalka
Scott F. Smith


title: Concurrency Combinators for Declarative Synchronization


title: PType System: A Featherweight Parallelizability Detector

authors:
Dana N. Xu
Siau-Cheng Khoo
Zhenjiang Hu


title: Exploiting Java Objects Behavior for Memory Management and Optimizations

authors:
Zoe C. H. Yu
Francis C. M. Lau
Cho-Li Wang


title: Calculating Polynomial Runtime Properties

authors:
Hugh Anderson
Siau-Cheng Khoo
Stefan Andrei
Beatrice Luca


title: A Typed, Compositional Logic for a Stack-Based Abstract Machine


title: Symbolic Execution with Separation Logic

authors:
Josh Berdine
Cristiano Calcagno
Peter W. O'Hearn


title: A Portable and Customizable Profiling Framework for Java Based on Bytecode Instruction Counting


title: Race Conditions in Message Sequence Charts

authors:
Chien-An Chen
Sara Kalvala
Jane E. Sinclair


title: Integrating Physical Systems in the Static Analysis of Embedded Control Software


title: Resource Bound Certification for a Tail-Recursive Virtual Machine

authors:
Silvano Dal-Zilio
Régis Gascon


title: A Parametric Model for the Analysis of Mobile Ambients


title: A New Occurrence Counting Analysis for BioAmbients

authors:
Roberta Gori
Francesca Levi


title: A Simple Semantics for Polymorphic Recursion


title: Type Systems for XML


title: Lightweight Family Polymorphism

authors:
Atsushi Igarashi
Chieri Saito
Mirko Viroli


title: Heterogeneous Fixed Points with Application to Points-To Analysis

authors:
Aditya Kanade
Uday P. Khedker
Amitabha Sanyal


title: A Path Sensitive Type System for Resource Usage Verification of C Like Languages

authors:
Hyun-Goo Kang
Youil Kim
Taisook Han
Hwansoo Han


title: Loop Invariants on Demand

authors:
K. Rustan M. Leino
Francesco Logozzo


title: Reflection Analysis for Java

authors:
V. Benjamin Livshits
John Whaley
Monica S. Lam


title: On the Rôle of Abstract Non-interference in Language-Based Security


title: Data Refinement with Low-Level Pointer Operations

authors:
Ivana Mijajlovic
Hongseok Yang


title: The Parallel Implementation of the Astrée Static Analyzer

abstract: The Astree static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Keeping analysis times reasonable for industrial use is one of the design objectives. In this paper, we discuss the parallel implementation of the analysis.


title: Register Allocation Via Coloring of Chordal Graphs

authors:
Fernando Magno Quintão Pereira
Jens Palsberg


title: An Abstract Interpretation Perspective on Linear vs. Branching Time

authors:
Francesco Ranzato
Francesco Tapparo


title: A Next-Generation Platform for Analyzing Executables

authors:
Thomas W. Reps
Gogul Balakrishnan
Junghee Lim
Tim Teitelbaum


title: Abstract Dependences for Alarm Diagnosis


title: Termination Analysis of Higher-Order Functional Programs

authors:
Damien Sereni
Neil D. Jones


title: The Essence of Dataflow Programming

authors:
Tarmo Uustalu
Varmo Vene


title: Transformation to Dynamic Single Assignment Using a Simple Data Flow Analysis

authors:
Peter Vanbroekhoven
Gerda Janssens
Maurice Bruynooghe
Francky Catthoor


title: Using Datalog with Binary Decision Diagrams for Program Analysis

authors:
John Whaley
Dzintars Avots
Michael Carbin
Monica S. Lam


title: Computational Secrecy by Typing for the Pi Calculus

authors:
Martín Abadi
Ricardo Corin
Cédric Fournet


title: Reading, Writing and Relations

authors:
Nick Benton
Andrew Kennedy
Martin Hofmann
Lennart Beringer


title: A Bytecode Logic for JML and Types

authors:
Lennart Beringer
Martin Hofmann


title: Relational Reasoning for Recursive Types and References

authors:
Nina Bohr
Lars Birkedal


title: A Localized Tracing Scheme Applied to Garbage Collection

authors:
Yannis Chicha
Stephen M. Watt


title: A Practical String Analyzer by the Widening Approach

authors:
Tae-Hyoung Choi
Oukseh Lee
Hyunha Kim
Kyung-Goo Doh


title: Type and Effect System for Multi-staged Exceptions

authors:
Hyunjun Eo
Ik-Soon Kim
Kwangkeun Yi


title: Scheme with Classes, Mixins, and Traits

authors:
Matthew Flatt
Robert Bruce Findler
Matthias Felleisen


title: On Jones-Optimal Specializers: A Case Study Using Unmix

authors:
Johan Gade
Robert Glück


title: Private Row Types: Abstracting the Unnamed


title: Polymorphism, Subtyping, Whole Program Analysis and Accurate Data Types in Usage Analysis

authors:
Tobias Gedell
Jörgen Gustavsson
Josef Svenningsson


title: An Analysis for Proving Temporal Properties of Biological Systems

authors:
Roberta Gori
Francesca Levi


title: Proof Abstraction for Imperative Languages


title: Automatic Testing of Higher Order Functions

authors:
Pieter W. M. Koopman
Rinus Plasmeijer


title: Using Metadata Transformations to Integrate Class Extensions in an Existing Class Hierarchy


title: A Fine-Grained Join Point Model for More Reusable Aspects

authors:
Hidehiko Masuhara
Yusuke Endoh
Akinori Yonezawa


title: XML Validation for Context-Free Grammars

authors:
Yasuhiko Minamide
Akihiko Tozawa


title: A Pushdown Machine for Recursive XML Processing

authors:
Keisuke Nakano
Shin-Cheng Mu


title: Event Driven Software Quality


title: A Modal Language for the Safety of Mobile Values


title: Comparing Completeness Properties of Static Analyses and Their Logics


title: Widening Polyhedra with Landmarks

authors:
Axel Simon
Andy King


title: Type Processing by Constraint Reasoning

authors:
Peter J. Stuckey
Martin Sulzmann
Jeremy Wazny


title: Principal Type Inference for GHC-Style Multi-parameter Type Classes

authors:
Martin Sulzmann
Tom Schrijvers
Peter J. Stuckey


title: Combining Offline and Online Optimizations: Register Allocation and Method Inlining

authors:
Hiroshi Yamauchi
Jan Vitek


title: Mixed Inductive/Coinductive Types and Strong Normalization


title: CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence

authors:
Jesús Aranda
Cinzia Di Giusto
Mogens Nielsen
Frank D. Valencia


title: Polymorphic Delimited Continuations

authors:
Kenichi Asai
Yukiyoshi Kameyama


title: Positive Arithmetic Without Exchange Is a Subclassical Logic

authors:
Stefano Berardi
Makoto Tatsuta


title: Timed, Distributed, Probabilistic, Typed Processes

authors:
Martin Berger
Nobuko Yoshida


title: Persistent Oberon: A Programming Language with Integrated Persistence


title: On a Tighter Integration of Functional and Logic Programming

authors:
Bernd Braßel
Frank Huch


title: Adjunct Elimination in Context Logic for Trees

authors:
Cristiano Calcagno
Thomas Dinsdale-Young
Philippa Gardner


title: Finally Tagless, Partially Evaluated

authors:
Jacques Carette
Oleg Kiselyov
Chung-chieh Shan


title: Monadic, Prompt Lazy Assertions in Haskell

authors:
Olaf Chitil
Frank Huch


title: Scalable Simulation of Cellular Signaling Networks

authors:
Vincent Danos
Jérôme Feret
Walter Fontana
Jean Krivine


title: Translation Correctness for First-Order Object-Oriented Pattern Matching

authors:
Burak Emir
Qin Ma
Martin Odersky


title: Local Reasoning for Storable Locks and Threads

authors:
Alexey Gotsman
Josh Berdine
Byron Cook
Noam Rinetzky
Mooly Sagiv


title: A Probabilistic Applied Pi-Calculus

authors:
Jean Goubault-Larrecq
Catuscia Palamidessi
Angelo Troina


title: Deriving Compilers and Virtual Machines for a Multi-level Language

authors:
Atsushi Igarashi
Masashi Iwaki


title: The Semantics of "Semantic Patches" in Coccinelle: Program Transformation for the Working Programmer

authors:
Neil D. Jones
René Rydhof Hansen


title: Call-by-Name and Call-by-Value in Normal Modal Logic


title: Type-Based Verification of Correspondence Assertions for Communication Protocols

authors:
Daisuke Kikuchi
Naoki Kobayashi


title: Call-by-Value Is Dual to Call-by-Name, Extended


title: An Efficient SSA-Based Algorithm for Complete Global Value Numbering

authors:
Jiu-Tao Nie
Xu Cheng


title: A Systematic Approach to Probabilistic Pointer Analysis

authors:
Alessandra Di Pierro
Chris Hankin
Herbert Wiklicky


title: Complete Lattices and Up-To Techniques


title: Static and Dynamic Analysis: Better Together


title: X10: Concurrent Programming for Modern Architectures


title: The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification

authors:
Paritosh Shroff
Christian Skalka
Scott F. Smith


title: A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract

abstract: A notion of open bisimulation is formulated for the spi calculus, an extension of the π-calculus with cryptographic primitives. In this formulation, open bisimulation is indexed by pairs of symbolic traces, which represent the history of interactions between the environment with the pairs of processes being checked for bisimilarity. The use of symbolic traces allows for a symbolic treatment of bound input in bisimulation checking which avoids quantification over input values. Open bisimilarity is shown to be sound with respect to testing equivalence, and futher, it is shown to be an equivalence relation on processes and a congruence on finite processes.


title: More Typed Assembly Languages for Confidentiality


title: A Novel Test Case Generation Method for Prolog Programs Based on Call Patterns Semantics

authors:
Lingzhong Zhao
Tianlong Gu
Junyan Qian
Guoyong Cai


title: Static Detection of Place Locality and Elimination of Runtime Checks

authors:
Shivali Agarwal
Rajkishore Barik
V. Krishna Nandivada
R. K. Shyamasundar
Pradeep Varma


title: On Affine Usages in Signal-Based Communication

authors:
Roberto M. Amadio
Mehdi Dogguy

abstract: We describe a type system for a synchronous *** -calculus formalising the notion of affine usage in signal-based communication. In particular, we identify a limited number of usages that preserve affinity and that can be composed. As a main application of the resulting system, we show that typable programs are deterministic .


title: Extensional Universal Types for Call-by-Value


title: Certified Reasoning in Memory Hierarchies

authors:
Gilles Barthe
César Kunz
Jorge Luis Sacchini


title: Exception Handlers as Extensible Cases

authors:
Matthias Blume
Umut A. Acar
Wonseok Chae


title: The Complexity of Coverage

authors:
Krishnendu Chatterjee
Luca de Alfaro
Rupak Majumdar


title: Game Characterizations of Process Equivalences

authors:
Xin Chen
Yuxin Deng


title: A Sound Floating-Point Polyhedra Abstract Domain

authors:
Liqian Chen
Antoine Miné
Patrick Cousot


title: Minimal Ownership for Active Objects

authors:
Dave Clarke
Tobias Wrigstad
Johan Östlund
Einar Broch Johnsen

abstract: Active objects offer a structured approach to concurrency, encapsulating both unshared state and a thread of control. For efficient data transfer, data should be passed by reference whenever possible, but this introduces aliasing and undermines the validity of the active objects. This paper proposes a minimal variant of ownership types that preserves the required race freedom invariant yet enables data transfer by reference between active objects (that is, without copying) in many cases, and a cheap clone operation where copying is necessary. Our approach is general and should be adaptable to several existing active object systems.


title: Abstraction of Clocks in Synchronous Data-Flow Systems

authors:
Albert Cohen
Louis Mandel
Florence Plateau
Marc Pouzet


title: The Essence of Form Abstraction

authors:
Ezra Cooper
Sam Lindley
Philip Wadler
Jeremy Yallop


title: Abductive Inference for Reasoning about Heaps


title: Reasoning about Java's Reentrant Locks

authors:
Christian Haack
Marieke Huisman
Clément Hurlin


title: From Authorization Logics to Types for Authorization


title: Harnessing the Multicores: Nested Data Parallelism in Haskell


title: JavaScript Instrumentation in Practice

authors:
Haruka Kikuchi
Dachuan Yu
Ajay Chander
Hiroshi Inamura
Igor Serikov


title: Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution

authors:
Xin Li
Daryl Shannon
Indradeep Ghosh
Mizuhito Ogawa
Sreeranga P. Rajan
Sarfraz Khurshid

abstract: Symbolic execution is a flexible and powerful, but computationally expensive technique to detect dynamic behaviors of a program. In this paper, we present a context-sensitive relevancy analysis algorithm based on weighted pushdown model checking, which pinpoints memory locations in the program where symbolic values can flow into. This information is then utilized by a code instrumenter to transform only relevant parts of the program with symbolic constructs, to help improve the efficiency of symbolic execution of Java programs. Our technique is evaluated on a generalized symbolic execution engine that is developed upon Java Path Finder with checking safety properties of Java applications. Our experiments indicate that this technique can effectively improve the performance of the symbolic execution engine with respect to the approach that blindly instruments the whole program.


title: An Operational Semantics for JavaScript

authors:
Sergio Maffeis
John C. Mitchell
Ankur Taly

abstract: We define a small-step operational semantics for the ECMAScript standard language corresponding to JavaScript, as a basis for analyzing security properties of web applications and mashups. The semantics is based on the language standard and a number of experiments with different implementations and browsers. Some basic properties of the semantics are proved, including a soundness theorem and a characterization of the reachable portion of the heap.


title: Sound and Complete Type Inference for a Systems Programming Language

authors:
Swaroop Sridhar
Jonathan S. Shapiro
Scott F. Smith


title: A Flow-Sensitive Region Inference for CLI

authors:
Alexandru Stefan
Florin Craciun
Wei-Ngan Chin


title: Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References


title: Interface Types for Haskell

authors:
Peter Thiemann
Stefan Wehr


title: ML Modules and Haskell Type Classes: A Constructive Comparison

authors:
Stefan Wehr
Manuel M. T. Chakravarty


title: Asymptotic Resource Usage Bounds

authors:
Elvira Albert
Diego Esteban Alonso-Blas
Puri Arenas
Samir Genaim
German Puebla

abstract: When describing the resource usage of a program, it is usual to talk in asymptotic terms, such as the well-known "big O" notation, whereby we focus on the behaviour of the program for large input data and make a rough approximation by considering as equivalent programs whose resource usage grows at the same rate. Motivated by the existence of non-asymptotic resource usage analyzers, in this paper, we develop a novel transformation from a non-asymptotic cost function (which can be produced by multiple resource analyzers) into its asymptotic form. Our transformation aims at producing tight asymptotic forms which do not contain redundant subexpressions (i.e., expressions asymptotically subsumed by others). Interestingly, we integrate our transformation at the heart of a cost analyzer to generate asymptotic upper bounds without having to first compute their non-asymptotic counterparts. Our experimental results show that, while non-asymptotic cost functions become very complex, their asymptotic forms are much more compact and manageable. This is essential to improve scalability and to enable the application of cost analysis in resource-aware verification/certification.


title: On Stratified Regions


title: Bi-abductive Resource Invariant Synthesis

authors:
Cristiano Calcagno
Dino Distefano
Viktor Vafeiadis


title: The Twilight Zone: From Testing to Formal Specifications and Back Again


title: A Fresh Look at Separation Algebras and Share Accounting

authors:
Robert Dockins
Aquinas Hobor
Andrew W. Appel


title: Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine

authors:
Yuan Dong
Kai Ren
Shengyuan Wang
Suqin Zhang


title: Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable


title: Classical Natural Deduction for S4 Modal Logic

authors:
Daisuke Kimura
Yoshihiko Kakutani


title: Types and Recursion Schemes for Higher-Order Program Verification


title: Refining Abstract Interpretation-Based Static Analyses with Hints

authors:
Vincent Laviron
Francesco Logozzo


title: Witnessing Purity, Constancy and Mutability


title: Ownership Downgrading for Ownership Types

authors:
Yi Lu
John Potter
Jingling Xue


title: A Short Cut to Optimal Sequences


title: Scalable Context-Sensitive Points-to Analysis Using Multi-dimensional Bloom Filters

authors:
Rupesh Nasre
Kaushik Rajan
Ramaswamy Govindarajan
Uday P. Khedker


title: Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation


title: Parallel Reduction in Resource Lambda-Calculus

authors:
Michele Pagani
Paolo Tranquilli


title: A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming

authors:
Shigeyuki Sato
Hideya Iwasaki


title: The Higher-Order, Call-by-Value Applied Pi-Calculus

authors:
Nobuyuki Sato
Eijiro Sumii


title: Abstract Transformers for Thread Correlation Analysis

authors:
Michal Segalov
Tal Lev-Ami
Roman Manevich
Ganesan Ramalingam
Mooly Sagiv


title: The Sketching Approach to Program Synthesis


title: Fractional Ownerships for Safe Memory Deallocation

authors:
Kohei Suenaga
Naoki Kobayashi


title: Weak updates and separation logic

authors:
Gang Tan
Zhong Shao
Xinyu Feng
Hongxu Cai


title: Proving Copyless Message Passing

authors:
Jules Villard
Étienne Lozes
Cristiano Calcagno


title: On the Decidability of Subtyping with Bounded Existential Types

authors:
Stefan Wehr
Peter Thiemann


title: An Interactive Tool for Analyzing Embedded SQL Queries

authors:
Aivar Annamaa
Andrey Breslav
Jevgeni Kabanov
Varmo Vene


title: Towards Deriving Type Systems and Implementations for Coroutines

authors:
Konrad Anton
Peter Thiemann


title: Concurrency Can't Be Observed, Asynchronously

authors:
Paolo Baldan
Filippo Bonchi
Fabio Gadducci
Giacoma Valentina Monreale


title: Typechecking Higher-Order Security Libraries

authors:
Karthikeyan Bhargavan
Cédric Fournet
Nataliya Guts


title: Metric Spaces and Termination Analyses

authors:
Aziem Chawdhary
Hongseok Yang


title: A Provably Correct Stackless Intermediate Representation for Java Bytecode

authors:
Delphine Demange
Thomas P. Jensen
David Pichardie


title: Interprocedural Control Flow Reconstruction

authors:
Andrea Flexeder
Bogdan Mihaila
Michael Petter
Helmut Seidl


title: A Certified Implementation of ML with Structural Polymorphism


title: Data Structure Fusion

authors:
Peter Hawkins
Alex Aiken
Kathleen Fisher
Martin C. Rinard
Mooly Sagiv

abstract: We consider the problem of specifying data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies; a novel fuse operation on relational indexes specifies where the underlying physical data structure representation has sharing. We permit the user to specify different concrete shared representations for relations, and show that the semantics of the relational specification are preserved.


title: Model Independent Order Relations for Processes


title: A Logical Mix of Approximation and Separation

authors:
Aquinas Hobor
Robert Dockins
Andrew W. Appel


title: Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics

authors:
Jan Hoffmann
Martin Hofmann


title: A Quick Tour of the VeriFast Program Verifier

authors:
Bart Jacobs
Jan Smans
Frank Piessens

abstract:
This paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in separation logic, inductive data type and fixpoint definitions, lemma functions and proof steps. The verifier checks that (1) the program does not perform illegal operations such as dividing by zero or illegal memory accesses and (2) that the assumptions described in method contracts hold in each execution.

Although VeriFast supports specifying and verifying deep data structure properties, it provides an interactive verification experience as verification times are consistently low and errors can be diagnosed using its symbolic debugger. VeriFast and a large number of example programs are available online at: http://www.cs.kuleuven.be/~bartj/verifast


title: Context-Preserving XQuery Fusion

authors:
Hiroyuki Kato
Soichiro Hidaka
Zhenjiang Hu
Keisuke Nakano
Yasunori Ishihara


title: Categorical Descriptional Composition


title: Live Heap Space Bounds for Real-Time Systems

authors:
Martin Kero
Pawel Pietrzak
Johan Nordlander


title: From a Verified Kernel towards Verified Systems


title: Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates

authors:
Soonho Kong
Yungbum Jung
Cristina David
Bow-Yaw Wang
Kwangkeun Yi


title: Type Inference for Sublinear Space Functional Programming

authors:
Ugo Dal Lago
Ulrich Schöpp


title: A Calculus for Hybrid CSP

authors:
Jiang Liu
Jidong Lv
Zhao Quan
Naijun Zhan
Hengjun Zhao
Chaochen Zhou
Liang Zou


title: Liberal Typing for Functional Logic Programs

authors:
Francisco Javier López-Fraguas
Enrique Martin-Martin
Juan Rodríguez-Hortalá


title: Reasoning about Computations Using Two-Levels of Logic


title: Simple and Precise Widenings for H-Polyhedra

authors:
Axel Simon
Liqian Chen


title: JNI Light: An Operational Model for the Core JNI


title: Index-Compact Garbage Collection

authors:
Liangliang Tong
Francis C. M. Lau


title: Verification of Tree-Processing Programs via Higher-Order Model Checking

authors:
Hiroshi Unno
Naoshi Tabuchi
Naoki Kobayashi


title: Liveness of Communicating Transactions (Extended Abstract)

authors:
Edsko de Vries
Vasileios Koutavas
Matthew Hennessy

abstract: We study liveness and safety in the context of CCS extended with communicating transactions, a construct we recently proposed to model automatic error recovery in distributed systems. We show that fair-testing and may-testing capture the right notions of liveness and safety in this setting, and argue that must-testing imposes too strong a requirement in the presence of transactions. We develop a sound and complete theory of fair-testing in terms of CCS-like tree failures and show that, compared to CCS, communicating transactions provide increased distinguishing power to the observer. We also show that weak bisimilarity is a sound, though incomplete, proof technique for both may- and fair-testing. To the best of our knowledge this is the first semantic treatment of liveness in the presence of transactions. We exhibit the usefulness of our theory by proving illuminating liveness laws and simple but non-trivial examples.


title: Foundations of Quantum Programming (Extended Abstract)


title: Relational Parametricity for a Polymorphic Linear Lambda Calculus

authors:
Jianzhou Zhao
Qi Zhang
Steve Zdancewic


title: Bisimulation Proof Methods in a Path-Based Specification Language for Polynomial Coalgebras

authors:
Xiaocong Zhou
Yongji Li
Wenjun Li
Hai-Yan Qiao
Zhongmei Shu


title: Cost Analysis of Concurrent OO Programs

authors:
Elvira Albert
Puri Arenas
Samir Genaim
Miguel Gómez-Zamalloa
German Puebla


title: Soundness of Data Flow Analyses for Weak Memory Models

authors:
Jade Alglave
Daniel Kroening
John Lugton
Vincent Nimal
Michael Tautschnig


title: Elementary Linear Logic Revisited for Polynomial Time and an Exponential Time Hierarchy


title: Engineering Theories with Z3


title: A Non-iterative Data-Flow Algorithm for Computing Liveness Sets in Strict SSA Programs

authors:
Benoit Boissinot
Florian Brandner
Alain Darte
Benoît Dupont de Dinechin
Fabrice Rastello


title: Towards a General Theory of Barbs, Contexts and Labels

authors:
Filippo Bonchi
Fabio Gadducci
Giacoma Valentina Monreale


title: Compiler Backend Generation for Application Specific Instruction Set Processors

authors:
Zhen Cao
Yuan Dong
Shengyuan Wang


title: Constructing List Homomorphisms from Proofs

authors:
Yun-Yan Chi
Shin-Cheng Mu


title: Template-Based Unbounded Time Verification of Affine Hybrid Automata

authors:
Thao Dang
Thomas Martin Gawlitza


title: Towards a Certified Petri Net Model-Checker

authors:
Lukasz Fronc
Franck Pommereau


title: Solving Recursion-Free Horn Clauses over LI+UIF

authors:
Ashutosh Gupta
Corneliu Popeea
Andrey Rybalchenko


title: Software Verification with Liquid Types


title: A Semantics for Context-Sensitive Reduction Semantics

authors:
Casey Klein
Jay A. McCarthy
Steven Jaconette
Robert Bruce Findler


title: Polymorphic Multi-stage Language with Control Effects

authors:
Yuichiro Kokaji
Yukiyoshi Kameyama


title: Decentralized Delimited Release

authors:
Jonas Magazinius
Aslan Askarov
Andrei Sabelfeld


title: On the Strength of Owicki-Gries for Resources

authors:
Alexander Malkis
Laurent Mauborgne


title: Static Object Race Detection

authors:
Ana L. Milanova
Wei Huang


title: Modular Abstractions of Reactive Nodes Using Disjunctive Invariants

authors:
David Monniaux
Martin Bodin

abstract:
We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to do so, we compute disjunctive invariants in predicate abstraction, with a bounded number of disjuncts, then we abstract the node, each disjunct representing an abstract state. The computation of the disjunctive invariant is performed by a form of quantifier elimination expressed using SMT-solving.

The same method can also be used to obtain disjunctive loop invariants.


title: Macro Tree Transformations of Linear Size Increase Achieve Cost-Optimal Parallelism


title: A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction

authors:
Keiko Nakata
Tarmo Uustalu
Marc Bezem


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

authors:
Aditya V. Nori
Sriram K. Rajamani


title: Algebra, Logic, Locality, Concurrency


title: Access-Based Localization with Bypassing

authors:
Hakjoo Oh
Kwangkeun Yi


title: A Deductive Database with Datalog and SQL Query Languages

authors:
Fernando Sáenz-Pérez
Rafael Caballero
Yolanda García-Ruiz


title: Computation-by-Interaction with Effects


title: SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA

authors:
Yulei Sui
Sen Ye
Jingling Xue
Pen-Chung Yew


title: Extending Hindley-Milner Type Inference with Coercive Structural Subtyping

authors:
Dmitriy Traytel
Stefan Berghofer
Tobias Nipkow


title: Ownership Types for Object Synchronisation

authors:
Yi Lu
John Potter
Jingling Xue


title: Dynamic Software Update for Message Passing Programs

authors:
Gabrielle Anderson
Julian Rathke


title: Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis

authors:
Kalmer Apinis
Helmut Seidl
Vesal Vojdani


title: A Functional View of Imperative Information Flow

authors:
Thomas H. Austin
Cormac Flanagan
Martín Abadi


title: A New Order-Theoretic Characterisation of the Polytime Computable Functions

authors:
Martin Avanzini
Naohi Eguchi
Georg Moser

abstract: We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order (sPOP⁎ for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with sPOP⁎ that employs recursion up to depth d, the (innermost) runtime complexity is polynomially bounded of degree d. This bound is tight. Thus we obtain a direct correspondence between a syntactic (and easily verifiable) condition of a program and the asymptotic worst-case complexity of the program.


title: End-to-end Multilevel Hybrid Information Flow Control


title: Inference of Necessary Field Conditions with Abstract Interpretation

authors:
Mehdi Bouaziz
Francesco Logozzo
Manuel Fähndrich


title: A Generic Cyclic Theorem Prover

authors:
James Brotherston
Nikos Gorogiannis
Rasmus Lerchedahl Petersen


title: Indexed Realizability for Bounded-Time Programming with References and Type Fixpoints

authors:
Aloïs Brunel
Antoine Madet

abstract: The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language features recursive types and higher-order store. Our realizability is based on biorthogonality, indexing and is quantitative. This last feature enables us not only to derive a semantical proof of termination, but also to give bounds on the number of computational steps of typed programs.


title: Linear Approximation of Continuous Systems with Trapezoid Step Functions

authors:
Giulia Costantini
Pietro Ferrara
Agostino Cortesi


title: A Case for Behavior-Preserving Actions in Separation Logic

authors:
David Costanzo
Zhong Shao


title: Modular Verification of Concurrent Thread Management

authors:
Yu Guo
Xinyu Feng
Zhong Shao
Peizhi Shi


title: Vinter: A Vampire-Based Tool for Interpolation

authors:
Krystof Hoder
Andreas Holzer
Laura Kovács
Andrei Voronkov


title: Succour to the Confused Deputy - Types for Capabilities

authors:
Radha Jagadeesan
Corin Pitcher
James Riely


title: Lazy v. Yield: Incremental, Linear Pretty-Printing

authors:
Oleg Kiselyov
Simon L. Peyton Jones
Amr Sabry


title: Decision Procedures over Sophisticated Fractional Permissions

authors:
Xuan Bach Le
Cristian Gherghina
Aquinas Hobor


title: Mechanized Semantics for Compiler Verification


title: JATO: Native Code Atomicity for Java

authors:
Siliang Li
Yu David Liu
Gang Tan


title: Java Bytecode Instrumentation Made Easy: The DiSL Framework for Dynamic Program Analysis

authors:
Lukás Marek
Yudi Zheng
Danilo Ansaloni
Aibek Sarimbekov
Walter Binder
Petr Tuma
Zhengwei Qi


title: A Dynamic Interpretation of the CPS Hierarchy

authors:
Marek Materzok
Dariusz Biernacki


title: Scalable Formal Machine Models


title: Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code

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


title: Types and Access Controls for Cross-Domain Security in Flash

authors:
Aseem Rastogi
Avik Chaudhuri
Rob Johnson


title: Concurrent Test Generation Using Concolic Multi-trace Analysis

authors:
Niloofar Razavi
Franjo Ivancic
Vineet Kahlon
Aarti Gupta


title: Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks

authors:
Pascal Sotin
Xavier Rival


title: Planet Dynamic or: How I Learned to Stop Worrying and Love Reflection


title: A Synchronous Language with Partial Delay Specification for Real-Time Systems Programming

authors:
Rémy Wyss
Frédéric Boniol
Julien Forget
Claire Pagetti


title: The Proof Assistant as an Integrated Development Environment


title: Environmental Bisimulations for Delimited-Control Operators

authors:
Dariusz Biernacki
Sergueï Lenglet

abstract: We present a theory of environmental bisimilarity for the delimited-control operators shift and reset. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we develop sound and complete environmental bisimilarities, and we discuss up-to techniques.


title: On Bar Recursion and Choice in a Classical Setting

authors:
Valentin Blot
Colin Riba


title: Brzozowski's and Up-To Algorithms for Must Testing

authors:
Filippo Bonchi
Georgiana Caltais
Damien Pous
Alexandra Silva


title: Paragon for Practical Programming with Information-Flow Control

authors:
Niklas Broberg
Bart van Delft
David Sands


title: Internal Deployment of the Parfait Static Code Analysis Tool at Oracle - (Invited Talk)

authors:
Cristina Cifuentes
Nathan Keynes


title: Generalized Quantitative Analysis of Metric Transition Systems

authors:
Uli Fahrenberg
Axel Legay


title: Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes

authors:
Koichi Fujima
Sohei Ito
Naoki Kobayashi


title: Ambivalent Types for Principal Type Inference with GADTs

authors:
Jacques Garrigue
Didier Rémy


title: Robustness Analysis of Finite Precision Implementations

authors:
Eric Goubault
Sylvie Putot

abstract: A desirable property of control systems is robustness to inputs, when small perturbations of the inputs of a system will cause only small perturbations on outputs. This property should be maintained at the implementation level, where close inputs can lead to different execution paths. The problem becomes crucial for finite precision implementations, where any elementary computation is affected by an error. In this context, almost every test is potentially unstable, that is, for a given input, the finite precision and real numbers paths may differ. Still, state-of-the-art error analyses rely on the stable test hypothesis, yielding unsound error bounds when the conditional block is not robust to uncertainties. We propose a new abstract-interpretation based error analysis of finite precision implementations, which is sound in presence of unstable tests, by bounding the discontinuity error for path divergences. This gives a tractable analysis implemented in the FLUCTUAT analyzer.


title: Sorting and Searching by Distribution: From Generic Discrimination to Generic Tries

authors:
Fritz Henglein
Ralf Hinze


title: Fine-Grained Function Visibility for Multiple Dispatch with Multiple Inheritance

authors:
Jieung Kim
Sukyoung Ryu
Victor Luchangco
Guy L. Steele Jr.


title: A Hoare Logic for SIMT Programs

authors:
Kensuke Kojima
Atsushi Igarashi


title: GDSL: A Universal Toolkit for Giving Semantics to Machine Language

authors:
Julian Kranz
Alexander Sepp
Axel Simon


title: Laws of Programming for References

authors:
Giovanny Lucero
David A. Naumann
Augusto Sampaio


title: ThisJava: An Extension of Java with Exact Types

authors:
Hyunik Na
Sukyoung Ryu


title: Secure Compilation of Object-Oriented Components to Protected Module Architectures

authors:
Marco Patrignani
Dave Clarke
Frank Piessens


title: Separation Logic Modulo Theories

authors:
Juan Antonio Navarro Pérez
Andrey Rybalchenko

abstract: Logical reasoning about program behaviours often requires dealing with heap structures as well as scalar data types. Advances in Satisfiability Modulo Theories (SMT) offer efficient procedures for dealing with scalar values, yet they lack expressive support for dealing with heap structures. In this paper, we present an approach that integrates separation logica prominent logic for reasoning about linked data structures on the heapand existing SMT solving technology. Our model-based approach communicates heap aliasing information between theory and separation logic reasoning, providing an efficient decision procedure for discharging verification conditions in program analysis and verification.


title: Semantics of Probabilistic Programs: A Weak Limit Approach

authors:
Alessandra Di Pierro
Herbert Wiklicky


title: Proofs, Upside Down - A Functional Correspondence between Natural Deduction and the Sequent Calculus


title: The Undefined Domain: Precise Relational Information for Entities That Do Not Exist

authors:
Holger Siegel
Bogdan Mihaila
Axel Simon


title: Model Checking Dynamic Pushdown Networks

authors:
Fu Song
Tayssir Touili


title: Bi-Abduction with Pure Properties for Specification Inference

authors:
Minh-Thai Trinh
Quang Loc Le
Cristina David
Wei-Ngan Chin


title: Dynamic Alias Protection with Aliasing Contracts

authors:
Janina Voigt
Alan Mycroft


title: Temporal Specification Mining for Anomaly Analysis

authors:
Farn Wang
Jung-Hsuan Wu
Chung-Hao Huang
Cheng-Chieh Chang
Chung-Cheng Li


title: Automated Inference of Library Specifications for Source-Sink Property Verification

authors:
Haiyan Zhu
Thomas Dillig
Isil Dillig


title: A Formalized Proof of Strong Normalization for Guarded Recursive Types

authors:
Andreas Abel
Andrea Vezzosi


title: Resource Protection Using Atomics - Patterns and Verification

authors:
Afshin Amighi
Stefan Blom
Marieke Huisman


title: Logic Programming and Logarithmic Space

authors:
Clément Aubert
Marc Bagnol
Paolo Pistone
Thomas Seiller

abstract: We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction. Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given via a syntactic restriction, using an encoding of words that derives from proof theory.


title: Hereditary History-Preserving Bisimilarity: Logics and Automata

authors:
Paolo Baldan
Silvia Crafa


title: A Precise and Abstract Memory Model for C Using Symbolic Values

authors:
Frédéric Besson
Sandrine Blazy
Pierre Wilke


title: Simple and Efficient Algorithms for Octagons

authors:
Aziem Chawdhary
Edward Robbins
Andy King


title: Suppl: A Flexible Language for Policies

authors:
Robert Dockins
Andrew Tolmach


title: Compositional Entailment Checking for a Fragment of Separation Logic

authors:
Constantin Enea
Ondrej Lengál
Mihaela Sighireanu
Tomás Vojnar


title: Resource Analysis of Complex Programs with Cost Equations

authors:
Antonio Flores-Montoya
Reiner Hähnle


title: A Translation of Intersection and Union Types for the λμ-Calculus

authors:
Kentaro Kikuchi
Takafumi Sakurai


title: Inferring Grammatical Summaries of String Values

authors:
Se-Won Kim
Wooyoung Chin
Jimin Park
Jeongmin Kim
Sukyoung Ryu


title: Automatic Constrained Rewriting Induction towards Verifying Procedural Programs

authors:
Cynthia Kop
Naoki Nishida


title: NetKAT - A Formal System for the Verification of Networks


title: Optimized Compilation of Multiset Rewriting with Comprehensions

authors:
Edmund Soon Lee Lam
Iliano Cervesato


title: Functional Pearl: Nearest Shelters in Manhattan

authors:
Shin-Cheng Mu
Ting-Wei Chen


title: Types for Flexible Objects

authors:
Zachary Palmer
Pottayil Harisanker Menon
Alexander Rozenshteyn
Scott F. Smith


title: Syntax-Directed Divide-and-Conquer Data-Flow Analysis

authors:
Shigeyuki Sato
Akimasa Morihata


title: Call-by-Value in a Basic Logic for Interaction


title: Necessary and Sufficient Preconditions via Eager Abstraction

authors:
Mohamed Nassim Seghir
Peter Schrammel

abstract: The precondition for safe execution of a procedure is useful for understanding, verifying and debugging programs. We have previously presented a cegar-based approach for inferring necessary and sufficient preconditions based on the iterative abstraction-refinement of the set of safe and unsafe states until they become disjoint. A drawback of that approach is that safe and unsafe traces are explored separately and each time they are built entirely before being checked for consistency. In this paper, we present an eager approach that explores shared prefixes between safe and unsafe traces conjointly. As a result, individual state sets, by construction, fulfil the property of separation between safe and unsafe states without requiring any refinement. Experiments using our implementation of this technique in the precondition generator P-Gen show a significant improvement compared to our previous cegar-based method. In some cases the running time drops from several minutes to several seconds.


title: Address Chain: Profiling Java Objects without Overhead in Java Heaps

authors:
Xiaohua Shi
Junru Xie
Hengyang Yu


title: Model-Checking for Android Malware Detection

authors:
Fu Song
Tayssir Touili


title: Automatic Memory Management Based on Program Transformation Using Ownership

authors:
Tatsuya Sonobe
Kohei Suenaga
Atsushi Igarashi


title: A ZDD-Based Efficient Higher-Order Model Checking Algorithm

authors:
Taku Terao
Naoki Kobayashi


title: The Essence of Ruby

authors:
Katsuhiro Ueno
Yutaka Fukasawa
Akimasa Morihata
Atsushi Ohori


title: A Method for Scalable and Precise Bug Finding Using Program Analysis and Model Checking

authors:
Manuel Valdiviezo
Cristina Cifuentes
Padmanabhan Krishnan


title: A Strong Distillery

authors:
Beniamino Accattoli
Pablo Barenbaum
Damiano Mazza

abstract: Abstract machines for the strong evaluation of \(\lambda \)-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.


title: Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics

authors:
Assalé Adjé
Pierre-Loïc Garoche
Alexis Werey

abstract:
Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $\epsilon \in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $\epsilon_i \epsilon_j$.
In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide set of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms.
In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.


title: Transactions on Mergeable Objects

authors:
Deepthi Devaki Akkoorath
Annette Bieniusa


title: Programming Techniques for Reversible Comparison Sorts

authors:
Holger Bock Axelsen
Tetsuo Yokoyama


title: Randomized Resource-Aware Path-Sensitive Static Analysis


title: Bottom-Up Context-Sensitive Pointer Analysis for Java

authors:
Yu Feng
Xinyu Wang
Isil Dillig
Thomas Dillig


title: Objects in Polynomial Time

authors:
Emmanuel Hainry
Romain Péchoux


title: A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers

authors:
Hiroaki Inoue
Atsushi Igarashi


title: Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques

authors:
Guilhem Jaber
Nicolas Tabareau


title: Decision Algorithms for Checking Definability of Order-2 Finitary PCF

authors:
Sadaaki Kawata
Kazuyuki Asada
Naoki Kobayashi


title: A Secure Compiler for ML Modules

authors:
Adriaan Larmuseau
Marco Patrignani
Dave Clarke


title: Abstraction of Optional Numerical Values

authors:
Jiangchao Liu
Xavier Rival


title: Tree-Like Grammars and Separation Logic

authors:
Christoph Matheja
Christina Jansen
Thomas Noll


title: Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs

authors:
Yuma Matsumoto
Naoki Kobayashi
Hiroshi Unno


title: Fault-Tolerant Resource Reasoning

authors:
Gian Ntzik
Pedro da Rocha Pinto
Philippa Gardner


title: Detection of Redundant Expressions: A Complete and Polynomial-Time Algorithm in SSA


title: From Call-by-Value to Interaction by Typed Closure Conversion


title: Shifting the Blame - A Blame Calculus with Delimited Control

authors:
Taro Sekiyama
Soichiro Ueda
Atsushi Igarashi


title: Aliasing Control in an Imperative Pure Calculus

authors:
Marco Servetto
Elena Zucca


title: More Sound Static Handling of Java Reflection

authors:
Yannis Smaragdakis
George Balatsouras
George Kastrinis
Martin Bravenboer

abstract: Reflection is a highly dynamic language feature that poses grave problems for static analyses. In the Java setting, reflection is ubiquitous in large programs. Any handling of reflection will be approximate, and overestimating its reach in a large codebase can be catastrophic for precision and scalability. We present an approach for handling reflection with improved empirical soundness (as measured against prior approaches and dynamic information) in the context of a points-to analysis. Our approach is based on the combination of string-flow and points-to analysis from past literature augmented with (a) substring analysis and modeling of partial string flow through string builder classes; (b) new techniques for analyzing reflective entities based on information available at their use-sites. In experimental comparisons with prior approaches, we demonstrate a combination of both improved soundness (recovering the majority of missing call-graph edges) and increased performance.


title: Analyzing Distributed Multi-platform Java and Android Applications with ShadowVM

authors:
Haiyang Sun
Yudi Zheng
Lubomír Bulej
Stephen Kell
Walter Binder


title: Separation Logic with Monadic Inductive Definitions and Implicit Existentials

authors:
Makoto Tatsuta
Daisuke Kimura


title: Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects

authors:
Tomás Tauber
Xuan Bi
Zhiyuan Shi
Weixin Zhang
Huang Li
Zhenrui Zhang
Bruno C. d. S. Oliveira


title: Quasi-Linearizability is Undecidable

authors:
Chao Wang
Yi Lv
Gaoang Liu
Peng Wu


title: Uncovering JavaScript Performance Code Smells Relevant to Type Mutations

authors:
Xiao Xiao
Shi Han
Charles Zhang
Dongmei Zhang


title: Programming with "Big Code"


title: Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models

authors:
Tatsuya Abe
Toshiyuki Maeda


title: Open Call-by-Value

authors:
Beniamino Accattoli
Giulio Guerrieri


title: A Debugger-Cooperative Higher-Order Contract System in Python

authors:
Ryoya Arai
Shigeyuki Sato
Hideya Iwasaki


title: Learning a Strategy for Choosing Widening Thresholds from a Large Codebase

authors:
Sooyoung Cha
Sehun Jeong
Hakjoo Oh


title: Substructural Proofs as Automata

authors:
Henry DeYoung
Frank Pfenning


title: A Realizability Interpretation for Intersection and Union Types

authors:
Daniel J. Dougherty
Ugo de'Liguoro
Luigi Liquori
Claude Stolze


title: Implementing Cantor's Paradise

authors:
Furio Honsell
Marina Lenisa
Luigi Liquori
Ivan Scagnetto


title: Completeness for a First-Order Abstract Separation Logic

authors:
Zhe Hou
Alwen Tiu

abstract: Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is not possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynolds's semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.


title: Binary Session Types for Psi-Calculi


title: Probabilistic Programming Language and its Incremental Evaluation


title: Refined Environment Classifiers - Type- and Scope-Safe Code Generation with Mutable Cells

authors:
Oleg Kiselyov
Yukiyoshi Kameyama
Yuto Sudo


title: Verifying Concurrent Graph Algorithms

authors:
Azalea Raad
Aquinas Hobor
Jules Villard
Philippa Gardner


title: DOM: Specification and Client Reasoning

authors:
Azalea Raad
José Fragoso Santos
Philippa Gardner


title: Eliom: A Core ML Language for Tierless Web Programming

authors:
Gabriel Radanne
Jérôme Vouillon
Vincent Balat

abstract: Eliom is a dialect of OCaml for Web programming in which server and client pieces of code can be mixed in the same file using syntactic annotations. This allows to build a whole application as a single distributed program, in which it is possible to define in a composable way reusable widgets with both server and client behaviors. Our language also enables simple and type-safe communication. Eliom matches the specificities of the Web by allowing the programmer to interleave client and server code while maintaining efficient one-way server-to-client communication. The Eliom language is both sufficiently small to be implemented on top of an existing language and sufficiently powerful to allow expressing many idioms of Web programming.


title: AkkaProf: A Profiler for Akka Actors in Parallel and Distributed Applications

authors:
Andrea Rosà
Lydia Y. Chen
Walter Binder


title: Static Trace-Based Deadlock Analysis for Synchronous Mini-Go

authors:
Kai Stadtmüller
Martin Sulzmann
Peter Thiemann

abstract: We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for deadlock-freedom. The approach is implemented and evaluated with a series of examples.


title: AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code

authors:
Jiaqi Tan
Hui Jun Tay
Rajeev Gandhi
Priya Narasimhan


title: Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

authors:
Makoto Tatsuta
Quang Loc Le
Wei-Ngan Chin


title: Higher-Order Model Checking in Direct Style

authors:
Taku Terao
Takeshi Tsukada
Naoki Kobayashi


title: SPEC: An Equivalence Checker for Security Protocols

authors:
Alwen Tiu
Nam Nguyen
Ross Horne


title: A Sound and Complete Bisimulation for Contextual Equivalence in \lambda -Calculus with Call/cc

authors:
Taichi Yachi
Eijiro Sumii


title: Unified Syntax with Iso-types

authors:
Yanpeng Yang
Xuan Bi
Bruno C. d. S. Oliveira


title: Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation

authors:
Kazuhide Yasukata
Takeshi Tsukada
Naoki Kobayashi


title: The Negligible and Yet Subtle Cost of Pattern Matching

authors:
Beniamino Accattoli
Bruno Barras


title: Bringing Order to the Separation Logic Jungle

authors:
Qinxiang Cao
Santiago Cuéllar
Andrew W. Appel


title: Compact Difference Bound Matrices

authors:
Aziem Chawdhary
Andy King


title: Black-Box Equivalence Checking Across Compiler Optimizations

authors:
Manjeet Dahiya
Sorav Bansal


title: A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

abstract: In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, \(\lambda _\rho \), follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, \(\lambda _\rho ^\circ \), takes advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.


title: Enforcing Programming Guidelines with Region Types and Effects

authors:
Serdar Erbatur
Martin Hofmann
Eugen Zalinescu

abstract: We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over an arbitrary guideline supplied in the form of a finite monoid or automaton and a type annotation or mockup code for external methods. Furthermore, we add a powerful type inference based on precise interprocedural analysis and provide an implementation in the Soot framework which has been tested on a number of benchmarks including large parts of the Stanford SecuriBench.


title: Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications

authors:
Neline van Ginkel
Raoul Strackx
Frank Piessens


title: Programming by Examples: PL Meets ML

authors:
Sumit Gulwani
Prateek Jain


title: Capabilities for Java: Secure Access to Resources

authors:
Ian J. Hayes
Xi Wu
Larissa A. Meinicke


title: Counterexample-Guided Bit-Precision Selection

authors:
Shaobo He
Zvonimir Rakamaric


title: Safety and Liveness of MCS Lock - Layer by Layer

authors:
Jieung Kim
Vilhelm Sjöberg
Ronghui Gu
Zhong Shao


title: Decision Procedure for Entailment of Symbolic Heaps with Arrays

authors:
Daisuke Kimura
Makoto Tatsuta

abstract: This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al, namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.


title: Sound and Efficient Language-Integrated Query - Maintaining the ORDER

authors:
Oleg Kiselyov
Tatsuya Katsushima


title: Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects

authors:
Yoonseok Ko
Xavier Rival
Sukyoung Ryu


title: Implementing Algebraic Effects in C - "Monads for Free in C"


title: Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

authors:
Ximeng Li
Heiko Mantel
Markus Tasch


title: Programming and Proving with Classical Types

authors:
Cristina Matache
Victor B. F. Gomes
Dominic P. Mulligan


title: A Nonstandard Functional Programming Language

authors:
Hirofumi Nakamura
Kensuke Kojima
Kohei Suenaga
Atsushi Igarashi


title: Verified Root-Balanced Trees


title: Sharper and Simpler Nonlinear Interpolants for Program Verification

authors:
Takamasa Okudono
Yuki Nishida
Kensuke Kojima
Kohei Suenaga
Kengo Kido
Ichiro Hasuo

abstract: Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent result by Dai et al.\ that combines real algebraic geometry and SDP optimization in synthesis of polynomial interpolants, the current paper contributes its enhancement that yields sharper and simpler interpolants. The enhancement is made possible by: theoretical observations in real algebraic geometry; and our continued fraction-based algorithm that rounds off (potentially erroneous) numerical solutions of SDP solvers. Experiment results support our tool's effectiveness; we also demonstrate the benefit of sharp and simple interpolants in program verification examples.


title: Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous

authors:
Adrien Pommellet
Tayssir Touili

abstract: We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Pushdown Networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to an iterative abstraction refinement scheme, using multiple abstractions of increasing complexity and precision.


title: Efficient Functional Reactive Programming Through Incremental Behaviors

authors:
Bob Reynders
Dominique Devriese

abstract: Many types of software are inherently event-driven ranging from web applications to embedded devices and traditionally, such applications are implemented using imperative callbacks. An alternative approach to writing such programs is functional reactive programming (FRP). FRP offers abstractions to make event-driven programming convenient, safe and composable, but they come at a price. FRP behaviors cannot efficiently deal with larger, incrementally constructed values such as a collection of messages or a list of connected devices. Since these situations occur naturally, it hinders the use of FRP. We report on a new FRP primitive: ‘incremental behavior’. We show that the semantics fit within existing FRP semantics and that their API can be used as a foundation for more ad-hoc solutions, such as incremental collections and discrete behaviors. Finally, we present benchmarks that demonstrate the advantages of incremental behaviors in terms of reduced computation time and bandwidth.


title: A Computational Interpretation of Context-Free Expressions

authors:
Martin Sulzmann
Peter Thiemann

abstract: We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a reachability problem by using a canonical representation of states. The proofs-as-programs principle yields a computational interpretation of the reachability problem in terms of a coercion that transforms the parse tree for a context-free expression into a parse tree for a regular expression. It also yields a partial coercion from regular parse trees to context-free ones. The partial coercion from the trivial language of all words to a context-free expression corresponds to a predictive parser for the expression.


title: Partiality and Container Monads

authors:
Tarmo Uustalu
Niccolò Veltri


title: Synthesizing SystemC Code from Delay Hybrid CSP

authors:
Gaogao Yan
Li Jiao
Shuling Wang
Naijun Zhan


title: Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access

authors:
Yongzhe Zhang
Hsiang-Shang Ko
Zhenjiang Hu

abstract: Pregel is a popular distributed computing model for dealing with large-scale graphs. However, it can be tricky to implement graph algorithms correctly and efficiently in Pregel’s vertex-centric model, especially when the algorithm has multiple computation stages, complicated data dependencies, or even communication over dynamic internal data structures. Some domain-specific languages (DSLs) have been proposed to provide more intuitive ways to implement graph algorithms, but due to the lack of support for remote access — reading or writing attributes of other vertices through references — they cannot handle the above mentioned dynamic communication, causing a class of Pregel algorithms with fast convergence impossible to implement.


title: The Practice of a Compositional Functional Programming Language

authors:
Timothy Jones
Michael Homer


title: Types of Fireballs

authors:
Beniamino Accattoli
Giulio Guerrieri


title: Scallina: Translating Verified Programs from Coq to Scala

authors:
Youssef El Bakouny
Dani Mezher


title: Factoring Derivation Spaces via Intersection Types

authors:
Pablo Barenbaum
Gonzalo Ciruelos


title: On the Complexity of Pointer Arithmetic in Separation Logic

authors:
James Brotherston
Max I. Kanovich

abstract: We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study an extension of the points-to fragment of symbolic-heap separation logic with sets of simple “difference constraints” of the form \(x \le y + k\), where x and y are pointer variables and k is an integer offset. This extension can be considered a practically minimal language for separation logic with pointer arithmetic.


title: HoIce: An ICE-Based Non-linear Horn Clause Solver

authors:
Adrien Champion
Naoki Kobayashi
Ryosuke Sato


title: Automated Modular Verification for Relaxed Communication Protocols

authors:
Andreea Costea
Wei-Ngan Chin
Shengchao Qin
Florin Craciun

abstract: Ensuring software correctness and safety for communication-centric programs is important but challenging. In this paper we introduce a solution for writing communication protocols, for checking protocol conformance and for verifying implementation safety. This work draws on ideas from both multiparty session types, which provide a concise way to express communication protocols, as well as from separation-style logics for shared-memory concurrency, which provide strong safety guarantees for resource sharing. On the one hand, our proposal improves the expressiveness and precision of session types, without sacrificing their conciseness. On the other hand, it increases the applicability of software verification as well as its precision, by making it protocol aware. We also show how to perform the verification of such programs in a modular and automatic fashion.


title: Non-linear Pattern Matching with Backtracking for Non-free Data Types

authors:
Satoshi Egi
Yuichi Nishiwaki


title: Automated Synthesis of Functional Programs with Auxiliary Functions

authors:
Shingo Eguchi
Naoki Kobayashi
Takeshi Tsukada


title: Shallow Effect Handlers

authors:
Daniel Hillerström
Sam Lindley


title: New Approaches for Almost-Sure Termination of Probabilistic Programs

authors:
Mingzhang Huang
Hongfei Fu
Krishnendu Chatterjee

abstract: We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explicit optimal bounds on tail probabilities of non-termination within a given number of steps. Second, we present a new approach based on Central Limit Theorem for the almost-sure termination problem, and show that this approach can establish almost-sure termination of programs which none of the existing approaches can handle. Finally, we discuss algorithmic approaches for the two above methods that lead to automated analysis techniques for almost-sure termination of probabilistic programs.


title: Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General

authors:
Hideyuki Kawabata
Yuta Tanaka
Mai Kimura
Tetsuo Hironaka


title: Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine

authors:
Fabian Kunze
Gert Smolka
Yannick Forster

abstract: We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.


title: A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints

authors:
Quang Loc Le
Mengda He


title: Complexity Analysis of Tree Share Structure

authors:
Xuan Bach Le
Aquinas Hobor
Anthony W. Lin

abstract: The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (that is, with all tree-share constants) is decidable and has the same complexity as of the first-order theory of Countable Atomless Boolean Algebras. We prove that combining this additive structure with a constant-restricted unary multiplicative “relativization” operator has a non-elementary lower bound. We examine the consequences of this lower bound and prove that it comes from the combination of both theories by proving an upper bound on a generalization of the restricted multiplicative theory in isolation.


title: Model Checking Differentially Private Properties

authors:
Depeng Liu
Bow-Yaw Wang
Lijun Zhang


title: Particle-Style Geometry of Interaction as a Module System


title: Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks

authors:
Taro Sekiyama
Kohei Suenaga


title: On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features - A Benchmark and Tool Evaluation

authors:
Li Sui
Jens Dietrich
Michael Emery
Shawn Rasheed
Amjed Tahir


title: Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Models

authors:
Thibault Suzanne
Antoine Miné


title: Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS

authors:
Urara Yamada
Kenichi Asai


title: Modular Verification of SPARCv8 Code

authors:
Junpeng Zha
Xinyu Feng
Lei Qiao


title: Factorization and Normalization, Essentially

authors:
Beniamino Accattoli
Claudia Faggian
Giulio Guerrieri

abstract:
Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems.
In this paper we provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi's technique to prove factorization for head reduction. Our technique is both simpler and more powerful, as it works in cases where Takahishi's does not. We then pair factorization with two other abstract properties, defining \emph{essential systems}, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.


title: Lightweight Functional Logic Meta-Programming

authors:
Nada Amin
William E. Byrd
Tiark Rompf


title: J-ReCoVer: Java Reducer Commutativity Verifier

authors:
Yu-Fang Chen
Chang-Yi Chiang
Lukás Holík
Wei-Tsung Kao
Hsin-Hung Lin
Tomás Vojnar
Yean-Fu Wen
Wei-Cheng Wu


title: Simulations in Rank-Based Büchi Automata Complementation

authors:
Yu-Fang Chen
Vojtech Havlena
Ondrej Lengál

abstract: The long search for an optimal complementation construction for Buchi automata climaxed with the work of Schewe, who proposed a worst-case optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of (0.76n)n, modulo a polynomial factor of O(n2). Although worst-case optimal, the procedure in many cases produces automata that are unnecessarily large. In this paper, we propose several ways of how to use the direct and delayed simulation relations to reduce the size of the automaton obtained in the rank-based complementation procedure. Our techniques are based on either (i) ignoring macrostates that cannot be used for accepting a word in the complement or (ii) saturating macrostates with simulation-smaller states, in order to decrease their total number. We experimentally showed that our techniques can indeed considerably decrease the size of the output of the complementation.


title: Existential Types for Relaxed Noninterference

authors:
Raimil Cruz
Éric Tanter

abstract:
Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data. Several approaches have provided a notion of relaxed noninterference supporting selective and expressive declassification while retaining a formal security property. The labels-as-functions approach provides relaxed noninterference by means of declassification policies expressed as functions. The labels-as-types approach expresses declassification policies using type abstraction and faceted types, a pair of types representing the secret and public facets of values. The original proposal of labels-as-types is formulated in an object-oriented setting where type abstraction is realized by subtyping. The object-oriented approach however suffers from limitations due to its receiver-centric paradigm.
In this work, we consider an alternative approach to labels-as-types, applicable in non-object-oriented languages, which allows us to express advanced declassification policies, such as extrinsic policies, based on a different form of type abstraction: existential types. An existential type exposes abstract types and operations on these; we leverage this abstraction mechanism to express secrets that can be declassified using the provided operations. We formalize the approach in a core functional calculus with existential types, define existential relaxed noninterference, and prove that well-typed programs satisfy this form of type-based relaxed noninterference.


title: TxForest: A DSL for Concurrent Filestores

authors:
Jonathan DiLorenzo
Katie Mancini
Kathleen Fisher
Nate Foster

abstract: Many systems use ad hoc collections of files and directories to store persistent data. For consumers of this data, the process of properly parsing, using, and updating these filestores using conventional APIs is cumbersome and error-prone. Making matters worse, most filestores are too big to fit in memory, so applications must process the data incrementally while managing concurrent accesses by multiple users. This paper presents Transactional Forest (TxForest), which builds on earlier work on Forest to provide a simpler, more powerful API for managing filestores, including a mechanism for managing concurrent accesses using serializable transactions. Under the hood, TxForest implements an optimistic concurrency control scheme using Huet's zippers to track the data associated with filestores. We formalize TxForest in a core calculus, develop a proof of serializability, and describe our OCaml prototype, which we have used to build several practical applications.


title: Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects

authors:
Thomas D. Dickerson
Eric Koskinen
Paul Gazzillo
Maurice Herlihy


title: Dissecting Widening: Separating Termination from Information

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


title: Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps

authors:
Jinlong He
Taolue Chen
Ping Wang
Zhilin Wu
Jun Yan


title: Pumping, with or Without Choice

authors:
Aquinas Hobor
Elaine Li
Frank Stephan


title: On Strings in Software Model Checking

authors:
Hossein Hojjat
Philipp Rümmer
Ali Shamakhi


title: Succinct Determinisation of Counting Automata via Sphere Construction

authors:
Lukás Holík
Ondrej Lengál
Olli Saarikivi
Lenka Turonová
Margus Veanes
Tomás Vojnar

abstract: We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the naive approach, and thus produces much smaller deterministic automata. We also develop a simplified and faster version of the general algorithm for the sub-class of so-called monadic CAs (MCAs), i.e., CAs with counting loops on character classes, which are common in practice. Our main motivation is (besides applications in verification and decision procedures of logics) the application of deterministic (M)CAs in pattern matching regular expressions with counting, which are very common in e.g. network traffic processing and log analysis. We have evaluated our algorithm against practical benchmarks from these application domains and concluded that compared to the naive approach, our algorithm is much less prone to explode, produces automata that can be several orders of magnitude smaller, and is overall faster.


title: A Type-Based HFL Model Checking Algorithm

authors:
Youkichi Hosoi
Naoki Kobayashi
Takeshi Tsukada

abstract: Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is based on Kobayashi et al.'s type-based characterization of HFL model checking, and was inspired by a saturation-based algorithm for HORS model checking, another higher-order extension of model checking. We prove the correctness of the algorithm and report on an implementation and experimental results.


title: A Dependently Typed Multi-stage Calculus

authors:
Akira Kawata
Atsushi Igarashi

abstract:
We study a dependently typed extension of a multi-stage programming language a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct for execution of programs dynamically generated by this code manipulation. Dependent types are expected to bring to multi-stage programming enforcement of strong invariant---beyond simple type safety---on the behavior of dynamically generated code. An extension is, however, not trivial because such a type system would have to take stages of types ---roughly speaking, the number of surrounding quotations---into account.
To rigorously study properties of such an extension, we develop $\lambda^{MD}$, which is an extension of Hanada and Igarashi's typed calculus $\lambda^{\triangleright\%} $ with dependent types, and prove its properties including preservation, confluence, strong normalization for full reduction, and progress for staged reduction. Motivated by code generators that generate code whose type depends on a value from outside of the quotations, we argue the significance of cross-stage persistence in dependently typed multi-stage programming and certain type equivalences that are not directly derived from reduction rules.


title: Mimalloc: Free List Sharding in Action

authors:
Daan Leijen
Benjamin Zorn
Leonardo de Moura


title: Proving that Programs Are Differentially Private

authors:
Annabelle McIver
Carroll Morgan


title: Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion

authors:
Masayuki Mizuno
Eijiro Sumii


title: Recursion Schemes in Coq

authors:
Kosuke Murata
Kento Emoto


title: Reducing Static Analysis Alarms Based on Non-impacting Control Dependencies

authors:
Tukaram Muske
Rohith Talluri
Alexander Serebrenik


title: LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

abstract: Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users' expertise to new Isabelle users.


title: Manifest Contracts with Intersection Types

authors:
Yuki Nishida
Atsushi Igarashi

abstract: We present a manifest contract system PCFv$\Delta$H with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a refinement type system and consistency of contracts is checked by combination of compile- and run-time type checking. Intersection types naturally arise when a contract is expressed by a conjunction of smaller contracts. Run-time contract checking for conjunctive higher-order contracts in an untyped language has been studied but our typed setting poses an additional challenge due to the fact that an expression of an intersection type $\tau_1 \wedge \tau_2$ may have to perform different run-time checking whether it is used as $\tau_1$ or $\tau_2$. We build PCFv$\Delta$H on top of the $\Delta$-calculus, a Church-style intersection type system by Liquori and Stolze. In the $\Delta$-calculus, a canonical expression of an intersection type is a strong pair, whose elements are the same expressions except for type annotations. To address the challenge above, we relax strong pairs so that expressions in a pair are the same except for type annotations and casts, which are a construct for run-time checking. We give a formal definition of PCFv$\Delta$H and show its basic properties as a manifest contract system: preservation, progress, and value inversion. Furthermore, we show that run-time checking does not affect essential computation.


title: Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning

authors:
Long H. Pham
Jun Sun
Quang Loc Le

abstract: Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.


title: Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions

authors:
Makoto Tatsuta
Koji Nakazawa
Daisuke Kimura


title: Uniform Random Process Model Revisited

authors:
Wenbo Zhang
Huan Long
Xian Xu


title: An Abstract Machine for Strong Call by Value

authors:
Malgorzata Biernacka
Dariusz Biernacki
Witold Charatonik
Tomasz Drab

abstract:
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $\lambda$-calculus. It is derived using Danvy et al.'s functional correspondence from Cregut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine.
This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al.'s generalized refocusing. As a byproduct, we present an example application of the machine to checking term convertibility by discriminating on the basis of their partially normalized forms.


title: Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language

authors:
Mario Bravetti
Adrian Francalanza
Iaroslav Golovanov
Hans Hüttel
Mathias Jakobsen
Mikkel Kettunen
António Ravara

abstract: We present a type-based analysis ensuring memory safety and object protocol completion in the Java-like language Mungo. Objects are annotated with usages, typestates-like specifications of the admissible sequences of method calls. The analysis entwines usage checking, controlling the order in which methods are called, with a static check determining whether references may contain null values. The analysis prevents null pointer dereferencing and memory leaks and ensures that the intended usage protocol of every object is respected and completed. The type system has been implemented in the form of a type checker.


title: Declarative Stream Runtime Verification (hLola)

authors:
Martín Ceresa
Felipe Gorostiaga
César Sánchez

abstract: Stream Runtime Verification is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing to compute richer verdicts than Booleans (including quantitative and arbitrary data). In this paper we study the problem of implementing an SRV engine that is truly extensible to arbitrary data theories, and we propose a solution as a Haskell embedded domain specific language. In spite of the theoretical clean separation in SRV between temporal dependencies and data computations, previous engines include ad-hoc implementations of a few data types, requiring complex changes to incorporate new data theories. We propose here an SRV language called hLola that borrows general Haskell types and embeds them transparently into an eDSL. This novel technique, which we call lift deep embedding, allows for example, the use of higher-order functions for static stream parameterization. We describe the Haskell implementation of hLola and illustrate simple extensions implemented using libraries, which require long and error-prone additions in other ad-hoc SRV formalisms.


title: A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving

authors:
Yu-Fang Chen
Vojtech Havlena
Ondrej Lengál
Andrea Turrini


title: Banyan: Coordination-Free Distributed Transactions over Mergeable Types

authors:
Shashank Shekhar Dubey
K. C. Sivaramakrishnan
Thomas Gazagnaire
Anil Madhavapeddy


title: A Set-Based Context Model for Program Analysis

authors:
Leandro Facchinetti
Zachary Palmer
Scott F. Smith
Ke Wu
Ayaka Yorihiro


title: Formal Verification of Atomicity Requirements for Smart Contracts

authors:
Ning Han
Ximeng Li
Guohui Wang
Zhiping Shi
Yong Guan


title: A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking

authors:
Hiroyuki Katsura
Naoki Iwayama
Naoki Kobayashi
Takeshi Tsukada


title: Neural Networks, Secure by Construction - An Exploration of Refinement Types

authors:
Wen Kokke
Ekaterina Komendantskaya
Daniel Kienitz
Robert Atkey
David Aspinall


title: Relational Synthesis for Pattern Matching

authors:
Dmitry Kosarev
Petr Lozov
Dmitry Boulytchev


title: Automatically Generating Descriptive Texts in Logging Statements: How Far Are We?

authors:
Xiaotong Liu
Tong Jia
Ying Li
Hao Yu
Yang Yue
Chuanjia Hou


title: Syntactically Restricting Bounded Polymorphism for Decidable Subtyping

authors:
Julian Mackay
Alex Potanin
Jonathan Aldrich
Lindsay Groves