Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Alessandro Armando, David A. Basin, Mehdi Bouallagui, Yannick Chevalier, Luca Compagna, Sebastian Mödersheim, Michaël Rusinowitch, Mathieu Turuani, Luca Viganò 0001, Laurent Vigneron |
The AVISS Security Protocol Analysis Tool. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Blom, Jaco van de Pol |
State Space Reduction by Proving Confluence. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
on-the-fly state space reduction, symbolic transformation, 7CRL tool set, theorem proving, Labeled transition systems, partial order reduction, confluence, branching bisimulation |
1 | Victor Khomenko, Maciej Koutny, Walter Vogler |
Canonical Prefixes of Petri Net Unfoldings. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
canonical prefix, Model checking, Petri nets, unfolding |
1 | Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia |
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Michael Colón, Henny Sipma |
Practical Methods for Proving Program Termination. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Gerard J. Holzmann |
Software Analysis and Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Li Tan, Rance Cleaveland |
Evidence-Based Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
diagnostic information, Model checking, temporal logic, mu-calculus |
1 | Kenneth L. McMillan |
Applying SAT Methods in Unbounded Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Eugene Asarin, Thao Dang 0001, Oded Maler |
The d/dt Tool for Verification of Hybrid Systems. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Marius Bozga, Susanne Graf, Laurent Mounier |
IF-2.0: A Validation Environment for Component-Based Real-Time Systems. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer |
Temporal-Safety Proofs for Systems Code. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
NuSMV 2: An OpenSource Tool for Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Sriram K. Rajamani, Jakob Rehof |
Conformance Checking for Models of Asynchronous Message Passing Software. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Sharon Barner, Orna Grumberg |
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Sankar Gurumurthy, Roderick Bloem, Fabio Somenzi |
Fair Simulation Minimization. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Robert P. Kurshan, Vladimir Levin, Hüsnü Yenigün |
Compressing Transitions for Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Amir Pnueli, Jessie Xu, Lenore D. Zuck |
Liveness with (0, 1, infty)-Counter Abstraction. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Alex Groce, Doron A. Peled, Mihalis Yannakakis |
AMC: An Adaptive Model Checker. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Clark W. Barrett, David L. Dill, Aaron Stump |
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
Satisfiability, First-Order Logic, Decision Procedures, Propositional Satisfiability |
1 | Wolfgang Thomas |
Infinite Games and Verification (Extended Abstract of a Tutorial). |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal |
PathFinder: A Tool for Design Exploration. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
Model Checking, Debugging, Design Exploration, PathFinder |
1 | Ed Brinksma, Kim Guldstrand Larsen (eds.) |
Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant |
Deciding Separation Formulas with SAT. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger |
The Symbolic Approach to Hybrid Systems. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Yannick Chevalier, Laurent Vigneron |
Automated Unbounded Verification of Security Protocols. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jesse D. Bingham, Alan J. Hu |
Semi-formal Bounded Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Mitra Purandare, Fabio Somenzi |
Vacuum Cleaning CTL Formulae. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Lintao Zhang, Sharad Malik |
The Quest for Efficient Boolean Satisfiability Solvers. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Bengt Jonsson 0001, Pritha Mahata, Julien d'Orso |
Regular Tree Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Sharon Barner, Daniel Geist, Anna Gringauze |
Symbolic Localization Reduction with Reconstruction Layering and Backtracking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Michael McDougall, Zijiang Yang |
Exploiting Behavioral Hierarchy for Efficient Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Marsha Chechik, Arie Gurfinkel, Benet Devereux |
chi-Chek: A Multi-valued Model-Checker. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang |
Interface Compatibility Checking for Software Modules. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Walter Hartong, Lars Hedrich, Erich Barke |
On Discrete Modeling and Model Checking for Nonlinear Analog Systems. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Patrick Cousot, Radhia Cousot |
On Abstraction in Software Verification. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Dawn Xiaodong Song, Adrian Perrig, Doantam Phan |
AGVI - Automatic Generation, Verification, and Implementation of Security Protocols. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Ball, Sriram K. Rajamani |
The SLAM Toolkit. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Orna Grumberg, Tamir Heyman, Assaf Schuster |
Distributed Symbolic Model Checking for µ-Calculus. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi |
Benefits of Bounded Model Checking at an Industrial Setting. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Agostino Dovier, Carla Piazza, Alberto Policriti |
A Fast Bisimulation Algorithm. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
non well-founded sets, verification, automata, Bisimulation |
1 | Yasmina Abdeddaïm, Oded Maler |
Job-Shop Scheduling Using Timed Automata. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin |
Attacking Symbolic State Explosion. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Paul Gastin, Denis Oddoux |
Fast LTL to Büchi Automata Translation. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu |
TReX: A Tool for Reachability Analysis of Complex Systems. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Martin Leucker, Thomas Noll 0001 |
Truth/SLC - A Parallel Verification Platform for Concurrent Systems. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi |
A Practical Approach to Coverage in Model Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Kuehlmann, Jason Baumgartner |
Transformation-Based Verification Using Generalized Retiming. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | J Strother Moore |
Rewriting for Symbolic Execution of State Machine Models. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
microprocessor simulation, pipelined machine, verification, theorem proving, Hardware modeling |
1 | Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh |
The Temporal Logic Sugar. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi |
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Ranjit Jhala, Kenneth L. McMillan |
Microarchitecture Verification by Compositional Model Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Gérard Berry, Hubert Comon, Alain Finkel (eds.) |
Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Yoav Rodeh, Ofer Strichman |
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn |
As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Miroslav N. Velev, Randal E. Bryant |
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen |
EASN: Integrating ASN.1 and Model Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | David Lorge Parnas |
Software Documentation and the Verification Process. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Blom, Wan J. Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol |
µCRL: A Toolset for Analysing Algebraic Specifications. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Yves Bertot |
Formalizing a JVML Verifier for Initialization in a Theorem Prover. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Xavier Leroy |
Java Bytecode Verification: An Overview. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Bow-Yaw Wang |
Verifying Network Protocol Implementations by Symbolic Refinement Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Zhe Dang |
Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Luca de Alfaro |
Model Checking the World Wide Web. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane |
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m). |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Asteroth, Christel Baier, Ulrich Aßmann |
Model Checking with Formula-Dependent Abstract Models. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, Stefan Schwoon |
A BDD-Based Model Checker for Recursive Programs. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Vladimir Levin, Hüsnü Yenigün |
SDLcheck: A Model Checking Tool. |
CAV |
2001 |
DBLP BibTeX RDF |
|
1 | Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar |
ICS: Integrated Canonizer and Solver. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Kousha Etessami, Mihalis Yannakakis |
Analysis of Recursive State Machines. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Kedar S. Namjoshi |
Certifying Model Checkers. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | A. Prasad Sistla, Patrice Godefroid |
Symmetry and Reduced Symmetry in Model Checking. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Girish Bhat, Rance Cleaveland, Alex Groce |
Efficient Model Checking Via Büchi Tableau Automata. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Hao Zheng 0001, Eric Mercer, Chris J. Myers |
Automatic Abstraction for Verification of Timed Circuits and Systems. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Peer Johannsen |
BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Tamarah Arons |
Using Timestamping and History Variables to Verify Sequential Consistency. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Abhik Roychoudhury, I. V. Ramakrishnan |
Automated Inductive Verification of Parameterized Protocols. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Dennis Dams, Yassine Lakhnech, Martin Steffen |
Iterating Transducers. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Per Bjesse, Tim Leonard, Abdel Mokkedem |
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss |
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venier, Daniel Weil, Sergio Yovine |
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala |
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Gianpiero Cabodi |
Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Monika Maidl |
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
Parameterized Verification with Automatically Computed Inductive Assertions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Ofer Strichman |
Tuning SAT Checkers for Bounded Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ernie Cohen |
TAPS: A First-Order Verifier for Cryptographic Protocols. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ahmed Bouajjani, Bengt Jonsson 0001, Marcus Nilsson, Tayssir Touili |
Regular Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit 0001 |
Are Timed Automata Updatable? |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Miroslav N. Velev |
Formal Verification of VLIW Microprocessors with Speculative Execution. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Bengt Jonsson 0001 |
Invited Tutorial: Verification of Infinite-State and Parameterized Systems. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nylén |
Unfoldings of Unbounded Petri Nets. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas |
Verifying Advanced Microarchitectures that Support Speculation and Exceptions. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta 0001 |
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Christopher Colby, Peter Lee 0001, George C. Necula |
A Proof-Carrying Code Architecture for Java. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
Detecting Errors Before Reaching Them. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Moshe Y. Vardi |
An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon |
Efficient Algorithms for Model Checking Pushdown Systems. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Amir Pnueli, Elad Shahar |
Liveness and Acceleration in Parameterized Verification. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Jens Vöge, Marcin Jurdzinski |
A Discrete Strategy Improvement Algorithm for Solving Parity Games. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Giorgio Delzanno |
Automatic Verification of Parameterized Cache Coherence Protocols. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|