| Title/Authors | Title | Research Artifacts
[?] A research
artifact is any by-product of a research project that is not
directly included in the published research paper. In Computer
Science research this is often source code and data sets, but
it could also be media, documentation, inputs to proof
assistants, shell-scripts to run experiments, etc.
|
Details |
|---|
|
Lightweight verification of separate compilation Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis |
Lightweight verification of separate compilation Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
A theory of effects and resources: adjunction models and polarised calculi Pierre-Louis Curien, Marcelo P. Fiore, Guillaume Munch-Maccagnoni |
A theory of effects and resources: adjunction models and polarised calculi Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
PSync: a partially synchronous language for fault-tolerant distributed algorithms Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey |
PSync: a partially synchronous language for fault-tolerant distributed algorithms Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Newtonian program analysis via tensor product Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu |
Newtonian program analysis via tensor product Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Not able to share produced artifacts
Verification:
Authors have
verified
information
|
|
Maximal specification synthesis Aws Albarghouthi, Isil Dillig, Arie Gurfinkel |
Maximal specification synthesis Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Modelling the ARMv8 architecture, operationally: concurrency and ISA Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell |
Modelling the ARMv8 architecture, operationally: concurrency and ISA Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Abstraction refinement guided by a learnt probabilistic model Radu Grigore, Hongseok Yang |
Abstraction refinement guided by a learnt probabilistic model Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Kleenex: compiling nondeterministic transducers to deterministic streaming transducers Niels Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm |
Kleenex: compiling nondeterministic transducers to deterministic streaming transducers Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Decidability of inferring inductive invariants Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv |
Decidability of inferring inductive invariants Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
PolyCheck: dynamic verification of iteration space transformations on affine programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan |
PolyCheck: dynamic verification of iteration space transformations on affine programs Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Fully-abstract compilation by approximate back-translation Dominique Devriese, Marco Patrignani, Frank Piessens |
Fully-abstract compilation by approximate back-translation Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Reducing crash recoverability to reachability Eric Koskinen, Junfeng Yang |
Reducing crash recoverability to reachability Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
'Cause I'm strong enough: reasoning about consistency choices in distributed systems Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro |
'Cause I'm strong enough: reasoning about consistency choices in distributed systems Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Stéphane Gimenez, Georg Moser |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Example-directed synthesis: a type-theoretic interpretation Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic |
Example-directed synthesis: a type-theoretic interpretation Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, Rouzbeh Hasheminezhad |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Rahman Lavaee |
Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Optimizing synthesis with metasketches James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze |
Optimizing synthesis with metasketches Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Estimating types in binaries using predictive modeling Omer Katz, Ran El-Yaniv, Eran Yahav |
Estimating types in binaries using predictive modeling Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Memoryful geometry of interaction II: recursion and adequacy Koko Muroya, Naohiko Hoshino, Ichiro Hasuo |
Memoryful geometry of interaction II: recursion and adequacy Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Symbolic computation of differential equivalences Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin |
Symbolic computation of differential equivalences Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
The artefact has been superseded by the tool ERODE:
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations, 23rd Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17).
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen |
Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
A journal version with additional data has been submitted. When it is accepted, we will provide a URL.
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Printing floating-point numbers: a faster, always correct method Marc Andrysco, Ranjit Jhala, Sorin Lerner |
Printing floating-point numbers: a faster, always correct method Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A program logic for concurrent objects under fair scheduling Hongjin Liang, Xinyu Feng |
A program logic for concurrent objects under fair scheduling Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Model checking for symbolic-heap separation logic with inductive predicates James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe |
Model checking for symbolic-heap separation logic with inductive predicates Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Learning programs from noisy data Veselin Raychev, Pavol Bielik, Martin T. Vechev, Andreas Krause |
Learning programs from noisy data Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Learning invariants using decision trees and implication counterexamples Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth |
Learning invariants using decision trees and implication counterexamples Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
SMO: an integrated approach to intra-array and inter-array storage optimization Somashekaracharya G. Bhaskaracharya, Uday Bondhugula, Albert Cohen |
SMO: an integrated approach to intra-array and inter-array storage optimization Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Overhauling SC atomics in C11 and OpenCL Mark Batty, Alastair F. Donaldson, John Wickerson |
Overhauling SC atomics in C11 and OpenCL Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Matthew Flatt |
Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Jean Pichon-Pharabod, Peter Sewell |
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Environmental bisimulations for probabilistic higher-order languages Davide Sangiorgi, Valeria Vignudelli |
Environmental bisimulations for probabilistic higher-order languages Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Query-guided maximum satisfiability Xin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik |
Query-guided maximum satisfiability Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Algorithms for algebraic path properties in concurrent systems of constant treewidth components Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis |
Algorithms for algebraic path properties in concurrent systems of constant treewidth components Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Synthesis of reactive controllers for hybrid systems (keynote) Richard M. Murray |
Synthesis of reactive controllers for hybrid systems (keynote) Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Transforming spreadsheet data types using examples Rishabh Singh, Sumit Gulwani |
Transforming spreadsheet data types using examples Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Automatic patch generation by learning correct code Fan Long, Martin Rinard |
Automatic patch generation by learning correct code Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
String solving with word equations and transducers: towards a logic for analysing mutation XSS Anthony Widjaja Lin, Pablo Barceló |
String solving with word equations and transducers: towards a logic for analysing mutation XSS Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Taming release-acquire consistency Ori Lahav, Nick Giannarakis, Viktor Vafeiadis |
Taming release-acquire consistency Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Sound type-dependent syntactic language extension Florian Lorenzen, Sebastian Erdweg |
Sound type-dependent syntactic language extension Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Fabular: regression formulas as probabilistic programming Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio V. Russo, Adam Scibior, Marcin Szymczak |
Fabular: regression formulas as probabilistic programming Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Pushdown control-flow analysis for free Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn |
Pushdown control-flow analysis for free Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Breaking through the normalization barrier: a self-interpreter for f-omega Matt Brown, Jens Palsberg |
Breaking through the normalization barrier: a self-interpreter for f-omega Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Effects as sessions, sessions as effects Dominic A. Orchard, Nobuko Yoshida |
Effects as sessions, sessions as effects Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Symbolic abstract data type inference Michael Emmi, Constantin Enea |
Symbolic abstract data type inference Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
System f-omega with equirecursive types for datatype-generic programming Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann |
System f-omega with equirecursive types for datatype-generic programming Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Chapar: certified causally consistent distributed key-value stores Mohsen Lesani, Christian J. Bell, Adam Chlipala |
Chapar: certified causally consistent distributed key-value stores Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Unboundedness and downward closures of higher-order pushdown automata Matthew Hague, Jonathan Kochems, C.-H. Luke Ong |
Unboundedness and downward closures of higher-order pushdown automata Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Programming the world of uncertain things (keynote) Kathryn S. McKinley |
Programming the world of uncertain things (keynote) Details |
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
|
From MinX to MinC: semantics-driven decompilation of recursive datatypes Edward Robbins, Andy King, Tom Schrijvers |
From MinX to MinC: semantics-driven decompilation of recursive datatypes Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Principal type inference for GADTs Sheng Chen, Martin Erwig |
Principal type inference for GADTs Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Not able to share produced artifacts
Verification:
Authors have
verified
information
|
|
Type theory in type theory using quotient inductive types Thorsten Altenkirch, Ambrus Kaposi |
Type theory in type theory using quotient inductive types Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Casper: an efficient approach to call trace collection Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang |
Casper: an efficient approach to call trace collection Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Damien Octeau, Somesh Jha, Matthew Dering, Patrick D. McDaniel, Alexandre Bartel, Li Li, Jacques Klein, Yves Le Traon |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Dependent types and multi-monadic effects in F Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin |
Dependent types and multi-monadic effects in F Details |
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility,
or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Scaling network verification using symmetry and surgery Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese |
Scaling network verification using symmetry and surgery Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Temporal verification of higher-order functional programs Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno |
Temporal verification of higher-order functional programs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Monitors and blame assignment for higher-order session types Limin Jia, Hannah Gommerstadt, Frank Pfenning |
Monitors and blame assignment for higher-order session types Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Lattice-theoretic progress measures and coalgebraic model checking Ichiro Hasuo, Shunsuke Shimizu, Corina Cîrstea |
Lattice-theoretic progress measures and coalgebraic model checking Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Ronald Garcia, Alison M. Clark, Éric Tanter |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Confluences in programming languages research (keynote) David Walker |
Confluences in programming languages research (keynote) Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
The gradualizer: a methodology and algorithm for generating gradual type systems Matteo Cimini, Jeremy G. Siek |
The gradualizer: a methodology and algorithm for generating gradual type systems Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|