Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Ruzica Piskac, Thomas Wies, Damien Zufferey |
Automating Separation Logic with Trees and Data. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Omar Chowdhury, Limin Jia 0001, Deepak Garg 0001, Anupam Datta |
Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta |
The nuXmv Symbolic Model Checker. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
Regression-Free Synthesis for Concurrency. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann |
G4LTL-ST: Automatic Generation of PLC Programs. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Omar Inverso, Ermenegildo Tomasco, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato |
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
Property-Directed Shape Analysis. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | 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. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Rahul Sharma 0001, Alex Aiken |
From Invariant Checking to Invariant Inference Using Randomized Search. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Pranav Garg 0001, Christof Löding, P. Madhusudan, Daniel Neider |
ICE: A Robust Framework for Learning Invariants. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Beyer 0001, Georg Dresler, Philipp Wendler |
Software Verification in the Google App-Engine Cloud. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
Proving Non-termination Using Max-SMT. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Loris D'Antoni, Rajeev Alur |
Symbolic Visibly Pushdown Automata. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Yakir Vizel, Arie Gurfinkel |
Interpolating Property Directed Reachability. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki |
SMT-Based Model Checking for Recursive Programs. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska |
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg |
Monadic Decomposition. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
Verifying LTL Properties of Hybrid Systems with K-Liveness. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher |
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic |
An SMT-Based Approach to Coverability Analysis. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Voronkov |
AVATAR: The Architecture for First-Order Theorem Provers. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen 0001, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman |
String Constraints for Verification. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Ravichandhran Madhavan, Viktor Kuncak |
Symbolic Resource Bound Inference for Functional Programs. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Jan Kretínský |
From LTL to Deterministic Automata: A Safraless Compositional Approach. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli |
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Andrey Kupriyanov, Bernd Finkbeiner |
Causal Termination of Multi-threaded Programs. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca |
CEGAR for Qualitative Analysis of Probabilistic Systems. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Milos Gligoric 0001, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov |
Regression Test Selection for Distributed Software Histories. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman |
Finding Instability in Biological Models. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jesse Bingham, Joe Leslie-Hurd |
Verifying Relative Error Bounds Using Symbolic Simulation. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
Termination Analysis by Learning Terminating Programs. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Moritz Sinn, Florian Zuleger, Helmut Veith |
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Nadel |
Bit-Vector Rewriting with Automatic Rule Generation. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Anton Wijs, Joost-Pieter Katoen, Dragan Bosnacki |
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Armin Biere, Roderick Bloem (eds.) |
Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alejandro Sánchez, César Sánchez 0001 |
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Mohsen Lesani, Todd D. Millstein, Jens Palsberg |
Automatic Atomicity Verification for Clients of Concurrent Data Structures. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Ashish Tiwari 0001, Patrick Lincoln |
A Nonlinear Real Arithmetic Fragment. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Petr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano |
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Dutertre |
Yices 2.2. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan 0001 |
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Dillig, Isil Dillig, Swarat Chaudhuri |
Optimal Guard Synthesis for Memory Safety. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Tomás Brázdil, David Klaska, Antonín Kucera 0001, Petr Novotný 0001 |
Minimizing Running Costs in Consumption Systems. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler |
Analyzing and Synthesizing Genomic Logic Functions. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
Shape Analysis via Second-Order Bi-Abduction. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Hassan Eldib, Chao Wang 0001 |
Synthesis of Masking Countermeasures against Side Channel Attacks. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Zvonimir Rakamaric, Michael Emmi |
SMACK: Decoupling Source Language Details from Verifier Implementations. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Henri Hansen, Shang-Wei Lin 0001, Yang Liu 0003, Truong Khanh Nguyen, Jun Sun 0001 |
Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl |
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Sudeep Kanav, Peter Lammich, Andrei Popescu 0001 |
A Conference Management System with Verified Document Confidentiality. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Willem Hagemann |
Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich |
The Spirit of Ghost Code. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato |
Vac - Verifier of Administrative Role-Based Access Control Policies. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Rodica Bozianu, Catalin Dima, Emmanuel Filiot |
Safraless Synthesis for Epistemic Temporal Specifications. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Suho Lee, Karem A. Sakallah |
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
Lazy Annotation Revisited. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Tianyi Liang, Andrew Reynolds 0001, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker |
Solving Games without Controllable Predecessor. |
CAV |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Puggelli, Wenchao Li 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Romain Brenguier |
PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, Jirí Weiser |
DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Isil Dillig, Thomas Dillig |
Explain: A Tool for Performing Abductive Inference. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Richard Uhler, Nirav Dave |
Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Lukás Holík, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar |
Fully Automated Shape Analysis Based on Forest Automata. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Fabrizio Biondi, Axel Legay, Louis-Marie Traonouez, Andrzej Wasowski |
QUAIL: A Quantitative Security Analyzer for Imperative Code. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid |
Recursive Program Synthesis. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz |
Lazy Abstractions for Timed Automata. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Donzé, Thomas Ferrère, Oded Maler |
Efficient Robust Monitoring for STL. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Oshri Adler, Cindy Eisner, Tatyana Veksler |
Relative Equivalence in the Presence of Ambiguity. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Aleksandar Chakarov, Sriram Sankaranarayanan 0001 |
Probabilistic Program Analysis with Martingales. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Krishnendu Chatterjee, Jakub Lacki |
Faster Algorithms for Markov Decision Processes with Low Treewidth. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Ming-Hsien Tsai 0001, Yih-Kuen Tsay, Yu-Shiang Hwang |
GOAL for Games, Omega-Automata, and Logics. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Qinsi Wang |
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Ocan Sankur |
Shrinktech: A Tool for the Robustness Analysis of Timed Automata. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
A Scalable and Nearly Uniform Generator of SAT Witnesses. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Étienne André, Yang Liu 0003, Jun Sun 0001, Jin Song Dong, Shang-Wei Lin 0001 |
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Pierre Ganty, Rupak Majumdar |
Parameterized Verification of Asynchronous Shared-Memory Systems. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Yakir Vizel, Vadim Ryvchin, Alexander Nadel |
Efficient Generation of Small Interpolants in CNF. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
A Fully Verified Executable LTL Model Checker. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Cezara Dragoi, Ashutosh Gupta 0001, Thomas A. Henzinger |
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Loris D'Antoni, Margus Veanes |
Equivalence of Extended Symbolic Finite Transducers. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Lubos Brim, Milan Ceska 0002, Sven Drazan, David Safránek |
Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Hristina Palikareva, Cristian Cadar |
Multi-solver Support in Symbolic Execution. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Alistair Stewart, Kousha Etessami, Mihalis Yannakakis |
Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Chih-Hong Cheng, Harald Ruess, Natarajan Shankar |
JBernstein: A Validity Checker for Generalized Polynomial Constraints. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko |
Solving Existentially Quantified Horn Clauses. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Shaull Almagor, Guy Avni, Orna Kupferman |
Automatic Generation of Quality Specifications. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli, Enrico Tronci |
System Level Formal Verification via Model Checking Driven Simulation. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Cyrille Jégourel, Axel Legay, Sean Sedwards |
Importance Splitting for Statistical Model Checking Rare Properties. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | João Marques-Silva 0001, Mikolás Janota, Anton Belov |
Minimal Sets over Monotone Predicates in Boolean Formulae. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
Software Model Checking for People Who Love Automata. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Maximilien Colange, Souheib Baarir, Fabrice Kordon, Yann Thierry-Mieg |
Towards Distributed Software Model-Checking Using Decision Diagrams. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Ayrat Khalimov 0001, Swen Jacobs, Roderick Bloem |
PARTY Parameterized Synthesis of Token Rings. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Liyun Dai, Bican Xia, Naijun Zhan |
Generating Non-linear Interpolants by Semidefinite Programming. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Wonisch, Alexander Schremmer, Heike Wehrheim |
Programs from Proofs - A PCC Alternative. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Christian von Essen, Barbara Jobstmann |
Program Repair without Regret. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Aws Albarghouthi, Kenneth L. McMillan |
Beautiful Interpolants. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Braibant, Adam Chlipala |
Formal Verification of Hardware Synthesis. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Marc Brockschmidt, Byron Cook, Carsten Fuhs |
Better Termination Proving through Cooperation. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|