Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Matt Kaufmann, Andrew Martin, Carl Pixley |
Design Constraints in Symbolic Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Adrian J. Isles, Ramin Hojati, Robert K. Brayton |
Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Gian-Luigi Ferrari 0002, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori |
Verifying Mobile Processes in the HAL Environment. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Hubert Comon, Yan Jurski |
Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed |
Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | David S. Hardin, Matthew Wilding, David A. Greve |
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Parosh Aziz Abdulla, Bengt Jonsson 0001, Mats Kindahl, Doron A. Peled |
A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract). |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran |
MOCHA: Modularity in Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Ulrich Stern, David L. Dill |
Using Magnatic Disk Instead of Main Memory in the Murphi Verifier. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Doron A. Peled |
A Toolset for Message Sequence Charts. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Gerard J. Holzmann |
On Checking Model Checkers. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Wendy Belluomini, Chris J. Myers |
Verification of Timed Systems Using POSETs. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | E. Allen Emerson, Kedar S. Namjoshi |
Verification of Parameterized Bus Arbitration Protocol. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Nicolas Halbwachs |
Synchronous Programming of Reactive Systems. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Yirng-An Chen, Randal E. Bryant |
Verification of Floating-Point Adders. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Albert John Camilleri |
A Role for Theorem Proving in Multi-Processor Design. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Wolper, Bernard Boigelot |
Verifying Systems with Infinite but Regular State Spaces. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | John Hoffman, Charlie Payne |
A Formal Method Experience at Secure Computing Corporation. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan |
Decomposing the Proof of Correctness of pipelined Microprocessors. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla |
Symmetry Reductions in Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Matthew Wilding |
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Saddek Bensalem, Yassine Lakhnech, Sam Owre |
Computing Abstractions of Infinite State Systems Compositionally and Automatically. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Michael Colón, Tomás E. Uribe |
Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Felice Balarin |
Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | W. O. David Griffioen, Frits W. Vaandrager |
Normed Simulations. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Giampaolo Bella, Lawrence C. Paulson |
Mechanising BAN Kerberos by the Inductive Method. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Doron A. Peled |
Ten Years of Partial Order Reduction. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Gurmeet Singh Manku, Ramin Hojati, Robert K. Brayton |
Structural Symmetry and Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj |
SCR*: A Toolset for Specifying and Analyzing Software Requirements. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer |
From Pre-historic to Post-modern Symbolic Model Checking. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine |
Kronos: A Model-Checking Tool for Real-Time Systems. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Bernard Boigelot, Louis Bronne, Stéphane Rassart |
An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract). |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Christel Baier, Holger Hermanns |
Weak Bisimulation for Fully Probabilistic Processes. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | A. Prasad Sistla, L. Miliades, Viktor Gyuris |
SMC: A Symmetry Based Model Checker for Verification of Liveness Properties. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Moshe Y. Vardi |
Module Checking Revisited. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | F. Erich Marschner |
Practical Challenges for Industrial Formal Verification Tools. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Armin Biere |
µcke - Efficient µ-Calculus Model Checking. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | William Chan 0001, Richard J. Anderson, Paul Beame, David Notkin |
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal |
RuleBase: Model Checking at IBM. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Susanne Graf, Hassen Saïdi |
Construction of Abstract State Graphs with PVS. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
state graph exploration, theorem proving, abstract interpretation |
1 | Hassen Saïdi |
The Invariant Checker: Automated Deductive Verification of Reactive Systems. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Kim Guldstrand Larsen, Paul Pettersson, Wang Yi 0001 |
UPPAAL: Status & Developments. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Bernd Grahlmann |
The PEP Tool. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
B(PN)2, Stubborn sets, Simulation, Model checking, Petri nets, Temporal logic, Tool, Binary decision diagrams, PEP |
1 | David Harel |
Some Thoughts on Statecharts, 13 Years Later. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Serdar Tasiran, Robert K. Brayton |
STARI: A Case Study in Compositional and Hierarchical Timing Verification. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Bolignano |
Towards a Mechanization of Cryptographic Protocal Verification. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Kathi Fisler |
Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
Partial-Order Reduction in Symbolic State Space Exploration. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Barrett, Anthony McIsaac |
Model Checking in a Microprocessor Design Project. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
Symbolic Model Checking with Rich ssertional Languages. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Y. S. Ramakrishna, C. R. Ramakrishnan 0001, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren |
Efficient Model Checking Using Tabled Resolution. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Viktor Gyuris, A. Prasad Sistla |
On-the-Fly Model Checking Under Fairness That Exploits Symmetry. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius |
prod 3.2: An Advanced Tool for Efficient Reachability Analysis. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Jun Sawada, Warren A. Hunt Jr. |
Trace Table Based Approach for Pipeline Microprocessor Verification. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | David Cyrluk, M. Oliver Möller, Harald Rueß |
An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine |
Some Progress in the Symbolic Verification of Timed Automata. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Gérard Berry |
Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Melzer, Stefan Römer |
Deadlock Checking Using Net Unfoldings. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ilkka Kokkarinen, Doron A. Peled, Antti Valmari |
Relaxed Visibility Enhances Partial Order Reduction. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Arne Borälv |
The Industrial Success of Verification Tools Based on Stålmarck's Method. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
A Compositional Rule for Hardware Design Refinement. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Miroslav N. Velev, Randal E. Bryant, Alok Jain |
Efficient Modeling of Memory Arrays in Symbolic Simulation. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | A. Prasad Sistla |
Parametrized Verification of Linear Networks Using Automata as Invariants. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh |
Efficient Detection of Vacuity in ACTL Formulaas. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Neil Immerman, Moshe Y. Vardi |
Model Checking and Transitive-Closure Logic. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Gérard Cécé, Alain Finkel |
Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract). |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik |
TermiLog: A System for Checking Termination of Queries to Logic Programs. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Orna Grumberg (eds.) |
Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu |
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Martin Rowe |
Formal Verification - Applications & Case Studies. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Adam L. Turk, Scott T. Probst, Gary J. Powers |
Verification of a Chemical Process Leak Test Procedure. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Jun Yuan 0007, Jian Shen, Jacob A. Abraham, Adnan Aziz |
On Combining Formal and Informal Verification. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi |
HYTECH: A Model Checker for Hybrid Systems. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger |
MOSEL: A Sound and Efficient Tool for M2L(Str). |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Manish Pandey, Randal E. Bryant |
Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Gila Kamhi, Osnat Weissberg, Limor Fix |
Automatic Datapath Extraction for Efficient Usage of HDD. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Roope Kaivola |
Using Compositional Preorders in the Verification of Sliding Window Protocal. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ulrich Stern, David L. Dill |
Parallelizing the Murphi Verifier. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Tevfik Bultan, Richard Gerber 0001, William W. Pugh |
Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea |
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Nils Klarlund |
An n log n Algorithm for Online BDD Refinement. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Roger B. Hughes |
Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Patrice Godefroid |
VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Abelardo Pardo, Gary D. Hachtel |
Automatic Abstraction Techniques for Propositional µ-calculus Model Checking. |
CAV |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Stavros Tripakis, Sergio Yovine |
Analysis of Timed Systems Based on Time-Abstracting Bisimulation. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi 0001 |
Verification of an Audio Protocol with Bus Collision Using UPPAAL. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Claude Fernandez, Claude Jard, Thierry Jéron, César Viho |
Using On-The-Fly Verification Techniques for the Generation of test Suites. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Rance Cleaveland, Steve Sims |
The NCSU Concurrency Workbench. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Igor Walukiewicz |
Pushdown Processes: Games and Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert K. Brayton |
Verifying Continuous Time Markov Chains. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | E. Pascal Gribomont |
Atomicity Refinement and Trace Reduction Theorems. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | George S. Avrunin |
Symbolic Model Checking Using Algebraic Geometry. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Moshe Y. Vardi |
Module Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun |
The METAFrame'95 Environment. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Kenneth L. McMillan |
A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | C. Norris Ip, David L. Dill |
Verifying Systems with Replicated Components in Murphi. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Duncan Clarke, Hanêne Ben-Abdallah, Insup Lee 0001, Hong-liang Xie, Oleg Sokolsky |
XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Systems. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Sérgio Vale Aguiar Campos, Orna Grumberg |
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Mark R. Greenstreet |
Verifying Safety Properties of Differential Equations. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|