| 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 |
|---|
|
SMACK: Decoupling Source Language Details from Verifier Implementations Zvonimir Rakamaric, Michael Emmi |
SMACK: Decoupling Source Language Details from Verifier Implementations Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Symbolic Resource Bound Inference for Functional Programs Ravichandhran Madhavan, Viktor Kuncak |
Symbolic Resource Bound Inference for Functional Programs Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Bruno Dutertre |
Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Author has
verified
information
|
|
|
Kenneth L. McMillan |
Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Regression Test Selection for Distributed Software Histories Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov |
Regression Test Selection for Distributed Software Histories Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Causal Termination of Multi-threaded Programs Andrey Kupriyanov, Bernd Finkbeiner |
Causal Termination of Multi-threaded Programs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
ICE: A Robust Framework for Learning Invariants Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider |
ICE: A Robust Framework for Learning Invariants Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Analyzing and Synthesizing Genomic Logic Functions Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler |
Analyzing and Synthesizing Genomic Logic Functions Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes Alejandro Sánchez, César Sánchez |
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Software Verification in the Google App-Engine Cloud Dirk Beyer, Georg Dresler, Philipp Wendler |
Software Verification in the Google App-Engine Cloud Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Verifying Relative Error Bounds Using Symbolic Simulation Jesse Bingham, Joe Leslie-Hurd |
Verifying Relative Error Bounds Using Symbolic Simulation Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
AVATAR: The Architecture for First-Order Theorem Provers Andrei Voronkov |
AVATAR: The Architecture for First-Order Theorem Provers Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Automatic Atomicity Verification for Clients of Concurrent Data Structures Mohsen Lesani, Todd D. Millstein, Jens Palsberg |
Automatic Atomicity Verification for Clients of Concurrent Data Structures Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
The nuXmv Symbolic Model Checker Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta |
The nuXmv Symbolic Model Checker Details |
|
Author Comments:
For any question or for the data related to the experimental evaluation performed, please contact nuxmv team. The contact information are available at: https://nuxmv.fbk.eu
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis Moritz Sinn, Florian Zuleger, Helmut Veith |
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections Willem Hagemann |
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Interpolating Property Directed Reachability Yakir Vizel, Arie Gurfinkel |
Interpolating Property Directed Reachability Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher |
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska |
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells Details |
|
Author Comments:
We have a tutorial appeared on the magazine of IEEE Design and Test, which can be found at https://ieeexplore.ieee.org/document/7130608
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
From Invariant Checking to Invariant Inference Using Randomized Search Rahul Sharma, Alex Aiken |
From Invariant Checking to Invariant Inference Using Randomized Search Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Minimizing Running Costs in Consumption Systems Tomás Brázdil, David Klaska, Antonín Kucera, Petr Novotný |
Minimizing Running Costs in Consumption Systems Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Engineering a Static Verification Tool for GPU Kernels Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer |
Engineering a Static Verification Tool for GPU Kernels Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Verifying LTL Properties of Hybrid Systems with K-Liveness Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
Verifying LTL Properties of Hybrid Systems with K-Liveness Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Suho Lee, Karem A. Sakallah |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Safraless Synthesis for Epistemic Temporal Specifications Rodica Bozianu, Catalin Dima, Emmanuel Filiot |
Safraless Synthesis for Epistemic Temporal Specifications Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
G4LTL-ST: Automatic Generation of PLC Programs Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann |
G4LTL-ST: Automatic Generation of PLC Programs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Vac - Verifier of Administrative Role-Based Access Control Policies Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato |
Vac - Verifier of Administrative Role-Based Access Control Policies Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies Omar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta |
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun |
Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Property-Directed Shape Analysis Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
Property-Directed Shape Analysis Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Finding Instability in Biological Models Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman |
Finding Instability in Biological Models Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Synthesis of Masking Countermeasures against Side Channel Attacks Hassan Eldib, Chao Wang |
Synthesis of Masking Countermeasures against Side Channel Attacks Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
From LTL to Deterministic Automata: A Safraless Compositional Approach Javier Esparza, Jan Kretínský |
From LTL to Deterministic Automata: A Safraless Compositional Approach Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli |
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Automating Separation Logic with Trees and Data Ruzica Piskac, Thomas Wies, Damien Zufferey |
Automating Separation Logic with Trees and Data Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
A Nonlinear Real Arithmetic Fragment Ashish Tiwari, Patrick Lincoln |
A Nonlinear Real Arithmetic Fragment Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components Anton Wijs, Joost-Pieter Katoen, Dragan Bosnacki |
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Regression-Free Synthesis for Concurrency Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
Regression-Free Synthesis for Concurrency Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Solving Games without Controllable Predecessor Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker |
Solving Games without Controllable Predecessor Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan |
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
A Conference Management System with Verified Document Confidentiality Sudeep Kanav, Peter Lammich, Andrei Popescu |
A Conference Management System with Verified Document Confidentiality Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Symbolic Visibly Pushdown Automata Loris D'Antoni, Rajeev Alur |
Symbolic Visibly Pushdown Automata Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Proving Non-termination Using Max-SMT Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
Proving Non-termination Using Max-SMT Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Shape Analysis via Second-Order Bi-Abduction Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
Shape Analysis via Second-Order Bi-Abduction Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl |
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications Petr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano |
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Termination Analysis by Learning Terminating Programs Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
Termination Analysis by Learning Terminating Programs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
CEGAR for Qualitative Analysis of Probabilistic Systems Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca |
CEGAR for Qualitative Analysis of Probabilistic Systems Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
String Constraints for Verification Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman |
String Constraints for Verification Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
SMT-Based Model Checking for Recursive Programs Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki |
SMT-Based Model Checking for Recursive Programs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Bit-Vector Rewriting with Automatic Rule Generation Alexander Nadel |
Bit-Vector Rewriting with Automatic Rule Generation Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Author has
verified
information
|
|
|
Optimal Guard Synthesis for Memory Safety Thomas Dillig, Isil Dillig, Swarat Chaudhuri |
Optimal Guard Synthesis for Memory Safety Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
An SMT-Based Approach to Coverability Analysis Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic |
An SMT-Based Approach to Coverability Analysis Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|