Search results for "CAV"

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

Publications at "CAV"( http://dblp.L3S.de/Venues/CAV )