default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID11th CAV 1999: Trento, Italy
- Nicolas Halbwachs, Doron A. Peled:
Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science 1633, Springer 1999, ISBN 3-540-66202-2
Tutorials and Invited Papers
- David L. Dill:
Alternative Approaches to Hardware Verification (abstract). 1 - Joseph Sifakis:
The Compositional Specification of Timed Systems - A Tutorial. 2-7 - Rajeev Alur:
Timed Automata. 8-22 - Zohar Manna, Henny Sipma:
Verification of Parameterized Systems by Dynamic Induction on Diagrams. 25-41 - Ed Brinksma:
Formal Methods for Conformance Testing: Theory Can Be Practical. 44-45
Processor Verification
- Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu:
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. 60-71 - Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz:
Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists. 72-83 - S. Ramesh, Purandar Bhaduri
:
Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study. 84-95
Protocol Verification and Testing
- Béatrice Bérard, Laurent Fribourg:
Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. 96-107 - Thierry Jéron, Pierre Morel:
Test Generation Derived from Model-Checking. 108-121 - Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli:
Latency Insensitive Protocols. 123-133
Infinite State Space
- Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson:
Handling Global Conditions in Parameterized System Verification. 134-145 - Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech:
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. 146-159 - Satyaki Das, David L. Dill, Seungjoon Park:
Experience with Predicate Abstraction. 160-171
Theory of Verification
- Orna Kupferman, Moshe Y. Vardi:
Model Checking of Safety Properties. 172-183 - Rom Langerak, Ed Brinksma:
A Complete Finite Prefix for Process Algebra. 184-195 - Ching-Tsun Chou:
The Mathematical Foundation fo Symbolic Trajectory Evaluation. 196-207 - Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
Assume-Guarantee Refinement Between Different Time Scales. 208-221
Linear Temporal Logic
- Roderick Bloem, Kavita Ravi, Fabio Somenzi:
Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. 222-235 - Kousha Etessami:
Stutter-Invariant Languages, omega-Automata, and Temporal Logic. 236-248 - Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi:
Improved Automata Generation for Linear Temporal Logic. 249-260
Modeling of Systems
- Marius Bozga, Oded Maler:
On the Representation of Probabilities over Structured Domains. 261-273 - Glenn Bruns, Patrice Godefroid:
Model Checking Partial State Spaces with 3-Valued Temporal Logics. 274-287 - John Matthews, John Launchbury:
Elementary Microarchitecture Algebra. 288-300 - Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. 301-315
Symbolic Model-Checking
- Jørn Lind-Nielsen, Henrik Reif Andersen:
Stepwise CTL Model Checking of State/Event Systems. 316-327 - Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron:
Optimizing Symbolic Model Checking for Constraint-Rich Models. 328-340 - Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, Wang Yi:
Efficient Timed Reachability Analysis Using Clock Difference Diagrams. 341-353
Theorem Proving
- Marcelo Glusman, Shmuel Katz:
Mechanizing Proofs of Computation Equivalence. 354-367 - Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers:
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. 369-379 - Per Bjesse:
Automatic Verification of Combinatorial and Pipelined FFT. 380-393
Automata-Theoretic Methods
- Kedar S. Namjoshi, Robert P. Kurshan:
Efficient Analysis of Cyclic Definitions. 394-405 - Nils Klarlund:
A Theory of Restrictions for Logics and Automata. 406-417 - Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, Masahiro Fujita:
Model Checking Based on Sequential ATPG. 418-430 - Marc Spielmann:
Automatic Verification of Abstract State Machines. 431-442
Abstraction
- Hassen Saïdi, Natarajan Shankar:
Abstract and Model Check While You Prove. 443-454 - Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel:
Deciding Equality Formulas by Small Domains Instantiations. 455-469 - Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. 470-482
Tool Presentations
- Peter Buchholz, Peter Kemper:
A Toolbox for the Analysis of Discrete Event Dynamic Systems. 483-486 - Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle:
TIPPtool: Compositional Specification and Analysis of Markovian Performance Models. 487-490 - David A. Basin, Stefan Friedrich, Joachim Posegga, Harald Vogt:
Java Bytecode Verification by Model Checking. 491-494 - Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri:
NUSMV: A New Symbolic Model Verifier. 495-499 - Johann Schumann:
PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. 500-504
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-20 21:06 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
