2,199 papers · page 14 of 110
Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, Zhenjiang Hu
Bidirectional live programming systems (BLP) enable developers to modify a program by directly manipulating the program output, so that the updated program can produce the manipulated output. One state-of-the-art approach to BLP systems is operation-based, which captures the deve…
Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, Cyrus Omar
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover fr…
Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao
Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. A…
Conrad Zimmerman, Jenna DiVincenzo, Jonathan Aldrich
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gra…
Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump
This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Extending the rich line of previous work on algebraic approaches to recursion schemes, we present an algebraic approach to divide-and-conquer recursion: recursions are represented as a…
Alejandro Aguirre, Lars Birkedal
Developing denotational models for higher-order languages that combine probabilistic and nondeterministic choice is known to be very challenging. In this paper, we propose an alternative approach based on operational techniques. We study a higher-order language combining parametr…
Rajeev Alur, Caleb Stanford, Christopher Watson
Motivated by distributed data processing applications, we introduce a class of labeled directed acyclic graphs constructed using sequential and parallel composition operations, and study automata and logics over them. We show that deterministic and non-deterministic acceptors ove…
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and computations to be related facilitates use of simpler relational invariants and relational procedure spe…
Victor Arrial, Giulio Guerrieri, Delia Kesner
We solve the inhabitation problem for a language called λ!, a subsuming paradigm (inspired by call-by-push-value) being able to encode, among others, call-by-name and call-by-value strategies of functional programming. The type specification uses a non-idempotent intersection typ…
Aurèle Barrière, Sandrine Blazy, David Pichardie
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution, interpretation can be initially used. But after a while, JITs dynamically produce native code for pa…
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
We develop a weakest-precondition-style calculus à la Dijkstra for reasoning about amortized expected runtimes of randomized algorithms with access to dynamic memory — the aert calculus. Our calculus is truly quantitative, i.e. instead of Boolean valued predicates, it manipulates…
Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
A fundamental problem in refinement verification is to check that the language of behaviors of an implementation is included in the language of the specification. We consider the refinement verification problem where the implementation is a multithreaded shared memory system mode…
Aaron Bembenek, Michael Greenberg, Stephen Chong
Given a set of candidate Datalog rules, the Datalog synthesis-as-rule-selection problem chooses a subset of these rules that satisfies a specification (such as an input-output example). Building off prior work using counterexample-guided inductive synthesis, we present a progress…
Filippo Bonchi, Alessandro Di Giorgio, Alessio Santamaria
Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as …
Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, Armando Solar-Lezama
This paper introduces corpus-guided top-down synthesis as a mechanism for synthesizing library functions that capture common functionality from a corpus of programs in a domain specific language (DSL). The algorithm builds abstractions directly from initial DSL primitives, using …
José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, Ashish Tiwari
Programming-by-Examples (PBE) involves synthesizing an "intended program" from a small set of user-provided input-output examples. A key PBE strategy has been to restrict the search to a carefully designed small domain-specific language (DSL) with "effectively-invertible" (EI) op…
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
Library learning compresses a given corpus of programs by extracting common structure from the corpus into reusable library functions. Prior work on library learning suffers from two limitations that prevent it from scaling to larger, more complex inputs. First, it explores too m…
Simon Castellan, Pierre Clairambault
We introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as Petri structures, certain coloured Petri nets. For the…
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic
This paper introduces ctrees, a monad for modeling nondeterministic, recursive, and impure programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds computations into coinductive trees with three kind of nodes: external events, and two variants of nondete…
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah
Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations …