Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Edward W. Felten |
Coping with Outside-the-Box Attacks. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Aarti Gupta, Sharad Malik (eds.) |
Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Surender Baswana, Shashank K. Mehta, Vishal Powar |
Implied Set Closure and Its Application to Memory Consistency Verification. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
Memory consistency model verification, Incremental transitive closure, Total store order, Shared memory multi-processor |
1 | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
Proving Conditional Termination. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv |
Thread Quantification for Concurrent Shape Analysis. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Ariel Cohen 0002, Kedar S. Namjoshi |
Local Proofs for Linear-Time Properties of Concurrent Programs. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Ambar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh 0002, Swarup Mohalik, K. C. Shashidhar |
AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Peter W. O'Hearn |
Tutorial on Separation Logic (Invited Tutorial). |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Peter Niebert, Doron A. Peled, Amir Pnueli |
Discriminative Model Checking. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Azadeh Farzan, P. Madhusudan |
Monitoring Atomicity in Concurrent Programs. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
Scalable Shape Analysis for Systems Code. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Laura I. Meikle, Jacques D. Fleuriot |
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Sebastian Burckhardt, Madanlal Musuvathi |
Effective Program Verification for Relaxed Memory Models. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou |
Automated Assume-Guarantee Reasoning by Abstraction Refinement. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Per Bjesse |
A Practical Approach to Word Level Model Checking of Industrial Netlists. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine |
Monotonic Abstraction for Programs with Dynamic Memory Heaps. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Deepak D'Souza, Madhu Gopinathan |
Conflict-Tolerant Features. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | James R. Larus |
Singularity: Designing Better Software (Invited Talk). |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Naoki Kobayashi 0001, Davide Sangiorgi |
A Hybrid Type System for Lock-Freedom of Mobile Processes. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou 0001 |
QMC: A Model Checker for Quantum Systems. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Huu Hai Nguyen, Wei-Ngan Chin |
Enhancing Program Verification with Lemmas. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
Lemma Proving, Lemma Application, Program Verification, Separation Logic, Entailment |
1 | Ariel Cohen 0002, Amir Pnueli, Lenore D. Zuck |
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Ruzica Piskac, Viktor Kuncak |
Linear Arithmetic with Stars. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith |
FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Beyer 0001, Damien Zufferey, Rupak Majumdar |
CSIsat: Interpolation for LA+EUF. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
The Barcelogic SMT Solver. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi |
Application of Formal Word-Level Analysis to Constrained Random Simulation. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Bhargav S. Gulavani, Sumit Gulwani |
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Holger Hermanns, Björn Wachter, Lijun Zhang 0001 |
Probabilistic CEGAR. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Edelkamp, Peter Sanders 0001, Pavel Simecek |
Semi-external LTL Model Checking. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Aditya Kanade, Gera Weiss |
Ranking Automata and Games for Prioritized Requirements. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Beyer 0001, Thomas A. Henzinger, Grégory Théoduloz |
Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Sumit Gulwani, Ashish Tiwari 0001 |
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Hubert Garavel, Radu Mateescu 0001, Frédéric Lang, Wendelin Serwe |
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Nathaniel Charlton, Michael Huth 0001 |
Hector: Software Model Checking with Cooperating Analysis Plugins. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Ball, Orna Kupferman, Mooly Sagiv |
Leaping Loops in the Presence of Abstraction. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Nishant Sinha 0001, Edmund M. Clarke |
SAT-Based Compositional Verification Using Lazy Learning. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Robert Brummayer, Armin Biere |
C32SAT: Checking C Expressions. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | David M. Russinoff |
A Mathematical Approach to RTL Verification. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Christophe Filliâtre, Claude Marché |
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv |
Revamping TVLA: Making Parametric Shape Analysis Competitive. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Luca de Alfaro, Marco Faella |
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev |
RAT: A Tool for the Formal Analysis of Requirements. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jonathan Ezekiel, Gerald Lüttgen, Gianfranco Ciardo |
Parallelising Symbolic State-Space Generators. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Werner Damm, Holger Hermanns (eds.) |
Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Ranjit Jhala, Kenneth L. McMillan |
Array Abstractions from Proofs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon 0001 |
BAT: The Bit-Level Analysis Tool. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
Hybrid Systems: From Verification to Falsification. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Beyer 0001, Thomas A. Henzinger, Vasu Singh |
Algorithms for Interface Synthesis. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, Roderick Bloem |
Anzu: A Tool for Property Synthesis. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta |
Boolean Abstraction for Temporal Logic Satisfiability. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Feng Chen 0006, Grigore Rosu |
Parametric and Sliced Causality. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Byron Cook |
Automatically Proving Program Termination. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jiri Barnat, Lubos Brim, Pavel Simecek |
I/O Efficient Accepting Cycle Detection. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine |
Parameterized Verification of Infinite-State Processes with Global Conditions. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Denis Gopan, Thomas W. Reps |
Low-Level Library Analysis and Summarization. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Ariel Cohen 0002, Kedar S. Namjoshi |
Local Proofs for Global Safety Properties. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Bengt Jonsson 0001, Mayank Saksena |
Systematic Acceleration in Regular Model Checking. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Oded Maler, Dejan Nickovic, Amir Pnueli |
On Synthesizing Controllers from Bounded-Response Properties. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kropf |
Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf |
Three-Valued Abstraction for Continuous-Time Markov Chains. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Domagoj Babic, Alan J. Hu |
Structural Abstraction of Software Verification Conditions. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Tarik Nahhal, Thao Dang 0001 |
Test Coverage for Continuous and Hybrid Systems. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Vijay Ganesh, David L. Dill |
A Decision Procedure for Bit-Vectors and Arrays. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Bernd Becker 0001, Christian Dax, Jochen Eisinger, Felix Klaedtke |
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
Comparison Under Abstraction for Verifying Linearizability. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Clark W. Barrett, Cesare Tinelli |
CVC3. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Chao Wang 0001, Zijiang Yang 0006, Aarti Gupta, Franjo Ivancic |
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Vineet Kahlon, Yu Yang 0013, Sriram Sankaranarayanan 0001, Aarti Gupta |
Fast and Accurate Static Data-Race Detection for Concurrent Programs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Martin Fränzle |
Verification of Hybrid Systems. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Arie Matsliah, Ofer Strichman |
Underapproximation for Model-Checking Based on Random Cryptographic Constructions. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer |
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Wahl |
Adaptive Symmetry Reduction. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Gaël Patin, Mihaela Sighireanu, Tayssir Touili |
Spade: Verification of Multithreaded Dynamic and Recursive Programs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar |
A Tutorial on Satisfiability Modulo Theories. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang |
Shape Analysis for Composite Data Structures. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
From Liveness to Promptness. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Luca de Alfaro, Pritam Roy |
Magnifying-Lens Abstraction for Markov Decision Processes. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Martin Ouimet, Kristina Lundqvist |
The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime |
UPPAAL-Tiga: Time for Playing Games! |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Marc Segelken |
Abstraction and Counterexample-Guided Construction of omega -Automata for Model Checking of Step-Discrete Linear Hybrid Models. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
automata construction, counterexample guidance, iterative abstraction refinement, step-discrete hybrid systems, model-checking |
1 | Sagar Chaki, Christian Schallhart, Helmut Veith |
Verification Across Intellectual Property Boundaries. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza |
jMoped: A Test Environment for Java Programs. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Gary T. Leavens, Joseph R. Kiniry, Erik Poll |
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Anubhav Gupta 0001, Kenneth L. McMillan, Zhaohui Fu |
Automated Assumption Generation for Compositional Verification. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Byron Cook, Andreas Podelski, Andrey Rybalchenko |
Terminator: Beyond Safety. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Manuvir Das |
Formal Specifications on Industrial-Strength Code-From Myth to Reality. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Koushik Sen, Gul Agha |
CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Kroening, Georg Weissenbacher |
Counterexamples with Loops for Predicate Abstraction. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin |
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Grigore Rosu, Saddek Bensalem |
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Azadeh Farzan, P. Madhusudan |
Causal Atomicity. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Sébastien Bardin, Jérôme Leroux, Gérald Point |
FAST Extended Release. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
counter systems verification, generic Presburger interface, automata with cache computation, acceleration |
1 | Mark Braverman |
Termination of Integer Linear Programs. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Amitabha Roy 0002, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang |
Fast and Generalized Polynomial Time Memory Consistency Verification. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
Languages of Nested Trees. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Vineet Kahlon, Aarti Gupta, Nishant Sinha 0001 |
Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Panagiotis Manolios, Daron Vroon 0001 |
Termination Analysis with Calling Context Graphs. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Dutertre, Leonardo Mendonça de Moura |
A Fast Linear-Arithmetic Solver for DPLL(T). |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|