title: (De/Re)-Composition of Data-Parallel Computations via Multi-Dimensional Homomorphisms

abstract: Data-parallel computations, such as linear algebra routines and stencil computations, constitute one of the most relevant classes in parallel computing, e.g., due to their importance for deep learning. Efficiently de-composing such computations for the memory and core hierarchies of modern architectures and re-composing the computed intermediate results back to the final result—we say (de/re)-composition for short—is key to achieve high performance for these computations on, e.g., GPU and CPU. Current high-level approaches to generating data-parallel code are often restricted to a particular subclass of data-parallel computations and architectures (e.g., only linear algebra routines on only GPU or only stencil computations), and/or the approaches rely on a user-guided optimization process for a well-performing (de/re)-composition of computations, which is complex and error prone for the user. We formally introduce a systematic (de/re)-composition approach, based on the algebraic formalism of Multi-Dimensional Homomorphisms (MDHs). Our approach is designed as general enough to be applicable to a wide range of data-parallel computations and for various kinds of target parallel architectures. To efficiently target the deep and complex memory and core hierarchies of contemporary architectures, we exploit our introduced (de/re)-composition approach for a correct-by-construction, parametrized cache blocking, and parallelization strategy. We show that our approach is powerful enough to express, in the same formalism, the (de/re)-composition strategies of different classes of state-of-the-art approaches (scheduling-based, polyhedral, etc.), and we demonstrate that the parameters of our strategies enable systematically generating code that can be fully automatically optimized (auto-tuned) for the particular target architecture and characteristics of the input and output data (e.g., their sizes and memory layouts). Particularly, our experiments confirm that via auto-tuning, we achieve higher performance than state-of-the-art approaches, including hand-optimized solutions provided by vendors (such as NVIDIA cuBLAS/cuDNN and Intel oneMKL/oneDNN), on real-world datasets and for a variety of data-parallel computations, including linear algebra routines, stencil and quantum chemistry computations, data mining algorithms, and computations that recently gained high attention due to their relevance for deep learning.


venue: toplas

title: CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams

authors:
Meghana Aparna Sistla
Swarat Chaudhuri
Thomas W. Reps

abstract: This article presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence are useful for representing certain classes of functions, matrices, graphs, relations, and so forth in a highly compressed fashion. CFLOBDDs share many of the good properties of BDDs, but—in the best case—the CFLOBDD for a Boolean function can be exponentially smaller than any BDD for that function . Compared with the size of the decision tree for a function, a CFLOBDD—again, in the best case—can give a double-exponential reduction in size . They have the potential to permit applications to (i) execute much faster and (ii) handle much larger problem instances than has been possible heretofore. We applied CFLOBDDs in quantum-circuit simulation and found that for several standard problems, the improvement in scalability, compared to BDDs, is quite dramatic. With a 15-minute timeout, the number of qubits that CFLOBDDs can handle are 65,536 for Greenberger-Horne-Zellinger, 524,288 for Bernstein-Vazirani, 4,194,304 for Deutsch-Jozsa, and 4,096 for Grover’s algorithm, besting BDDs by factors of 128×, 1,024×, 8,192×, and 128×, respectively.


title: Interactive Abstract Interpretation with Demanded Summarization

authors:
Benno Stein
Bor-Yuh Evan Chang
Manu Sridharan

abstract: We consider the problem of making expressive, interactive static analyzers compositional . Such a technique could help bring the power of server-based static analyses to integrated development environments (IDEs), updating their results live as the code is modified. Compositionality is key for this scenario, as it enables reuse of already-computed analysis results for unmodified code. Previous techniques for interactive static analysis either lack compositionality, cannot express arbitrary abstract domains, or are not from-scratch consistent. We present demanded summarization, the first algorithm for incremental compositional analysis in arbitrary abstract domains that guarantees from-scratch consistency. Our approach analyzes individual procedures using a recent technique for demanded analysis, computing summaries on demand for procedure calls. A dynamically updated summary dependency graph enables precise result invalidation after program edits, and the algorithm is carefully designed to guarantee from-scratch-consistent results after edits, even in the presence of recursion and in arbitrary abstract domains. We formalize our technique and prove soundness, termination, and from-scratch consistency. An experimental evaluation of a prototype implementation on synthetic and real-world program edits provides evidence for the feasibility of this theoretical framework, showing potential for major performance benefits over non-demanded compositional analyses.


title: Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

authors:
Cyril Cohen
Enzo Crance
Assia Mahboubi

abstract: This article presents Trocq , a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq/Coq interactive theorem prover, in the Coq-Elpi meta-language.


title: Circuit Width Estimation via Effect Typing and Linear Dependency

authors:
Andrea Colledan
Ugo Dal Lago
Niki Vazou

abstract: Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit . Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this article, we present Proto-Quipper-R , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. Lastly, we introduce QuRA , a static analysis tool based on Proto-Quipper-R ’s type system, and use it to show that our framework allows for the automatic width verification of realistic quantum algorithms, such as the QFT and Grover’s algorithm.


title: Editorial: New Year, New Paper Tracks

abstract: I am excited to take up the mantle and will do my utmost to take the journal from strength to strength over the coming years!I am extremely grateful to Colin Gordon, outgoing Editor-in-Chief, for the many hours he has spent showing me the ropes, which has made taking on this new role much less daunting


title: Modal Crash Types for WAR-Aware Intermittent Computing

authors:
Myra Dotzel
Farzaneh Derakhshan
Milijana Surbatovich
Limin Jia

abstract: Programs are executed intermittently on devices that experience arbitrary power failures such as Energy Harvesting Devices (EHDs). To ensure progress, intermittent systems need runtime support to checkpoint state and re-execute after power failure by restoring the last saved state. Such re-execution should be correct , i.e., simulated by a continuously-powered execution. We study the logical underpinning of intermittent computing and model checkpoint, crash, restore, and re-execution operations as computation on crash types. We draw inspiration from adjoint logic and define crash types by introducing two adjoint modality operators to model persistent and transient memory values of partial (re-)executions and the transitions between them caused by checkpoints and restoration. Our formalism is general enough to accommodate a variety of checkpointing policies. We define a crash type system for a core calculus. To prove the correctness of intermittent systems, we define a novel logical relation for crash types.


title: A Brookes-Style Denotational Semantics for Release/Acquire Concurrency

authors:
Yotam Dvir
Ohad Kammar
Ori Lahav

abstract: We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic approach and is based on Brookes-style traces. To do so we adapt Brookes’s traces to view-based machine for RA by Kang et al., and supplement Brookes’s mumble and stutter closure operations with additional operations, specific to RA. The latter provides a more nuanced understanding of traces that uncouples them from operational interrupted executions. We show that our denotational semantics is adequate and use it to validate various program transformations of interest. This is the first work to put weak memory models on the same footing as many other programming effects in Moggi’s standard monadic approach.


title: Generic Bidirectional Typing for Dependent Type Theories

abstract: Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing one to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of bidirectional type theories, each giving rise to both a declarative and a bidirectional type system. We then show, in a theory-independent fashion, that the two systems are equivalent. Finally, we establish the decidability of bidirectional typing for normalizing theories, yielding a generic typing algorithm that has been implemented in a prototype and used in practice with many theories.


title: Monadic Intersection Types, Relationally, and Ordered

authors:
Zeinab Galal
Francesco Gavazzo
Riccardo Treglia
Gabriele Vanoni

abstract: We extend intersection types to a computational \(\lambda\) -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics but also in the type system . Since in the effectful setting, termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system can characterize the natural notion of observation, both in the finitary and in the infinitary setting. In a second phase, we extend our system with subtyping to incorporate a richer class of effects via monads on preorders instead of sets allowing us to model in particular non-determinism. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, for example, of typability and logical relation, to the monadic setting.


title: Squibs and Discussions at TOPLAS


title: Changing of the Seasons at TOPLAS

abstract: No abstract available.


title: Sound Static Data Race Verification for C: Is the Race Lost?

authors:
Karoliine Holter
Simmo Saan
Patrick Lam
Vesal Vojdani

abstract: Sound static data race freedom verification has been a long-standing challenge in the field of programming languages. While actively researched a decade ago, most practical data race detection tools have since abandoned soundness. Is sound static race freedom verification for real-world C programs a lost cause? In this work, we investigate the obstacles to making significant progress in automated race freedom verification. We selected a benchmark suite of real-world programs and, as our primary contribution, extracted a set of coding idioms that represent fundamental barriers to verification. We expressed these idioms as micro-benchmarks and contributed them as evaluation tasks for the International Competition on Software Verification, SV-COMP. To understand the current state, we measure how sound automated verification tools competing in SV-COMP perform on these idioms and also when used out of the box on the real-world programs. For 8 of the 20 coding idioms, there does exist an automated race freedom verifier that can verify it; however, we also found significant unsoundness in leading verifiers, including Goblint and Deagle. Five of the seven tools failed to return any result on any real-world benchmarks under our chosen resource limitations, with the remaining two tools verifying race freedom for 2 of the 18 programs and crashing or returning inconclusive results on the others. We thus show that state-of-the-art verifiers have both superficial and fundamental barriers to correctly analyzing real-world programs. These barriers constitute the open problems that must be solved to make progress on automated static data race freedom verification.


title: Rate-Based Session Types for IoT Systems

authors:
Grant Iraci
Cheng-En Chuang
Raymond Hu
Lukasz Ziarek

abstract: We develop a session types framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursion primitive. This allows us to model rate-based computations and communications inherent to these application domains. We introduce a definition of rate-based session types in a binary session types setting and a new compatibility relationship, which we call rate compatibility . Programs which type-check enjoy the standard session types guarantees as well as rate error freedom—meaning processes which exchanges messages do so at the same rate . Rate compatibility is defined through a new notion of type expansion, a relation that allows communication between processes of differing periods by synthesizing and checking a common superperiod type. We prove type preservation and rate error freedom for our system and show a decidable method for type checking based on computing superperiods for a collection of processes. We implement a prototype of our type system including rate compatibility via an embedding into the native type system of Rust. We apply this framework to a range of examples from our target domain such as Android software sensors, wearable devices, and sound processing. Our framework is used to implement a heart rate sensor application that runs on a commercially available smartwatch.


title: Scoped Effects, Scoped Operations, and Parameterized Algebraic Theories

authors:
Cristina Matache
Sam Lindley
Sean K. Moss
Sam Staton
Nicolas Wu
Zhixuan Yang

abstract: Notions of computation can be modeled by monads. Algebraic effects offer a characterization of monads in terms of algebraic operations and equational axioms, where operations are basic programming features, such as reading or updating the state, and axioms specify observably equivalent expressions. However, many useful programming features depend on additional mechanisms such as delimited scopes or dynamically allocated resources. Such mechanisms can be supported via extensions to algebraic effects including scoped effects and parameterized algebraic theories . We present a fresh perspective on scoped effects by translation into a variation of parameterized algebraic theories. The translation enables a new approach to equational reasoning for scoped effects and gives rise to an alternative characterization of monads in terms of generators and equations involving both scoped and algebraic operations. We demonstrate the power of our approach by way of equational characterizations of several known models of scoped effects.


title: A Modular Approach to Metatheoretic Reasoning for Extensible Languages

authors:
Dawn Michaelson
Gopalan Nadathur
Eric Van Wyk

abstract: This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In this context, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of modular metatheory , by which we mean that proofs of relevant properties should be constructible by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called Sterling and a proof assistant called Extensibella and have used them to validate the examples that motivate the theoretical discussions.


title: Will It Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection

authors:
Alexandre Moine
Arthur Charguéraud
François Pottier

abstract: We present IrisFit, a Separation Logic with space credits for reasoning about heap space in a concurrent call-by-value language equipped with tracing garbage collection and shared mutable state. We point out a fundamental difficulty in the analysis of the worst-case heap space complexity of concurrent programs in the presence of tracing garbage collection: If garbage collection phases and program steps can be arbitrarily interleaved, then there exist undesirable scenarios where a root held by a sleeping thread prevents a possibly large amount of memory from being freed. To remedy this problem and eliminate such undesirable scenarios, we propose several language features, namely possibly-blocking memory allocation, polling points, and protected sections. Polling points are meant to be automatically inserted by the compiler; protected sections are delimited by the programmer and represent regions where no polling points must be inserted. The heart of our contribution is IrisFit, a novel program logic that can establish worst-case heap space complexity bounds and whose reasoning rules can take advantage of the presence of protected sections. IrisFit is formalized inside the Coq proof assistant, on top of the Iris Separation Logic framework. We prove that IrisFit offers both a safety guarantee—programs cannot crash and cannot exceed a heap space limit—and a liveness guarantee—provided enough polling points have been inserted, every memory allocation request is satisfied in bounded time. We illustrate the use of IrisFit via several case studies, including a version of Treiber’s stack whose worst-case behavior relies on the presence of protected sections.


title: Observational Equality Meets CIC

authors:
Loïc Pujet
Yann Leray
Nicolas Tabareau

abstract: The notion of equality is at the heart of dependent type theory, as it plays a fundamental role in program specifications and mathematical reasoning. In mainstream proof assistants such as Agda , Lean , and Coq , equality is usually defined using Martin-Löf’s identity type, an elegant and simple approach that has stood the test of time since the 1970s. However, this definition also comes with serious downsides: the intensional nature of Martin-Löf’s identity type means that it is impractical for reasoning about functions and predicates, and it is impossible to define quotient types. Recently, observational equality has garnered attention as an alternative method for encoding equality, particularly in proof assistants supporting definitionally proof-irrelevant propositions. However, it has yet to be integrated in any of the three proof assistants mentioned above, as it is not fully compatible with another important feature of type theory: indexed inductive types. In this article, we propose a systematic approach to reconcile observational equality with indexed inductive types, using a type coercion operator that computes on reflexive identity proofs. The second contribution of this article is a formal proof that this additional computation rule can be integrated to the system without compromising the decidability of conversion. Finally, we provide an implementation of our observational equality in an extension of Coq . This extension is based on the recently introduced rewrite rules and provides new extensionality principles while remaining fully backward-compatible.


title: Type-Safe Compilation of Dynamic Inheritance via Merging

authors:
Yaozhu Sun
Xuejing Huang
Bruno C. d. S. Oliveira

abstract: Inheritance is a key concept in many programming languages. Dynamically typed languages, such as JavaScript, often support powerful forms of dynamic inheritance. However, dynamic inheritance poses significant challenges for static typing. Most statically typed languages only provide static inheritance to achieve type safety at the cost of flexibility. This article presents a compiler for the CP language, which is a statically typed language that supports dynamic inheritance via a merge operator and also has an expressive form of parametric polymorphism. The merge operator enables a form of multiple inheritance and first-class classes, as well as virtual classes and family polymorphism. With these features, CP allows the development of highly modular and loosely coupled components. However, the efficient compilation of CP code is non-trivial, especially if separate compilation is desired. In particular, subtyping in CP is coercive for type safety, which poses significant challenges in obtaining an efficient compilation scheme. We show how CP is compilable to languages supporting extensible records or similar data structures, where record labels are generated from types for efficient lookup on merges. The main ideas of the compilation scheme are formalized in Coq and proven to be type-safe. The concrete implementation of the CP compiler targets JavaScript, where records are modeled as JavaScript objects. We conduct an empirical evaluation with various benchmarks and evaluate the impact of several CP-specific optimizations. With our optimizations, CP can be orders of magnitude faster than with a naive compilation scheme for merges, obtaining performance on par with class-based JavaScript programs.


title: Editorial: Embracing the Empirical with the New PL Experiments Track


title: Synthesizing Invariants for Polynomial Programs by Semidefinite Programming

authors:
Hao Wu
Qiuye Wang
Bai Xue
Naijun Zhan
Lihong Zhi
Zhi-Hong Yang

abstract: Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the strong invariant synthesis problem , while the problem of finding a concrete valid parameter assignment is called the weak invariant synthesis problem . For both problems, the challenge lies in solving or reducing the encoded constraints, which are generally non-convex and lack efficient solvers. In this article, we propose two novel algorithms for synthesizing invariants of polynomial programs using semidefinite programming (SDP): (1) The Cluster algorithm targets the strong invariant synthesis problem for polynomial invariant templates. Leveraging robust optimization techniques, it solves a series of SDP relaxations and yields a sequence of increasingly precise under-approximations of the set of valid parameter assignments. We prove the algorithm’s soundness, convergence, and weak completeness under a specific robustness assumption on templates. Moreover, the outputs can simplify the weak invariant synthesis problem. (2) The Mask algorithm addresses the weak invariant synthesis problem in scenarios where the aforementioned robustness assumption does not hold, rendering the Cluster algorithm ineffective. It identifies a specific subclass of invariant templates, termed masked templates, involving parameterized polynomial equalities and known inequalities. By applying variable substitution, the algorithm transforms constraints into an equivalent form amenable to SDP relaxations. Both algorithms have been implemented and demonstrated superior performance compared to state-of-the-art methods in our empirical evaluation.


title: Polynomial Bounds of CFLOBDDs against BDDs

authors:
Xusheng Zhi
Thomas Reps

abstract: Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs—roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, “For a given family of Boolean functions F , what is the relationship between the size of a BDD for \(f\in F\) and the size of a CFLOBDD for f ?” Sistla et al. established that there are best-case families of functions , which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions \(\{f_{n}\}\) for which, for all \(n=2^{k}\) , the CFLOBDD for \(f_{n}\) (using a particular variable order) is exponentially more succinct than any BDD for \(f_{n}\) (i.e., using any variable order). However, they did not give a worst-case bound —i.e., they left open the question, “Is there a family of functions \(\{g_{i}\}\) for which the size of a CFLOBDD for \(g_{i}\) must be substantially larger than a BDD for \(g_{i}\) ?” For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs. This article studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function h cannot be far worse than the size of the BDD for h . The bound that relates their sizes is polynomial: The article also shows that the bound is tight: there is a family of functions for which \(|C|\) grows as \(\Omega(|B|^{3})\) .


title: Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects

abstract: Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the different kinds of programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice. Outcome Logic reimagines Hoare Logic with branching at its core, using an algebraic representation of choice to capture programs that branch into many outcomes. In this article, we give a comprehensive account of the Outcome Logic metatheory. This includes a relatively complete proof system for Outcome Logic with the ability to reason about general purpose looping. We also show that this proof system applies to programs with various types of branching, that it subsumes some well-known logics such as Hoare Logic, and that it facilitates the reuse of proof fragments across different kinds of specifications.


title: A Sound Type System for Secure Currency Flow

authors:
Luca Aceto
Daniele Gorla
Stian Lybech

abstract: In this article, we focus on TinySol , a minimal calculus for Solidity smart contracts, introduced by Bartoletti, Galletta and Murgia. We start by rephrasing its syntax (to emphasise its object-oriented flavour) and give a new big-step operational semantics for that language. We then use it to define two security properties, namely call integrity and noninterference. These two properties have some similarities in their definition, in that they both require that some part of a program is not influenced by the other part. However, we show that the two properties are actually incomparable. Nevertheless, we provide a type system that statically ensures both noninterference and call integrity; hence, well-typed programs satisfy both properties. We finally discuss the practical usability of the type system and its limitations by means of some simple examples.


title: Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

authors:
Danel Ahman
Karthikeyan Bhargavan
Barry Bond
Jay Bosamiya
Christopher Brzuska
Antoine Delignat-Lavaud
Cédric Fournet
Aymeric Fromherz
Sydney Gibson
Chris Hawblitzel
Catalin Hritcu
Markulf Kohlweiss
Guido Martínez
Haobin Ni
Bryan Parno
Jonathan Protzenko
Tahina Ramananandro
Aseem Rastogi
Exequiel Rivas
Nikhil Swamy
Santiago Zanella-Béguelin

abstract: Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.


title: StreamAlloc: A Framework for Analyzing and Transforming CUDA Code to Enable Asynchronous Execution

authors:
Soumik Kumar Basu
Jyothi Vedurada

abstract: In the CUDA programming model, data transfers on the default stream are synchronous, and, similarly, device kernels launched on the default stream cannot overlap with other kernel computations and data transfers. Overlapping execution can be enabled using asynchronous APIs and streams in CUDA. Using them, however, requires careful handling of data dependencies across multiple data transfer calls, host operations, and kernel computations to ensure program correctness. Moreover, numerous data transfer calls and kernel calls in a program make it even more challenging to manually assign the appropriate stream identifier for each such call. This challenge remains daunting for non-expert programmers because they lack the right tools and expertise. To address this, we propose sync2async, a novel optimization technique that transforms synchronous data transfers and kernel launches into non-default-stream asynchronous calls by allocating stream identifiers (and adding stream synchronizations at appropriate places) to maximize parallelizability while preserving dependencies. To identify sync2async opportunities and apply transformations, we introduce StreamAlloc, a dataflow-analysis-based framework with four components: (1) inter-procedural compositional read–write analysis to identify variables read and written at call sites, (2) intra-procedural flow-sensitive Can-Run-Asynchronously (CRA) analysis to detect data transfer and kernel calls that can run asynchronously, (3) Dataflow Stream Assignment (DFSA) algorithm to schedule such asynchronous calls to different non-default streams, and (4) a transformation framework to apply sync2async and automatically optimize the input program. We have implemented StreamAlloc using LLVM/Clang. On P100, A4000, and A100 GPUs, sync2async achieves geomean speedups of 1.49×, 1.63×, and 2.02× over the baseline, respectively.


title: Denotation-based Compositional Compiler Verification

authors:
Zhang Cheng
Jiyang Wu
Di Wang
Qinxiang Cao

abstract: A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that of its substructures ranging from statements, functions, and modules. This article proposes a novel compiler verification framework based on denotational semantics for better compositionality, compared to previous approaches based on small-step operational semantics and simulation theories. Our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral sets , with compiler correctness established through behavior refinement between the semantic domains of the source and target programs. The main contributions of this article include proposing a denotational semantics for open modules, a novel semantic linking operator, and a refinement algebra that unifies various behavior refinements, making compiler verification structured and compositional. Furthermore, our formalization captures the full meaning of a program and bridges the gap between traditional power-domain-based denotational semantics and the practical needs of compiler verification. We apply our denotation-based framework to verify the front-end of CompCert and typical optimizations on simple prototypes of imperative languages. Our results demonstrate that the compositionality from sub-statements to statements, from functions to modules, and from modules to the whole program can be effectively achieved.


title: Navigating Mixed-Typed Migration with Profilers

authors:
Nathaniel Hejduk
Ben Greenman
Matthias Felleisen
Christos Dimoulas

abstract: The component-by-component migration of a program from untyped to typed can trigger unintended performance degradations. When such a degradation occurs, typing well-chosen components can lessen the cost of type enforcement, while typing poorly chosen components can exacerbate it. This article examines whether off-the-shelf profiling tools deliver information that is an effective guide for navigating these migration choices in Typed Racket. Using the rational-programmer method, the article tests this hypothesis with an experiment that involves tens of thousands of performance-debugging scenarios, two different profiler types, and 23 strategies that convert profiler output to migration choices. The most effective strategy relies on a boundary profiler to identify the costliest inter-component boundary and then adds deeply enforced types to both sides. When the output of this profiler fails to identify a boundary, the strategy takes a random migration step—similar to the way many computational approaches resort temporarily to random choices to avoid getting stuck. The strategy completely eliminates the cost of run-time type checks in more than half of the scenarios if at most two performance degradations are tolerable along the way.


title: A Typed Intermediate Representation for Dynamic Languages

authors:
Mickaël Laurent
Jakob Hain
Filip Krikava
Sebastián Krynski
Jan Vitek

abstract: Dynamic programming languages pose significant challenges for optimizing compilers due to features such as dynamic typing, late binding, reflection, copy-on-write, and delayed evaluation. To generate efficient code, compilers must speculate on which dynamic features will be exercised and produce specialized code based on these assumptions. This article presents the design of a statically typed, high-level intermediate representation (IR) that makes dynamic behaviors explicit and amenable to static analysis. Our IR combines gradual typing with ownership tracking, and explicitly represents promises, multiple function versions, and contextual dispatch. Together, these features directly support optimizations such as specialization, inlining, scope elision, and copy elimination. We formalize a core calculus, called FIŘ, that captures the essential features required for these optimizations. We provide an operational semantics, a type system, and flow and reflection analyses, and we prove the soundness of the type system.


title: Guiding LLM-Based Loop Invariant Synthesis via Feedback on Local Reasoning Errors

authors:
Tianchi Li
Zhenyu Yan
Junhao Liu
Peng Di
Xin Zhang

abstract: We propose a novel framework that provides constructive feedback to an LLM in the “guess-and-check” paradigm by formally verifying its own thinking process and detecting local reasoning errors. We apply this framework to the loop invariant synthesis problem. We prompt the model to produce a step-by-step natural language proof justifying its thinking process for the failed verification condition of its generated loop invariants. Then, we use an LLM to translate the reasoning steps into first-order logic implications, which can be checked automatically. An invalid implication pinpoints the exact logical flaw in the LLM’s thinking process, which we then use to construct targeted feedback for refinement. We have implemented our approach in a tool called LORIS and evaluated it on a main benchmark suite of 460 C programs and an additional benchmark suite of 50 C programs each of which involves non-linear properties. On the main benchmark suite, LORIS solved 445 of the programs and achieved an overall success rate of 93.1%. LORIS also demonstrates robustness on the challenging non-linear benchmark suite.


title: An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics

authors:
Zongyuan Liu
Angus Hammond
Thibaut Pérami
Peter Sewell
Lars Birkedal
Jean Pichon-Pharabod

abstract: Very relaxed concurrency memory models, like those of the Arm-A, RISC-V and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the ‘current’ state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a family of separation logics for relaxed hardware memory models, and instantiate it on sequential consistency and on the Arm-A memory model. The Arm-A instance captures the fine-grained reasoning underpinning the low-overhead synchronisation idioms used by high-performance systems code. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. By instantiating AxSL on different memory models, we demonstrate the generality of our approach, and show that it is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other models, and for the combination of production concurrency models and full-scale ISAs.


title: Fair Termination of Asynchronous Binary Sessions

authors:
Luca Padovani
Gianluigi Zavattaro

abstract: We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.


title: Scaling Inter-procedural Dataflow Analysis on the Cloud

authors:
Zewen Sun
Yujin Zhang
Yueyang Wang
Duanchen Xu
Yiyu Zhang
Yun Qi
Zhaokang Wang
Yue Li
Xuandong Li
Qingda Lu
Wenwen Peng
Shengjian Guo
Zhiqiang Zuo

abstract: Apart from forming the backbone of compiler optimization, static dataflow analysis has been widely applied in a vast variety of applications, such as bug detection, privacy analysis, and program comprehension. Despite its importance, performing inter-procedural dataflow analysis on large-scale programs is well-known to be challenging. In this article, we propose a novel distributed analysis framework supporting the general inter-procedural dataflow analysis. Inspired by large-scale graph processing, we devise dedicated distributed worklist algorithms for both whole-program analysis and incremental analysis. We implement these algorithms and develop a distributed framework called BigDataflow running on a large-scale cluster. The experimental results validate the promising performance of BigDataflow—BigDataflow can finish analyzing the program of million lines of code in minutes. Compared with the state-of-the-art, BigDataflow achieves much more analysis efficiency.


venue: vmcai

title: A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines

authors:
Gilles Barthe
Guillaume Dufay
Line Jakubiec
Simão Melo de Sousa


title: Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness

authors:
Kai Baukus
Yassine Lakhnech
Karsten Stahl


title: Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode

authors:
Cinzia Bernardeschi
Nicoletta De Francesco


title: Compositional Termination Analysis of Symbolic Forward Analysis

authors:
Witold Charatonik
Supratik Mukhopadhyay
Andreas Podelski


title: Improving the Encoding of LTL Model Checking into SAT

authors:
Alessandro Cimatti
Marco Pistore
Marco Roveri
Roberto Sebastiani


title: A Fully Abstract Model for Higher-Order Mobile Ambients

authors:
Mario Coppo
Mariangiola Dezani-Ciancaglini


title: Automata-Theoretic Decision of Timed Games

authors:
Marco Faella
Salvatore La Torre
Aniello Murano


title: Proofs Methods for Bisimulation Based Information Flow Security

authors:
Riccardo Focardi
Carla Piazza
Sabina Rossi


title: Combining Norms to Prove Termination

authors:
Samir Genaim
Michael Codish
John P. Gallagher
Vitaly Lagoon


title: An Experiment in Type Inference and Verification by Abstract Interpretation

authors:
Roberta Gori
Giorgio Levi


title: Approximating ATL* in ATL

authors:
Aidan Harding
Mark Ryan
Pierre-Yves Schobbens


title: A Refinement of the Escape Property

authors:
Patricia M. Hill
Fausto Spoto


title: Model Checking Modal Transition Systems Using Kripke Structures


title: Verifying BDD Algorithms through Monadic Interpretation

authors:
Sava Krstic
John Matthews


title: Static Monotonicity Analysis for lambda-definable Functions over Lattices

authors:
Andrzej S. Murawski
Kwangkeun Yi


title: Analyzing Cryptographic Protocols in a Reactive Framework


title: Synchronous Closing of Timed SDL Systems for Model Checking

authors:
Natalia Sidorova
Martin Steffen


title: An Abstract Schema for Equivalence-Checking Games


title: A Simulation Preorder for Abstraction of Reactive Systems

authors:
Ferucio Laurentiu Tiplea
Aurora Tiplea


title: Weak Muller Acceptance Conditions for Tree Automata

authors:
Salvatore La Torre
Aniello Murano
Margherita Napoli


title: Storage Size Reduction by In-place Mapping of Arrays

authors:
Remko Tronçon
Maurice Bruynooghe
Gerda Janssens
Francky Catthoor


title: Automatic Verification of Probabilistic Free Choice

authors:
Lenore D. Zuck
Amir Pnueli
Yonit Kesten


title: Bisimulation and Unwinding for Verifying Possibilistic Security Properties

authors:
Annalisa Bossi
Riccardo Focardi
Carla Piazza
Sabina Rossi


title: Complexity of Nesting Analysis in Mobile Ambients

authors:
Chiara Braghin
Agostino Cortesi
Riccardo Focardi
Flaminia L. Luccio
Carla Piazza


title: CHASE: A Static Checker for JML's Assignable Clause

authors:
Néstor Cataño
Marieke Huisman


title: Automatic Verification by Abstract Interpretation


title: Shape Analysis through Predicate Abstraction and Model Checking

authors:
Dennis Dams
Kedar S. Namjoshi


title: Domain Compression for Complete Abstractions

authors:
Roberto Giacobazzi
Isabella Mastroeni


title: On the Expressiveness of 3-Valued Models

authors:
Patrice Godefroid
Radha Jagadeesan


title: Properties of a Type Abstract Interpreter


title: Efficient Computation of Recurrence Diameters

authors:
Daniel Kroening
Ofer Strichman


title: Types for Evolving Communication in Safe Ambients


title: Action Refinement from a Logical Point of View

authors:
Mila E. Majster-Cederbaum
Naijun Zhan
Harald Fecher


title: Property Checking Driven Abstract Interpretation-Based Static Analysis


title: Reasoning about Layered Message Passing Systems

authors:
B. Meenakshi
Ramaswamy Ramanujam


title: Abstraction of Expectation Functions Using Gaussian Distributions


title: Lifting Temporal Proofs through Abstractions


title: Formal Verification of the Horn-Preneel Micropayment Protocol

authors:
Kazuhiro Ogata
Kokichi Futatsugi


title: Model-Checking and Abstraction to the Aid of Parameterized Systems

authors:
Amir Pnueli
Lenore D. Zuck


title: Software Model Checking with Abstraction Refinement


title: Abstract Interpretation-Based Certification of Assembly Code


title: Symmetry Reductions in Model-Checking


title: Behavior-Based Model Construction

authors:
Bernhard Steffen
Hardi Hungar


title: Optimized Live Heap Bound Analysis

authors:
Leena Unnikrishnan
Scott D. Stoller
Yanhong A. Liu


title: Efficient Verification of Timed Automata with BDD-Like Data-Structures


title: Using Simulated Execution in Verifying Distributed Algorithms

authors:
Toh Ne Win
Michael D. Ernst
Stephen J. Garland
Dilsun Kirli Kaynar
Nancy A. Lynch


title: A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution

authors:
Ping Yang
C. R. Ramakrishnan
Scott A. Smolka


title: Type Inference for Parameterized Race-Free Java

authors:
Rahul Agarwal
Scott D. Stoller


title: Applying Jlint to Space Exploration Software

authors:
Cyrille Artho
Klaus Havelund


title: Widening Operators for Powerset Domains

authors:
Roberto Bagnara
Patricia M. Hill
Enea Zaffanella


title: Rule-Based Runtime Verification

authors:
Howard Barringer
Allen Goldberg
Klaus Havelund
Koushik Sen


title: Security Types Preserving Compilation: (Extended Abstract)

authors:
Gilles Barthe
Amitabh Basu
Tamara Rezk


title: Completeness and Complexity of Bounded Model Checking

authors:
Edmund M. Clarke
Daniel Kroening
Joël Ouaknine
Ofer Strichman


title: Static Analysis versus Software Model Checking for Bug Finding

authors:
Dawson R. Engler
Madanlal Musuvathi


title: Analysis of Recursive Game Graphs Using Data Flow Equations


title: Liveness with Invisible Ranking

authors:
Yi Fang
Nir Piterman
Amir Pnueli
Lenore D. Zuck


title: Security, Protocols, and Trust


title: A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal


title: Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking

authors:
John Hatcliff
Robby
Matthew B. Dwyer


title: Approximate Probabilistic Model Checking

authors:
Thomas Hérault
Richard Lassaigne
Frédéric Magniette
Sylvain Peyronnet


title: Boolean Algebra of Shape Analysis Constraints

authors:
Viktor Kuncak
Martin C. Rinard

abstract: The parametric shape analysis framework of Sagiv, Reps, and Wilhelm [45,46] uses three-valued structures as dataflow lattice elements to represent sets of states at different program points. The recent work of Yorsh, Reps, Sagiv, Wilhelm [48,50] introduces a family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures [46] and represent the same sets of concrete states.


title: Constructing Quantified Invariants via Predicate Abstraction

authors:
Shuvendu K. Lahiri
Randal E. Bryant


title: Automatic Inference of Class Invariants


title: Model Checking for Object Specifications in Hidden Algebra

authors:
Dorel Lucanu
Gabriel Ciobanu


title: Model Checking Polygonal Differential Inclusions Using Invariance Kernels

authors:
Gordon J. Pace
Gerardo Schneider


title: A Complete Method for the Synthesis of Linear Ranking Functions

authors:
Andreas Podelski
Andrey Rybalchenko


title: Symbolic Implementation of the Best Transformer

authors:
Thomas W. Reps
Shmuel Sagiv
Greta Yorsh


title: On the Expressive Power of Canonical Abstraction


title: Construction of a Semantic Model for a Typed Assembly Language

authors:
Gang Tan
Andrew W. Appel
Kedar N. Swadi
Dinghao Wu


title: History-Dependent Scheduling for Cryptographic Processes


title: Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone


title: Certifying Temporal Properties for Compiled C Programs

authors:
Songtao Xia
James Hook


title: Checking Interval Based Properties for Reactive Systems

authors:
Yu Pei
Qiwen Xu


title: Optimizing Bounded Model Checking for Linear Hybrid Systems

authors:
Erika Ábrahám
Bernd Becker
Felix Klaedtke
Martin Steffen


title: Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs

authors:
Paul C. Attie
Hana Chockler


title: Shape Analysis by Predicate Abstraction

authors:
Ittai Balaban
Amir Pnueli
Lenore D. Zuck


title: Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs


title: Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties


title: Termination of Polynomial Programs

authors:
Aaron R. Bradley
Zohar Manna
Henny B. Sipma


title: Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement

authors:
Sebastian Burckhardt
Rajeev Alur
Milo M. K. Martin


title: Abstract Interpretation with Alien Expressions and Heap Structures

authors:
Bor-Yuh Evan Chang
K. Rustan M. Leino


title: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming


title: Automata as Abstractions

authors:
Dennis Dams
Kedar S. Namjoshi


title: The Arithmetic-Geometric Progression Abstract Domain

abstract: We present a new numerical abstract domain. This domain automatically detects and proves bounds on the values of program variables. For that purpose, it relates variable values to a clock counter. More precisely, it bounds these values with the i-th iterate of the function [X↦α×X+β] applied on M, where i denotes the clock counter and the floating-point numbers α, β, and M are discovered by the analysis. Such properties are especially useful to analyze loops in which a variable is iteratively assigned with a barycentric mean of the values that were associated with the same variable at some previous iterations. Because of rounding errors, the computation of this barycenter may diverge when the loop is iterated forever. Our domain provides a bound that depends on the execution time of the program.


title: Information Flow Analysis for Java Bytecode

authors:
Samir Genaim
Fausto Spoto


title: Cryptographic Protocol Analysis on Real C Code

authors:
Jean Goubault-Larrecq
Fabrice Parrennes


title: Don't Know in the µ-Calculus

authors:
Orna Grumberg
Martin Lange
Martin Leucker
Sharon Shoham


title: The Verifying Compiler, a Grand Challenge for Computing Research


title: Verification of an Error Correcting Code by Abstract Interpretation


title: I/O Efficient Directed Model Checking

authors:
Shahid Jabbar
Stefan Edelkamp


title: On the Complexity of Error Explanation

authors:
Nirman Kumar
Viraj Kumar
Mahesh Viswanathan


title: Generalized Typestate Checking for Data Structure Consistency

authors:
Patrick Lam
Viktor Kuncak
Martin C. Rinard


title: Weak Automata for the Linear Time µ-Calculus


title: Simple Is Better: Efficient Bounded Model Checking for Past LTL

authors:
Timo Latvala
Armin Biere
Keijo Heljanko
Tommi A. Junttila


title: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists

authors:
Roman Manevich
Eran Yahav
Ganesan Ramalingam
Shmuel Sagiv


title: An Overview of Semantics for the Validation of Numerical Programs


title: Checking Herbrand Equalities and Beyond

authors:
Markus Müller-Olm
Oliver Rüthing
Helmut Seidl


title: Abstraction for Liveness


title: Purity and Side Effect Analysis for Java Programs

authors:
Alexandru Salcianu
Martin C. Rinard


title: Scalable Analysis of Linear Systems Using Mathematical Programming

authors:
Sriram Sankaranarayanan
Henny B. Sipma
Zohar Manna


title: Minimizing Counterexample with Unit Core Extraction and Incremental SAT

authors:
ShengYu Shen
Ying Qin
Sikun Li

abstract: It is a hotly researching topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. K Ravi proposes a two-stages counterexample minimization algorithm. This algorithm is the most effective one among all existing approaches, but time overhead of its second stage(called BFL) is very large due to one call to SAT solver per candidate variable to be eliminated. So we propose a faster counterexample minimization algorithm based on unit core extraction and incremental SAT. First, for every unsatisfiable instance of BFL, we perform unit core extraction algorithm to extract the set of variables that are sufficient to lead to conflict, all variables not belong to this set can be eliminated simultaneously. In this way, we can eliminate many variables with only one call to SAT solver. At the same time, we employ incremental SAT approach to share learned clauses between similar instances of BFL, to prevent overlapped state space from being searched repeatedly. Theoretic analysis and experiment result show that, our approach is 1 order of magnitude faster than K Ravi's algorithm, and still retains its ability to eliminate irrelevant variables.


title: Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives


title: Model Checking of Systems Employing Commutative Functions

authors:
A. Prasad Sistla
Min Zhou
Xiaodong Wang


title: Combining Shape Analyses by Intersecting Abstractions

authors:
Gilad Arnold
Roman Manevich
Mooly Sagiv
Ran Shaham


title: Ranking Abstraction of Recursive Programs

authors:
Ittai Balaban
Ariel Cohen
Amir Pnueli


title: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs

authors:
Jesse D. Bingham
Zvonimir Rakamaric


title: Complexity Results on Branching-Time Pushdown Model Checking


title: Verification of Well-Formed Communicating Recursive State Machines

authors:
Laura Bozzelli
Salvatore La Torre
Adriano Peron


title: What's Decidable About Arrays?

authors:
Aaron R. Bradley
Zohar Manna
Henny B. Sipma


title: A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety

authors:
Bor-Yuh Evan Chang
Adam Chlipala
George C. Necula


title: Environment Abstraction for Parameterized Verification

authors:
Edmund M. Clarke
Muralidhar Talupur
Helmut Veith


title: A Complete Abstract Interpretation Framework for Coverability Properties of WSTS

authors:
Pierre Ganty
Jean-François Raskin
Laurent Van Begin


title: Piecewise FIFO Channels Are Analyzable

authors:
Naghmeh Ghafari
Richard J. Trefler


title: Systematic Construction of Abstractions for Model-Checking

authors:
Arie Gurfinkel
Ou Wei
Marsha Chechik


title: Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems

authors:
Katia Hristova
Yanhong A. Liu


title: Parallel External Directed Model Checking with Linear I/O

authors:
Shahid Jabbar
Stefan Edelkamp


title: A CLP Method for Compositional and Intermittent Predicate Abstraction

authors:
Joxan Jaffar
Andrew E. Santosa
Razvan Voicu


title: Relative Safety


title: Resource Usage Analysis for the pi-Calculus

authors:
Naoki Kobayashi
Kohei Suenaga
Lucian Wischik


title: Semantic Hierarchy Refactoring by Abstract Interpretation

authors:
Francesco Logozzo
Agostino Cortesi


title: Symbolic Methods to Enhance the Precision of Numerical Abstract Domains

abstract:
We present lightweight and generic symbolic methods to improve the precision of numerical static analyses based on Abstract Interpretation. The main idea is to simplify numerical expressions before they are fed to abstract transfer functions. An important novelty is that these simplifications are performed on-the-fly, using information gathered dynamically by the analyzer.

A first method, called “linearization,” allows abstracting arbitrary expressions into affine forms with interval coefficients while simplifying them. A second method, called “symbolic constant propagation,” enhances the simplification feature of the linearization by propagating assigned expressions in a symbolic way. Combined together, these methods increase the relationality level of numerical abstract domains and make them more robust against program transformations. We show how they can be integrated within the classical interval, octagon and polyhedron domains. These methods have been incorporated within the Astree static analyzer that checks for the absence of run-time errors in embedded critical avionics software. We present an experimental proof of their usefulness.


title: Synthesis of Reactive(1) Designs

authors:
Nir Piterman
Amir Pnueli
Yaniv Sa'ar


title: Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation

authors:
Francesco Ranzato
Francesco Tapparo


title: Detecting Non-cyclicity by Abstract Compilation into Boolean Functions

authors:
Stefano Rossignoli
Fausto Spoto


title: Efficient Strongly Relational Polyhedral Analysis

authors:
Sriram Sankaranarayanan
Michael Colón
Henny B. Sipma
Zohar Manna


title: Closure Operators for ROBDDs

authors:
Peter Schachte
Harald Søndergaard


title: Monitoring Off-the-Shelf Components

authors:
A. Prasad Sistla
Min Zhou
Lenore D. Zuck


title: Totally Clairvoyant Scheduling with Relative Timing Constraints


title: A Compositional Logic for Control Flow

authors:
Gang Tan
Andrew W. Appel


title: Field Constraint Analysis

authors:
Thomas Wies
Viktor Kuncak
Patrick Lam
Andreas Podelski
Martin C. Rinard

abstract: Note: MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010 Full version of http://infoscience.epfl.ch/search.py?recid=110250l=en Reference LARA-REPORT-2005-003 Record created on 2007-08-21, modified on 2017-05-12


title: Error Control for Probabilistic Model Checking


title: Shape Analysis of Single-Parent Heaps

authors:
Ittai Balaban
Amir Pnueli
Lenore D. Zuck


title: DIVINE: DIscovering Variables IN Executables

authors:
Gogul Balakrishnan
Thomas W. Reps


title: Better Under-Approximation of Programs by Hiding Variables

authors:
Thomas Ball
Orna Kupferman


title: Invariant Synthesis for Combined Theories

authors:
Dirk Beyer
Thomas A. Henzinger
Rupak Majumdar
Andrey Rybalchenko


title: Using First-Order Theorem Provers in the Jahob Data Structure Verification System

authors:
Charles Bouillaguet
Viktor Kuncak
Thomas Wies
Karen Zee
Martin C. Rinard

abstract:
This paper presents our integration of efficient resolution-based theorem provers into the Jahob data structure verification system. Our experimental results show that this approach enables Jahob to automatically verify the correctness of a range of complex dynamically instantiable data structures, such as hash tables and search trees, without the need for interactive theorem proving or techniques tailored to individual data structures.

Our primary technical results include: (1) a translation from higher-order logic to first-order logic that enables the application of resolution-based theorem provers and (2) a proof that eliminating type (sort) information in formulas is both sound and complete, even in the presence of a generic equality operator. Our experimental results show that the elimination of type information often dramatically decreases the time required to prove the resulting formulas.

These techniques enabled us to verify complex correctness properties of Java programs such as a mutable set implemented as an imperative linked list, a finite map implemented as a functional ordered tree, a hash table with a mutable array, and a simple library system example that uses these container data structures. Our system verifies (in a matter of minutes) that data structure operations correctly update the finite map, that they preserve data structure invariants (such as ordering of elements, membership in appropriate hash table buckets, or relationships between sets and relations), and that there are no run-time errors such as null dereferences or array out of bounds accesses.


title: On Flat Programs with Lists

authors:
Marius Bozga
Radu Iosif


title: Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning

authors:
Sigmund Cherem
Radu Rugina


title: Verifying Compensating Transactions

authors:
Michael Emmi
Rupak Majumdar


title: More Precise Partition Abstractions

authors:
Harald Fecher
Michael Huth


title: Assertion Checking Unified

authors:
Sumit Gulwani
Ashish Tiwari


title: Language-Based Abstraction Refinement for Hybrid System Verification

authors:
Felix Klaedtke
Stefan Ratschan
Zhikun She


title: Lattice Automata

authors:
Orna Kupferman
Yoad Lustig


title: Constructing Specialized Shape Analyses for Uniform Change

authors:
Tal Lev-Ami
Mooly Sagiv
Neil Immerman
Thomas W. Reps


title: Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes


title: Learning Algorithms and Formal Verification (Invited Tutorial)


title: Interpolants and Symbolic Model Checking


title: Model Checking Via GammaCFA

authors:
Matthew Might
Benjamin Chambers
Olin Shivers


title: Symmetry and Completeness in the Analysis of Parameterized Systems


title: Automated Verification of Shape and Size Properties Via Separation Logic

authors:
Huu Hai Nguyen
Cristina David
Shengchao Qin
Wei-Ngan Chin

abstract: Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system.


title: An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints

authors:
Mathias Péron
Nicolas Halbwachs


title: An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

authors:
Zvonimir Rakamaric
Jesse D. Bingham
Alan J. Hu


title: The Constraint Database Approach to Software Verification


title: Constraint Solving for Interpolation

authors:
Andrey Rybalchenko
Viorica Sofronie-Stokkermans


title: Model Checking Nonblocking MPI Programs


title: Automata-Theoretic Model Checking Revisited


title: The Spotlight Principle

authors:
Björn Wachter
Bernd Westphal


title: Towards Shape Analysis for Device Drivers


title: Handling Parameterized Systems with Non-atomic Global Conditions

authors:
Parosh Aziz Abdulla
Noomene Ben Henda
Giorgio Delzanno
Ahmed Rezine


title: An Improved Tight Closure Algorithm for Integer Octagonal Constraints

authors:
Roberto Bagnara
Patricia M. Hill
Enea Zaffanella

abstract: Integer octagonal constraints (a.k.a. Unit Two Variables Per Inequality or UTVPI integer constraints) constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and formal analysis and verification of software and hardware systems, since they couple algorithms having polynomial complexity with a relatively good expressive power. The main algorithms required for the manipulation of such constraints are the satisfiability check and the computation of the inferential closure of a set of constraints. The latter is called tight closure to mark the difference with the (incomplete) closure algorithm that does not exploit the integrality of the variables. In this paper we present and fully justify an O(n3) algorithm to compute the tight closure of a set of UTVPI integer constraints.


title: Abstract Interpretation of the Physical Inputs of Embedded Programs

authors:
Olivier Bouissou
Matthieu Martel


title: Diagnostic Information for Realizability

authors:
Alessandro Cimatti
Marco Roveri
Viktor Schuppan
Andrei Tchaltsev


title: Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions


title: Approximation Refinement for Interpolation-Based Model Checking

authors:
Vijay Victor D'Silva
Mitra Purandare
Daniel Kroening


title: Abstract Interpretation of Cellular Signalling Networks

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


title: Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?

authors:
Rayna Dimitrova
Andreas Podelski


title: Model Checking for Action Abstraction

authors:
Harald Fecher
Michael Huth


title: On Bridging Simulation and Formal Verification


title: Extending Model Checking with Dynamic Analysis

authors:
Alex Groce
Rajeev Joshi


title: CTL as an Intermediate Language

authors:
Neil D. Jones
René Rydhof Hansen


title: Multi-valued Logics, Automata, Simulations, and Games

authors:
Orna Kupferman
Yoad Lustig


title: Deriving Bisimulations by Simplifying Partitions


title: Precise Set Sharing Analysis for Java-Style Programs

authors:
Mario Méndez-Lojo
Manuel V. Hermenegildo

abstract: Finding useful sharing information between instances in object- oriented programs has recently been the focus of much research. The applications of such static analysis are multiple: by knowing which variables definitely do not share in memory we can apply conventional compiler optimizations, find coarse-grained parallelism opportunities, or, more importantly, verify certain correctness aspects of programs even in the absence of annotations. In this paper we introduce a framework for deriving precise sharing information based on abstract interpretation for a Java-like language. Our analysis achieves precision in various ways, including supporting multivariance, which allows separating different contexts. We propose a combined Set Sharing + Nullity + Classes domain which captures which instances do not share and which ones are definitively null, and which uses the classes to refine the static information when inheritance is present. The use of a set sharing abstraction allows a more precise representation of the existing sharings and is crucial in achieving precision during interprocedural analysis. Carrying the domains in a combined way facilitates the interaction among them in the presence of multivariance in the analysis. We show through examples and experimentally that both the set sharing part of the domain as well as the combined domain provide more accurate information than previous work based on pair sharing domains, at reasonable cost.


title: From LTL to Symbolically Represented Deterministic Automata

authors:
Andreas Morgenstern
Klaus Schneider


title: Sufficient Preconditions for Modular Assertion Checking


title: Runtime Checking for Separation Logic

authors:
Huu Hai Nguyen
Viktor Kuncak
Wei-Ngan Chin


title: Verification of Register Allocators


title: Decision Procedures for Multisets with Cardinality Constraints

authors:
Ruzica Piskac
Viktor Kuncak


title: Program Analysis and Programming Languages for Security


title: All You Need Is Compassion

authors:
Amir Pnueli
Yaniv Sa'ar


title: A Forward-Backward Abstraction Refinement Algorithm

authors:
Francesco Ranzato
Olivia Rossi-Doria
Francesco Tapparo


title: Internal and External Logics of Abstract Interpretations


title: Monitoring Temporal Properties of Stochastic Systems

authors:
A. Prasad Sistla
Abhigna R. Srinivas


title: A Hybrid Algorithm for LTL Games

authors:
Saqib Sohail
Fabio Somenzi
Kavita Ravi


title: Towards Automatic Stability Analysis for Rely-Guarantee Proofs

authors:
Hasan Amjad
Richard Bornat


title: Mostly-Functional Behavior in Java Programs

authors:
William C. Benton
Charles N. Fischer


title: Advances in Program Termination and Liveness


title: Verification of Security Protocols


title: The Higher-Order Aggregate Update Problem

authors:
Christos Dimoulas
Mitchell Wand


title: Model Checking: Progress and Problems


title: An Abort-Aware Model of Transactional Programming

authors:
Kousha Etessami
Patrice Godefroid


title: Model-Checking the Linux Virtual File System

authors:
Andy Galloway
Gerald Lüttgen
Jan Tobias Mühlberg
Radu Siminiceanu


title: LTL Generalized Model Checking Revisited

authors:
Patrice Godefroid
Nir Piterman


title: Monitoring the Full Range of omega-Regular Properties of Stochastic Systems

authors:
Kalpana Gondi
Yogeshkumar Patel
A. Prasad Sistla


title: Constraint-Based Invariant Inference over Predicate Abstraction

authors:
Sumit Gulwani
Saurabh Srivastava
Ramarathnam Venkatesan


title: Model Checking Concurrent Programs

abstract: With the growth of multi-core processing and concurrent programming in modern computing systems, there is a great need to develop effective verification techniques for concurrent programs. Static analysis techniques have been shown effective for finding data races, but suffer from a general problem of too many false alarms. Dynamic techniques like testing have also shown promise, but provide limited coverage over the state space including all possible thread interleavings. Model checking alone cannot scale. However, it works better in combination with these techniques, with the potential of finding real error traces on one hand and better coverage on the other. In this talk, I will describe our recent advances in concurrent dataflow analysis, symbolic model checking with partial order reduction, and dynamic techniques for verifying concurrent programs. These techniques have been implemented in a unified verification platform, currently targeted at multi-threaded C programs. I will also report on our experiences on some challenging examples from the public domain and the industry.


title: Reducing Behavioural to Structural Properties of Programs with Procedures

authors:
Dilian Gurov
Marieke Huisman


title: Query-Driven Program Testing

authors:
Andreas Holzer
Christian Schallhart
Michael Tautschnig
Helmut Veith


title: Average-Price-per-Reward Games on Hybrid Automata with Strong Resets

authors:
Marcin Jurdzinski
Ranko Lazic
Michal Rutkowski


title: Abstraction Refinement for Probabilistic Software

authors:
Mark Kattenbelt
Marta Z. Kwiatkowska
Gethin Norman
David Parker


title: Finding Concurrency-Related Bugs Using Random Isolation

authors:
Nicholas Kidd
Thomas W. Reps
Julian Dolby
Mandana Vaziri


title: An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries

authors:
Johannes Kinder
Florian Zuleger
Helmut Veith


title: SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities

authors:
Vincent Laviron
Francesco Logozzo


title: Deciding Extensions of the Theories of Vectors and Bags


title: A PosterioriSoundness for Non-deterministic Abstract Interpretations

authors:
Matthew Might
Panagiotis Manolios


title: An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking


title: A Scalable Memory Model for Low-Level Code

authors:
Zvonimir Rakamaric
Alan J. Hu


title: Thread-Modular Shape Analysis


title: Synthesizing Switching Logic Using Constraint Solving

authors:
Ankur Taly
Sumit Gulwani
Ashish Tiwari


title: Extending Symmetry Reduction by Exploiting System Architecture

authors:
Richard J. Trefler
Thomas Wahl


title: Shape-Value Abstraction for Verifying Linearizability


title: Mixed Transition Systems Revisited

authors:
Ou Wei
Arie Gurfinkel
Marsha Chechik


title: Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking

authors:
Ralf Wimmer
Bettina Braitling
Bernd Becker


title: Temporal Reasoning for Procedural Programs

authors:
Rajeev Alur
Swarat Chaudhuri


title: Improved Model Checking of Hierarchical Systems

authors:
Benjamin Aminof
Orna Kupferman
Aniello Murano


title: Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming

authors:
Lei Bu
Jianhua Zhao
Xuandong Li


title: Complexity Bounds for the Verification of Real-Time Software

authors:
Rohit Chadha
Axel Legay
Pavithra Prabhakar
Mahesh Viswanathan


title: An Abstract Domain to Discover Interval Linear Equalities

authors:
Liqian Chen
Antoine Miné
Ji Wang
Patrick Cousot


title: Interpolant Strength

authors:
Vijay Victor D'Silva
Daniel Kroening
Mitra Purandare
Georg Weissenbacher


title: Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing


title: Analysis of Systems with Stochastic Process Creation


title: Abstract Interpretation-Based Protection


title: Invariant and Type Inference for Matrices

authors:
Thomas A. Henzinger
Thibaud Hottelier
Laura Kovács
Andrei Voronkov


title: Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction

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


title: Advances in Probabilistic Model Checking


title: Automatic Abstraction for Congruences

authors:
Andy King
Harald Søndergaard


title: Shape Analysis of Low-Level C with Overlapping Structures

authors:
Jörg Kreiker
Helmut Seidl
Vesal Vojdani


title: Building a Calculus of Data Structures

authors:
Viktor Kuncak
Ruzica Piskac
Philippe Suter
Thomas Wies


title: Abstract Threads

authors:
Shuvendu K. Lahiri
Alexander Malkis
Shaz Qadeer


title: Verifying Concurrent Programs with Chalice


title: Shape Analysis with Reference Set Relations

authors:
Mark Marron
Rupak Majumdar
Darko Stefanovic
Deepak Kapur


title: Shape Analysis in the Absence of Pointers and Structure


title: An Analysis of Permutations in Arrays

authors:
Valentin Perrelle
Nicolas Halbwachs


title: Regular Linear Temporal Logic with Past

authors:
César Sánchez
Martin Leucker


title: Model-Checking In-Lined Reference Monitors

authors:
Meera Sridhar
Kevin W. Hamlen


title: Considerate Reasoning and the Composite Design Pattern

authors:
Alexander J. Summers
Sophia Drossopoulou


title: RGSep Action Inference


title: Best Probabilistic Transformers

authors:
Björn Wachter
Lijun Zhang


title: Static Timing Analysis for Hard Real-Time Systems

authors:
Reinhard Wilhelm
Sebastian Altmeyer
Claire Burguière
Daniel Grund
Jörg Herter
Jan Reineke
Björn Wachter
Stephan Wilhelm


title: Collections, Cardinalities, and Relations

authors:
Kuat Yessenov
Ruzica Piskac
Viktor Kuncak

abstract: Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to compute direct and inverse relation and function images. We establish decidability and complexity bounds for the extended logics.


title: More Precise Yet Widely Applicable Cost Analysis

authors:
Elvira Albert
Samir Genaim
Abu Naser Masud


title: Refinement-Based CFG Reconstruction from Unstructured Programs

authors:
Sébastien Bardin
Philippe Herrmann
Franck Védrine


title: SAT-Based Model Checking without Unrolling


title: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic

authors:
Angelo Brillout
Daniel Kroening
Philipp Rümmer
Thomas Wahl

abstract: Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifier-free. We go on to identify fragments of QPA+UP and QPA+UF with restricted forms of guarded quantification that are closed under interpolation. Formulae in these fragments can easily be mapped to quantifier-free expressions with integer division. For QPA+AR, we formulate a sound interpolation procedure that potentially produces interpolants with unrestricted quantifiers.


title: Probabilistic Büchi Automata with Non-extremal Acceptance Thresholds

authors:
Rohit Chadha
A. Prasad Sistla
Mahesh Viswanathan


title: Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice

authors:
Chih-Hong Cheng
Harald Rueß
Alois C. Knoll
Christian Buckl


title: Proving Stabilization of Biological Systems

authors:
Byron Cook
Jasmin Fisher
Elzbieta Krepska
Nir Piterman


title: Precondition Inference from Intermittent Assertions and Application to Contracts on Collections

authors:
Patrick Cousot
Radhia Cousot
Francesco Logozzo


title: Abstract Probabilistic Automata

authors:
Benoît Delahaye
Joost-Pieter Katoen
Kim G. Larsen
Axel Legay
Mikkel L. Pedersen
Falak Sher
Andrzej Wasowski


title: Are Cells Asynchronous Circuits? - (Invited Talk)


title: Strengthening Induction-Based Race Checking with Lightweight Static Analysis

authors:
Alastair F. Donaldson
Leopold Haller
Daniel Kroening


title: Access Nets: Modeling Access to Physical Spaces

authors:
Robert Frohardt
Bor-Yuh Evan Chang
Sriram Sankaranarayanan


title: Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation

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


title: Verifying Deadlock-Freedom of Communication Fabrics

authors:
Alexander Gotmanov
Satrajit Chatterjee
Michael Kishinevsky


title: Static Analysis of Finite Precision Computations

authors:
Eric Goubault
Sylvie Putot


title: An Evaluation of Automata Algorithms for String Analysis

authors:
Pieter Hooimeijer
Margus Veanes


title: Automata Learning with Automated Alphabet Abstraction Refinement

authors:
Falk Howar
Bernhard Steffen
Maik Merten


title: Towards Complete Reasoning about Axiomatic Specifications

authors:
Swen Jacobs
Viktor Kuncak

abstract: To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision procedures for reasoning about such universally quantified properties of functional programs, using local theory extensionmethodology. We establish new classes of universally quantified formulas whose satisfiability can be checked in a complete way by finite quantifier instantiation. These classes include single-invocation axioms that generalize standard function contracts, but also certain many-invocation axioms, specifying that functions satisfy congruence, injectivity, or monotonicity with respect to abstraction functions, as well as conjunctions of some of these properties. These many-invocation axioms can specify correctness of abstract data type implementations as well as certain information-flow properties. We also present a decidability-preserving construction that enables the same function to be specified using different classes of decidable specifications on different partitions of its domain.


title: String Analysis as an Abstract Interpretation

authors:
Se-Won Kim
Kwang-Moo Choe


title: ExplainHoudini: Making Houdini Inference Transparent

authors:
Shuvendu K. Lahiri
Julien Vanegue


title: Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation - (Invited Talk)


title: Distributed and Predictable Software Model Checking

authors:
Nuno P. Lopes
Andrey Rybalchenko


title: Access Analysis-Based Tight Localization of Abstract Memories

authors:
Hakjoo Oh
Lucas Brutschy
Kwangkeun Yi


title: Decision Procedures for Automating Termination Proofs

authors:
Ruzica Piskac
Thomas Wies

abstract: Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.


title: Formal Analysis of Message Passing - (Invited Talk)

authors:
Stephen F. Siegel
Ganesh Gopalakrishnan


title: Collective Assertions

authors:
Stephen F. Siegel
Timothy K. Zirkel


title: Quality Engineering: Leveraging Heterogeneous Information - (Invited Talk)

authors:
Bernhard Steffen
Oliver Rüthing


title: Sets with Cardinality Constraints in Satisfiability Modulo Theories

authors:
Philippe Suter
Robin Steiger
Viktor Kuncak

abstract: Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier-free BAPA (QFBAPA). In contrast to many other NP-complete problems (such as quantifier-free first-order logic or linear arithmetic), the applications of QFBAPA to a broader set of problems has so far been hindered by the lack of an efficient implementation that can be used alongside other efficient decision procedures. We overcome these limitations by extending the efficient SMT solver Z3 with the ability to reason about cardinality (QFBAPA) constraints. Our implementation uses the DPLL(T) mechanism of Z3 to reason about the top-level propositional structure of a QFBAPA formula, improving the efficiency compared to previous implementations. Moreover, we present a new algorithm for automatically decomposing QFBAPA formulas. Our algorithm alleviates the exponential explosion of considering all Venn regions, significantly improving the tractability of formulas with many set variables. Because it is implemented as a theory plugin, our implementation enables Z3 to prove formulas that use QFBAPA constructs with constructs from other theories that Z3 supports, as well as with quantifiers. We have applied our implementation to the verification of functional programs; we show it can automatically prove formulas that no automated approach was reported to be able to prove before.


title: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification

authors:
Aws Albarghouthi
Arie Gurfinkel
Marsha Chechik


title: Synchronizability for Verification of Asynchronously Communicating Systems

authors:
Samik Basu
Tevfik Bultan
Meriem Ouederni


title: On the Termination of Integer Loops

authors:
Amir M. Ben-Amram
Samir Genaim
Abu Naser Masud


title: Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data

authors:
Ahmed Bouajjani
Cezara Dragoi
Constantin Enea
Mihaela Sighireanu


title: Verification of Gap-Order Constraint Abstractions of Counter Systems

authors:
Laura Bozzelli
Sophie Pinchinat


title: On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking


title: Regression Verification for Multi-threaded Programs

authors:
Sagar Chaki
Arie Gurfinkel
Ofer Strichman


title: Crowfoot: A Verifier for Higher-Order Store Programs

authors:
Nathaniel Charlton
Ben Horsfall
Bernhard Reus

abstract: We present Crowfoot, an automatic verification tool for imperative programs that manipulate procedures dynamically at runtime; these programs use a heap that can store not only data but also code (commands or procedures). Such heaps are often called higher-order store , and allow for instance the creation of new recursions on the fly. One can use higher-order store to model phenomena such as runtime loading and unloading of code, runtime update of code and runtime code generation. Crowfoot's assertion language, based on separation logic, features nested Hoare triples which describe the behaviour of procedures stored on the heap. The tool addresses complex issues like deep frame rules and recursion through the store, and is the first verification tool based on recent developments in the mathematical foundations of Hoare logics with nested triples.


title: Synthesizing Protocols for Digital Contract Signing

authors:
Krishnendu Chatterjee
Vishwanath Raman


title: Model Checking Information Flow in Reactive Systems

authors:
Rayna Dimitrova
Bernd Finkbeiner
Máté Kovács
Markus N. Rabe
Helmut Seidl


title: Splitting via Interpolants

authors:
Evren Ermis
Jochen Hoenicke
Andreas Podelski


title: Synthesizing Efficient Controllers

authors:
Christian von Essen
Barbara Jobstmann


title: Automatic Inference of Access Permissions

authors:
Pietro Ferrara
Peter Müller


title: Lazy Synthesis

authors:
Bernd Finkbeiner
Swen Jacobs


title: Donut Domains: Efficient Non-convex Domains for Abstract Interpretation

authors:
Khalil Ghorbal
Franjo Ivancic
Gogul Balakrishnan
Naoto Maeda
Aarti Gupta


title: Inferring Canonical Register Automata

authors:
Falk Howar
Bernhard Steffen
Bengt Jonsson
Sofia Cassel


title: Software Verification with Liquid Types


title: Alternating Control Flow Reconstruction

authors:
Johannes Kinder
Dmitry Kravchenko


title: Effective Synthesis of Asynchronous Systems from GR(1) Specifications

authors:
Uri Klein
Nir Piterman
Amir Pnueli

abstract: We consider automatic synthesis from linear temporal logic specifications for asynchronous systems. We aim the produced reactive systems to be used as software in a multi-threaded environment. We extend previous reduction of asynchronous synthesis to synchronous synthesis to the setting of multiple input and multiple output variables. Much like synthesis for synchronous designs, this solution is not practical as it requires determinization of automata on infinite words and solution of complicated games. We follow advances in synthesis of synchronous designs, which restrict the handled specifications but achieve scalability and efficiency. We propose a heuristic that, in some cases, maintains scalability for asynchronous synthesis. Our heuristic can prove that specifications are realizable and extract designs. This is done by a reduction to synchronous synthesis that is inspired by the theoretical reduction.


title: Sound Non-statistical Clustering of Static Analysis Alarms

authors:
Woosuk Lee
Wonchan Lee
Kwangkeun Yi


title: Automating Induction with an SMT Solver


title: Modeling Asynchronous Message Passing for C Programs

authors:
Everett Morse
Nick Vrvilo
Eric Mercer
Jay McCarthy


title: Local Symmetry and Compositional Verification

authors:
Kedar S. Namjoshi
Richard J. Trefler


title: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs


title: versat: A Verified Modern SAT Solver

authors:
Duckki Oe
Aaron Stump
Corey Oliver
Kevin Clancy


title: Decision Procedures for Region Logic

authors:
Stan Rosenberg
Anindya Banerjee
David A. Naumann


title: A General Framework for Probabilistic Characterizing Formulae

authors:
Joshua Sack
Lijun Zhang


title: Loop Invariant Symbolic Execution for Parallel Programs

authors:
Stephen F. Siegel
Timothy K. Zirkel


title: Ideal Abstractions for Well-Structured Transition Systems

authors:
Damien Zufferey
Thomas Wies
Thomas A. Henzinger


title: All for the Price of Few

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


title: Quantifying Information Leakage of Randomized Protocols

authors:
Fabrizio Biondi
Axel Legay
Pasquale Malacaria
Andrzej Wasowski


title: An Abstract Interpretation of DPLL(T)

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


title: Compositional Sequentialization of Periodic Programs

authors:
Sagar Chaki
Arie Gurfinkel
Soonho Kong
Ofer Strichman


title: Flow-Sensitive Fault Localization

authors:
Jürgen Christ
Evren Ermis
Martin Schäf
Thomas Wies


title: Automatic Inference of Necessary Preconditions

authors:
Patrick Cousot
Radhia Cousot
Manuel Fähndrich
Francesco Logozzo


title: Tool Integration with the Evidential Tool Bus

authors:
Simon Cruanes
Grégoire Hamon
Sam Owre
Natarajan Shankar


title: Static Analysis of String Encoders and Decoders

authors:
Loris D'Antoni
Margus Veanes


title: Abstraction of Syntax

authors:
Vijay Victor D'Silva
Daniel Kroening


title: SMT-Based Bisimulation Minimisation of Markov Models

authors:
Christian Dehnert
Joost-Pieter Katoen
David Parker


title: Abstract Read Permissions: Fractional Permissions without the Fractions

authors:
Stefan Heule
K. Rustan M. Leino
Peter Müller
Alexander J. Summers


title: Reductions for Synthesis Procedures

authors:
Swen Jacobs
Viktor Kuncak
Philippe Suter


title: Knockout Prediction for Reaction Networks with Partial Kinetic Information

authors:
Mathias John
Mirabelle Nebut
Joachim Niehren


title: Towards Efficient Parameterized Synthesis

authors:
Ayrat Khalimov
Swen Jacobs
Roderick Bloem


title: SMT-Based Array Invariant Generation

authors:
Daniel Larraz
Enric Rodríguez-Carbonell
Albert Rubio


title: Causality Checking for Complex System Models

authors:
Florian Leitner-Fischer
Stefan Leue


title: A Model-Constructing Satisfiability Calculus

authors:
Leonardo Mendonça de Moura
Dejan Jovanovic


title: Uncovering Symmetries in Irregular Process Networks

authors:
Kedar S. Namjoshi
Richard J. Trefler


title: Sound and Complete Flow Typing with Unions, Intersections and Negations


title: A Constraint Solver Based on Abstract Domains

authors:
Marie Pelleau
Antoine Miné
Charlotte Truchet
Frédéric Benhamou


title: Automata as Proofs


title: Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems

authors:
Pavithra Prabhakar
Parasara Sridhar Duggirala
Sayan Mitra
Mahesh Viswanathan


title: Complete Abstractions Everywhere


title: Robustness Analysis of Networked Systems

authors:
Roopsha Samanta
Jyotirmoy V. Deshmukh
Swarat Chaudhuri


title: Logico-Numerical Max-Strategy Iteration

authors:
Peter Schrammel
Pavle Subotic


title: Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools

authors:
Yassamine Seladji
Olivier Bouissou


title: ClabureDB: Classified Bug-Reports Database

authors:
Jiri Slaby
Jan Strejcek
Marek Trtík


title: Reduced Product Combination of Abstract Domains for Shapes

authors:
Antoine Toubhans
Bor-Yuh Evan Chang
Xavier Rival


title: Abstraction-Guided Synthesis


title: State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction

authors:
Manchun Zheng
David Sanán
Jun Sun
Yang Liu
Jin Song Dong
Yu Gu


title: Compositional and Lightweight Dependent Type Inference for ML

authors:
He Zhu
Suresh Jagannathan


title: Modeling Parsimonious Putative Regulatory Networks: Complexity and Heuristic Approach

authors:
Vicente Acuña
Andrés Aravena
Alejandro Maass
Anne Siegel

abstract:
A relevant problem in systems biology is the description of the regulatory interactions between genes. It is observed that pairs of genes have significant correlation through several experimental conditions. The question is to find causal relationships that can explain this experimental evidence.

A putative regulatory network can be represented by an oriented weighted graph, where vertices represent genes, arcs represent predicted regulatory interactions and the arc weights represent the p-value of the prediction. Given such graph, and experimental evidence of correlation between pairs of vertices, we propose an abstraction and a method to enumerate all parsimonious subgraphs that assign causality relationships compatible with the experimental evidence.

When the problem is modeled as the minimization of a global weight function, we show that the enumeration of scenarios is a hard problem. As an heuristic, we model the problem as a set of independent minimization problems, each solvable in polynomial time, which can be combined to explore a relevant subset of the solution space. We present a logic-programming formalization of the model implemented using Answer Set Programming.

We show that, when the graph follows patterns that can be found in real organisms, our heuristic finds solutions that are good approximations to the full model. We encoded these approach using Answer Set Programming, applied this to a specific case in the organism E. coli and compared the execution time of each approach.


title: Parameterized Model Checking of Token-Passing Systems

authors:
Benjamin Aminof
Swen Jacobs
Ayrat Khalimov
Sasha Rubin

abstract:
We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL i?ź\X. Emerson and Namjoshi 1995, 2003 have shown that parameterized model checking of indexed CTL i?ź\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. 2004 have shown a similar result for general topologies and indexed LTL \X, provided processes cannot choose the directions for sending or receiving the token.

We unify and substantially extend these results by systematically exploring fragments of indexed CTL i?ź\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token.


title: Verifying Array Programs by Transforming Verification Conditions

authors:
Emanuele De Angelis
Fabio Fioravanti
Alberto Pettorossi
Maurizio Proietti


title: SAT-Based Synthesis Methods for Safety Specs

authors:
Roderick Bloem
Robert Könighofer
Martina Seidl

abstract: Automatic synthesis of hardware components from declarative specifications is an ambitious endeavor in computer aided design. Existing synthesis algorithms are often implemented with Binary Decision Diagrams BDDs, inheriting their scalability limitations. Instead of BDDs, we propose several new methods to synthesize finite-state systems from safety specifications using decision procedures for the satisfiability of quantified and unquantified Boolean formulas SAT-, QBF- and EPR-solvers. The presented approaches are based on computational learning, templates, or reduction to first-order logic. We also present an efficient parallelization, and optimizations to utilize reachability information and incremental solving. Finally, we compare all methods in an extensive case study. Our new methods outperform BDDs and other existing work on some classes of benchmarks, and our parallelization achieves a super-linear speedup.


title: Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops

authors:
Marius Bozga
Radu Iosif
Filip Konecný

abstract: This paper proves the NP-completeness of the reachability problem for the class of flat counter machines with difference bounds and, more generally, octagonal relations, labeling the transitions on the loops. The proof is based on the fact that the sequence of powers $\{R^i\}_{i=1}^\infty$ of such relations can be encoded as a periodic sequence of matrices, and that both the prefix and the period of this sequence are $2^{{O}||R||_2}$ in the size of the binary encoding ||R||2 of a relation R. This result allows to characterize the complexity of the reachability problem for one of the most studied class of counter machines [6,10], and has a potential impact on other problems in program verification.


title: Refuting Heap Reachability


title: Doomsday Equilibria for Omega-Regular Games

authors:
Krishnendu Chatterjee
Laurent Doyen
Emmanuel Filiot
Jean-François Raskin

abstract:
Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.

In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.

We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.


title: A Logic-Based Framework for Verifying Consensus Algorithms

authors:
Cezara Dragoi
Thomas A. Henzinger
Helmut Veith
Josef Widder
Damien Zufferey


title: Synthesis with Identifiers

authors:
Rüdiger Ehlers
Sanjit A. Seshia
Hadas Kress-Gazit


title: Monitoring Parametric Temporal Logic

authors:
Peter Faymonville
Bernd Finkbeiner
Doron A. Peled