Computer Aided Verification, CAV 2014


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

Yices 2.2

Bruno Dutertre

Yices 2.2

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Author has verified information

Lazy Annotation Revisited

Kenneth L. McMillan

Lazy Annotation Revisited

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

Monadic Decomposition

Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, Sergey Bereg

Monadic Decomposition

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

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction

Suho Lee, Karem A. Sakallah

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction

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

The Spirit of Ghost Code

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich

The Spirit of Ghost Code

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