| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Fabio Somenzi, Roderick Bloem |
Efficient Büchi Automata from LTL Formulae.  |
CAV  |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | James H. Kukula, Thomas R. Shiple |
Building Circuits from Relations. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix |
Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur, Radu Grosu, Michael McDougall |
Efficient Reachability Analysis of Hierarchical Reactive Machines. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomohiro Yoneda |
VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen |
An Abstraction Algorithm for the Verification of Generalized C-Slow Designs. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu 0004, Helmut Veith |
Counterexample-Guided Abstraction Refinement. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster |
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kedar S. Namjoshi, Robert P. Kurshan |
Syntactic Program Transformations for Automatic Abstraction. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Abdelwaheb Ayari, David A. Basin |
Bounded Model Construction for Monadic Second-Order Logics. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Scott D. Stoller, Leena Unnikrishnan, Yanhong A. Liu |
Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenneth L. McMillan, Shaz Qadeer, James B. Saxe |
Induction in Compositional Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Kedar S. Namjoshi, Richard J. Trefler |
On the Competeness of Compositional Reasoning. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | E. Allen Emerson, A. Prasad Sistla (eds.) |
Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, Harald Rueß |
Integrating WS1S with PVS. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Elsa L. Gunter, Robert P. Kurshan, Doron A. Peled |
PET: An Interactive Software Testing Tool. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Miroslav N. Velev |
Boolean Satisfiability with Transitivity Constraints. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, Yaron Wolfsthal |
FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier |
IF: A Validation Environment for Timed Asynchronous Systems. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Catherine Meadows 0001 |
Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | William Chan |
Temporal-Locig Queries. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su |
Binary Reachability Analysis of Discrete Pushdown Timed Automata. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Aurore Annichini, Eugene Asarin, Ahmed Bouajjani |
Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerd Behrmann, Thomas Hune, Frits W. Vaandrager |
Distributing Timed Model Checking - How the Search Order Matters. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Franck Cassez, François Laroussinie |
Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen |
Model Checking Continuous-Time Markov Chains by Transient Analysis. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Bienmüller, Werner Damm, Hartmut Wittke |
The STATEMATE Verification Environment - Making It Real. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | João Marques-Silva 0001, Karem A. Sakallah |
Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | C. R. Ramakrishnan 0001, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury, V. N. Venkatakrishnan |
XMC: A Logic-Programming-Based Verification Toolset. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Michaël Rusinowitch, Sorin Stratulat, Francis Klay |
Mechanical Verification of an Ideal Incremental ABR Conformance. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Abdelwaheb Ayari, David A. Basin, Felix Klaedtke |
Decision Procedures for Inductive Boolean Functions Based on Alternating Automata. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Spielmann |
Automatic Verification of Abstract State Machines. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Johann Schumann |
PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Basin, Stefan Friedrich 0001, Joachim Posegga, Harald Vogt |
Java Bytecode Verification by Model Checking. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron |
Optimizing Symbolic Model Checking for Constraint-Rich Models. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Zohar Manna, Henny Sipma |
Verification of Parameterized Systems by Dynamic Induction on Diagrams. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Jørn Lind-Nielsen, Henrik Reif Andersen |
Stepwise CTL Model Checking of State/Event Systems. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson 0001, Marcus Nilsson |
Handling Global Conditions in Parameterized System Verification. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Steven M. German, Miroslav N. Velev |
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz |
Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Nils Klarlund |
A Theory of Restrictions for Logics and Automata. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Rom Langerak, Ed Brinksma |
A Complete Finite Prefix for Process Algebra. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Kousha Etessami |
Stutter-Invariant Languages, omega-Automata, and Temporal Logic. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Béatrice Bérard, Laurent Fribourg |
Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | David L. Dill |
Alternative Approaches to Hardware Verification (abstract). |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Per Bjesse |
Automatic Verification of Combinatorial and Pipelined FFT. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli |
Latency Insensitive Protocols. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | John Matthews, John Launchbury |
Elementary Microarchitecture Algebra. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle |
TIPPtool: Compositional Specification and Analysis of Markovian Performance Models. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Sifakis |
The Compositional Specification of Timed Systems - A Tutorial. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Kavita Ravi, Fabio Somenzi |
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi |
Improved Automata Generation for Linear Temporal Logic. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Kupferman, Moshe Y. Vardi |
Model Checking of Safety Properties. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | S. Ramesh 0001, Purandar Bhaduri |
Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcelo Glusman, Shmuel Katz |
Mechanizing Proofs of Computation Equivalence. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
Deciding Equality Formulas by Small Domains Instantiations. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Hassen Saïdi, Natarajan Shankar |
Abstract and Model Check While You Prove. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Alur |
Timed Automata. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri |
NUSMV: A New Symbolic Model Verifier. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
Assume-Guarantee Refinement Between Different Time Scales. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Marius Bozga, Oded Maler |
On the Representation of Probabilities over Structured Domains. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Kedar S. Namjoshi, Robert P. Kurshan |
Efficient Analysis of Cyclic Definitions. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers |
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Buchholz 0001, Peter Kemper |
A Toolbox for the Analysis of Discrete Event Dynamic Systems. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Ed Brinksma |
Formal Methods for Conformance Testing: Theory Can Be Practical. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Satyaki Das, David L. Dill, Seungjoon Park |
Experience with Predicate Abstraction. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech |
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Glenn Bruns, Patrice Godefroid |
Model Checking Partial State Spaces with 3-Valued Temporal Logics. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu |
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, Masahiro Fujita |
Model Checking Based on Sequential ATPG. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Halbwachs, Doron A. Peled (eds.) |
Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Ching-Tsun Chou |
The Mathematical Foundation fo Symbolic Trajectory Evaluation. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, Wang Yi 0001 |
Efficient Timed Reachability Analysis Using Clock Difference Diagrams. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thierry Jéron, Pierre Morel |
Test Generation Derived from Model-Checking. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
You Assume, We Guarantee: Methodology and Case Studies. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Ilan Beer, Shoham Ben-David, Avner Landver |
On-the-Fly Model Checking of RCTL Formulas. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Raphaël Couturier, Dominique Méry |
An Experiment in Parallelizing an Application Using Formal Methods. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Douglas J. Howe, Frank A. Stomp |
Protocol Verification in Nuprl. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Anuj Goel, Khurram Sajid, Hai Zhou 0001, Adnan Aziz, Vigyan Singhal |
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas R. Shiple, James H. Kukula, Rajeev K. Ranjan 0001 |
A Comparison of Presburger Engines for EFSM Reachability. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jun Sawada, Warren A. Hunt Jr. |
Processor Verification with Precise Exeptions and Speculative Execution. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jayram S. Thathachar |
On the Limitations of Ordered Representations of Functions. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacob Elgaard, Nils Klarlund, Anders Møller |
MONA 1.x: New Techniques for WS1S and WS2S. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Bolignano |
Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Wallner |
Model Checking LTL Using Net Unforldings. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Scott D. Stoller, Yanhong A. Liu |
Efficient Symbolic Detection of Global Properties in Distributed Systems. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan J. Hu, Moshe Y. Vardi (eds.) |
Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Amar Bouali |
XEVE, an ESTEREL Verification Environment. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | J Strother Moore |
An ACL2 Proof of Write Invalidate Cache Coherence. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Saddek Bensalem, Yassine Lakhnech, Sam Owre |
InVeST: A Tool for the Verification of Invariants. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | John C. Mitchell |
Finite-State Analysis of Security Protocols. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan |
The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jens U. Skakkebæk, Robert B. Jones, David L. Dill |
Formal Verification of Out-of-Order Execution Using Incremental Flushing. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson 0001 |
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Udo Brockmeyer, Gunnar Wittich |
Real-Time Verification of Statemate Designs. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Conrado Daws |
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Jorge Cuéllar |
Formal Methods in an Industrial Environment. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license