| 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 |
|---|
|
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer |
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks 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
|
|
Simulation-Equivalent Reachability of Large Linear Systems with Inputs Stanley Bak, Parasara Sridhar Duggirala |
Simulation-Equivalent Reachability of Large Linear Systems with Inputs 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
|
|
Classification and Coverage-Based Falsification for Embedded Control Systems Arvind S. Adimoolam, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin |
Classification and Coverage-Based Falsification for Embedded Control Systems Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Synthesis with Abstract Examples Dana Drachsler-Cohen, Sharon Shoham, Eran Yahav |
Synthesis with Abstract Examples Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
The Power of Symbolic Automata and Transducers Loris D'Antoni, Margus Veanes |
The Power of Symbolic Automata and Transducers Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar |
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds 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
|
|
Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul L. Jones, Scott A. Smolka, Radu Grosu |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Value Iteration for Long-Run Average Reward in Markov Decision Processes Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer |
Value Iteration for Long-Run Average Reward in Markov Decision Processes Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Runtime Monitoring with Recovery of the SENT Communication Protocol Konstantin Selyunin, Stefan Jaksic, Thang Nguyen, Christian Reidl, Udo Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu |
Runtime Monitoring with Recovery of the SENT Communication Protocol Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Runtime Verification of Temporal Properties over Out-of-Order Data Streams David A. Basin, Felix Klaedtke, Eugen Zalinescu |
Runtime Verification of Temporal Properties over Out-of-Order Data Streams Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Safety Verification of Deep Neural Networks Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu |
Safety Verification of Deep Neural Networks Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Context-Sensitive Dynamic Partial Order Reduction Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, Peter J. Stuckey |
Context-Sensitive Dynamic Partial Order Reduction Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan |
DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems 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:
DryVR is an open source tool for verification of hybrid systems with black-box components
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
MightyL: A Compositional Translation from MITL to Timed Automata Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege |
MightyL: A Compositional Translation from MITL to Timed Automata 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
|
|
Repairing Decision-Making Programs Under Uncertainty Aws Albarghouthi, Loris D'Antoni, Samuel Drews |
Repairing Decision-Making Programs Under Uncertainty Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Markov Automata with Multiple Objectives Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen |
Markov Automata with Multiple Objectives 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
|
|
Logical Clustering and Learning for Time-Series Data Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Sanjit A. Seshia |
Logical Clustering and Learning for Time-Series Data 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
|
|
Program Verification Under Weak Memory Consistency Using Separation Logic Viktor Vafeiadis |
Program Verification Under Weak Memory Consistency Using Separation Logic Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
GPUDrano: Detecting Uncoalesced Accesses in GPU Programs Rajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania |
GPUDrano: Detecting Uncoalesced Accesses in GPU Programs 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
|
|
Data-Driven Synthesis of Full Probabilistic Programs Sarah Chasins, Phitchaya Mangpo Phothilimthana |
Data-Driven Synthesis of Full Probabilistic Programs Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Montre: A Tool for Monitoring Timed Regular Expressions Dogan Ulus |
Montre: A Tool for Monitoring Timed Regular Expressions 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
|
|
STLInspector: STL Validation with Guarantees Hendrik Roehm, Thomas Heinz, Eva Charlotte Mayer |
STLInspector: STL Validation with Guarantees 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
|
|
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes Christel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich |
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes 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
|
|
Maximum Satisfiability in Software Analysis: Applications and Techniques Xujie Si, Xin Zhang, Radu Grigore, Mayur Naik |
Maximum Satisfiability in Software Analysis: Applications and Techniques Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Starling: Lightweight Concurrency Verification with Views Matt Windsor, Mike Dodds, Ben Simner, Matthew J. Parkinson |
Starling: Lightweight Concurrency Verification with Views 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
|
|
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek |
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems 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
|
|
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen |
Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants 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
|
|
Learning a Static Analyzer from Data Pavol Bielik, Veselin Raychev, Martin T. Vechev |
Learning a Static Analyzer from Data Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Compositional Model Checking with Incremental Counter-Example Construction Anton Wijs, Thomas Neele |
Compositional Model Checking with Incremental Counter-Example Construction 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
|
|
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks Luca Cardelli, Milan Ceska, Martin Fränzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby |
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems Marie Fortin, Anca Muscholl, Igor Walukiewicz |
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin |
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Model Counting for Recursively-Defined Strings Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar |
Model Counting for Recursively-Defined Strings Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
On Multiphase-Linear Ranking Functions Amir M. Ben-Amram, Samir Genaim |
On Multiphase-Linear Ranking Functions Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Automating Induction for Solving Horn Clauses Hiroshi Unno, Sho Torii, Hiroki Sakamoto |
Automating Induction for Solving Horn Clauses 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
|
|
Cutoff Bounds for Consensus Algorithms Ognjen Maric, Christoph Sprenger, David A. Basin |
Cutoff Bounds for Consensus Algorithms Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex |
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Verifying Equivalence of Spark Programs Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv |
Verifying Equivalence of Spark Programs 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
|
|
Quantitative Assume Guarantee Synthesis Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner |
Quantitative Assume Guarantee Synthesis Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
BoSy: An Experimentation Framework for Bounded Synthesis Peter Faymonville, Bernd Finkbeiner, Leander Tentrup |
BoSy: An Experimentation Framework for Bounded Synthesis 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
|
|
Efficient Parallel Strategy Improvement for Parity Games John Fearnley |
Efficient Parallel Strategy Improvement for Parity Games Details |
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
|
Non-polynomial Worst-Case Analysis of Recursive Programs Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady |
Non-polynomial Worst-Case Analysis of Recursive Programs 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
|
|
Towards Verifying Nonlinear Integer Arithmetic Paul Beame, Vincent Liew |
Towards Verifying Nonlinear Integer Arithmetic Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli |
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification 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
|
|
EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties Bernd Finkbeiner, Christopher Hahn, Marvin Stenger |
EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties 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
|
|
Synchronization Synthesis for Network Programs Jedidiah McClurg, Hossein Hojjat, Pavol Cerný |
Synchronization Synthesis for Network Programs 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
|
|
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis Adrià Gascón, Ashish Tiwari, Brent Carmer, Umang Mathur |
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis 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
|
|
Verified Compilation of Space-Efficient Reversible Circuits Matthew Amy, Martin Roetteler, Krysta M. Svore |
Verified Compilation of Space-Efficient Reversible Circuits Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin T. Vechev |
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Ascertaining Uncertainty for Efficient Exact Cache Analysis Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke |
Ascertaining Uncertainty for Efficient Exact Cache Analysis Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq 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
|
|
Minimization of Symbolic Transducers Olli Saarikivi, Margus Veanes |
Minimization of Symbolic Transducers Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A Storm is Coming: A Modern Probabilistic Model Checker Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk |
A Storm is Coming: A Modern Probabilistic Model Checker 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
|
|
Eshan Singh, Clark W. Barrett, Subhasish Mitra |
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 Correct-by-Decision Solution for Simultaneous Place and Route Alexander Nadel |
A Correct-by-Decision Solution for Simultaneous Place and Route Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Author has
verified
information
|
|
|
Proving Linearizability Using Forward Simulations Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil |
Proving Linearizability Using Forward Simulations Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Abstract Interpretation with Unfoldings Marcelo Sousa, César Rodríguez, Vijay D'Silva, Daniel Kroening |
Abstract Interpretation with Unfoldings 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
|
|
Automated Resource Analysis with Coq Proof Objects Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao |
Automated Resource Analysis with Coq Proof Objects 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:
Not able to share produced artifacts
Verification:
Authors have
verified
information
|
|
Bounded Synthesis for Streett, Rabin, and \text CTL^* Ayrat Khalimov, Roderick Bloem |
Bounded Synthesis for Streett, Rabin, and \text CTL^* Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
On Expansion and Resolution in CEGAR Based QBF Solving Leander Tentrup |
On Expansion and Resolution in CEGAR Based QBF Solving 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
|
|
Network-Wide Configuration Synthesis Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin T. Vechev |
Network-Wide Configuration Synthesis Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|