Search results for "PVS"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
11	Joe Hurd	Predicate Subtyping with Predicate Sets.	TPHOLs	2001	DBLP DOI BibTeX RDF
11	Natarajan Shankar	Using Decision Procedures with a Higher-Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
11	Joseph E. Stoy, Xiaowei Shen, Arvind	Proofs of Correctness of Cache-Coherence Protocols.	FME	2001	DBLP DOI BibTeX RDF
11	Bart Jacobs 0001	A Formalisation of Java's Exception Mechanism.	ESOP	2001	DBLP DOI BibTeX RDF
11	Ulrich Hannemann, Jozef Hooman	Formal Design of Real-Time Components on a Shared Data Space Architecture.	COMPSAC	2001	DBLP DOI BibTeX RDF
11	Kenneth L. McMillan	Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking.	CHARME	2001	DBLP DOI BibTeX RDF
11	Christoph Berg, Christian Jacobi 0002	Formal Verification of the VAMP Floating Point Unit.	CHARME	2001	DBLP DOI BibTeX RDF
11	Vangalur S. Alagar, Qiaoyun Li, Olga Ormandjieva	Assessment of Maintainability in Object-Oriented Software.	TOOLS (39)	2001	DBLP DOI BibTeX RDF	design complexity measurement, software maintenance, information theory, object-oriented software, software maintainability
11	Axel Dold, Vincent Vialard	A Mechanically Verified Compiling Specification for a Lisp Compiler.	FSTTCS	2001	DBLP DOI BibTeX RDF
11	Neeraj Jaggi, K. Gopinath	Verification of a Leader Election Algorithm in Timed Asynchronous Systems.	FSTTCS	2001	DBLP DOI BibTeX RDF
11	Natarajan Shankar	Static Analysis for Safe Destructive Updates in a Functional Language.	LOPSTR	2001	DBLP DOI BibTeX RDF
11	Bart Jacobs 0001, Erik Poll	A Logic for the Java Modeling Language JML.	FASE	2001	DBLP DOI BibTeX RDF
11	Edwin D. de Jong, Jaco van de Pol, Jozef Hooman	Refinement in Requirements Specification and Analysis: A Case Study.	ECBS	2000	DBLP DOI BibTeX RDF	requirements specification and analysis, formal methods, refinement, theorem provers
11	Kurt Lichtner, Paulo S. C. Alencar, Donald D. Cowan	A Framework for Software Architecture Verification.	Australian Software Engineering Conference	2000	DBLP DOI BibTeX RDF	formal modeling, architecture description languages (ADLs), higher-order logic, Software architecture analysis
11	Dmitri Chkliaev, Jozef Hooman, Peter van der Stok	Mechanical Verification of Transaction Processing Systems.	ICFEM	2000	DBLP DOI BibTeX RDF
11	Abdel Mokkedem, Tim Leonard	Formal Verification of the Alpha 21364 Network Protocol.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Victor Carreño, César A. Muñoz	Aircraft Trajectory Modeling and Altering Algorithm Verification.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Marieke Huisman, Bart Jacobs 0001	Inheritance in Higher Order Logic: Modeling and Reasoning.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Mamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec, Xavier Thirioux	Refinement Based Validation of an Algorithm for Detecting Distributed Termination.	IPDPS Workshops	2000	DBLP DOI BibTeX RDF
11	Tamarah Arons, Amir Pnueli	A Comparison of Two Verification Methods for Speculative Instruction Execution.	TACAS	2000	DBLP DOI BibTeX RDF
11	Joachim van den Berg, Bart Jacobs 0001, Erik Poll	Formal Specification and Verification of JavaCard's Application Identifier Class.	Java Card Workshop	2000	DBLP DOI BibTeX RDF
11	Marieke Huisman, Bart Jacobs 0001	Java Program Verification via a Hoare Logic with Abrupt Termination.	FASE	2000	DBLP DOI BibTeX RDF
11	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
11	Nazanin Mansouri, Ranga Vemuri	Accounting for Various Register Allocation Schemes During Post-Synthesis Verification of RTL Designs.	DATE	1999	DBLP DOI BibTeX RDF
11	John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou	A Formalization of Software Architecture.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
11	Richard Verhoeven, Roland Carl Backhouse	Interfacing Program Construction and Verification.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
11	Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen	Divide, Abstract, and Model-Check.	SPIN	1999	DBLP DOI BibTeX RDF
11	Jason Hickey	Fault-Tolerant Distributed Theorem Proving.	CADE	1999	DBLP DOI BibTeX RDF
11	Andrew A. Adams, Hanne Gottliebsen, Steve Linton, Ursula Martin	VSDITLU: a verifiable symbolic definite integral table look-up.	CADE	1999	DBLP DOI BibTeX RDF
11	David Spelt, Susan Even	A Theorem Prover-Based Analysis Tool for Object-Oriented Databases.	TACAS	1999	DBLP DOI BibTeX RDF
11	Douglas J. Howe	Interactive Theorem Proving Using Type Theory.	CSL	1999	DBLP DOI BibTeX RDF
11	James Kirby, Myla Archer, Constance L. Heitmeyer	SCR: A Practical Approach to Building a High Assurance COMSEC System.	ACSAC	1999	DBLP DOI BibTeX RDF
11	Raphaël Couturier, Dominique Méry	An Experiment in Parallelizing an Application Using Formal Methods.	CAV	1998	DBLP DOI BibTeX RDF
11	W. O. David Griffioen, Frits W. Vaandrager	Normed Simulations.	CAV	1998	DBLP DOI BibTeX RDF
11	Bart Jacobs 0001, Joachim van den Berg, Marieke Huisman, Martijn van Berkum	Reasoning about Java Classes (Preliminary Report).	OOPSLA	1998	DBLP DOI BibTeX RDF	Java
11	Paul B. Jackson	Verifying a Garbage Collection Algorithm.	TPHOLs	1998	DBLP DOI BibTeX RDF
11	Hussein Zedan, Hongji Yang	A Sound and Practical Approach To The Re-Engineering Of Time-Critical Systems.	CSMR	1998	DBLP DOI BibTeX RDF
11	Frank Pfenning, Carsten Schürmann	Algorithms for Equality and Unification in the Presence of Notational Definitions.	TYPES	1998	DBLP DOI BibTeX RDF
11	Amir Pnueli	Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk).	CADE	1998	DBLP DOI BibTeX RDF
11	Detlef Schwier, Friedrich W. von Henke	Mechanical Verification of Clock Synchronization Algorithms.	FTRTFT	1998	DBLP DOI BibTeX RDF
11	Amir Pnueli, Tamarah Arons	Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study.	FMCAD	1998	DBLP DOI BibTeX RDF
11	Abdelillah Mokkedem, Ravi Hosabettu, Ganesh Gopalakrishnan	Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem.	FMCAD	1998	DBLP DOI BibTeX RDF
11	Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu	Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.	FMCAD	1998	DBLP DOI BibTeX RDF
11	Bruno Dutertre, Victoria Stavridou	Formal Requirements Analysis of an Avionics Control System.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	Formal specification, formal verification, requirements analysis, safety critical systems, avionics systems
11	William D. Young	Comparing Verification Systems: Interactive Consistency in ACL2.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	fault tolerance, Formal verification, specification languages, computational logic, automatic theorem proving
11	Marco Devillers, W. O. David Griffioen, Olaf Müller	Possibly Infinite Sequences in Theorem Provers: A Comparative Study.	TPHOLs	1997	DBLP DOI BibTeX RDF
11	Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß	Formal Verification of Transformations for Peephole Optimization.	FME	1997	DBLP DOI BibTeX RDF	reusability of specifications, formal verification, transformations, higher-order logic
11	Jozef Hooman	Compositional Verification of Real-Time Applications.	COMPOS	1997	DBLP DOI BibTeX RDF
11	Susanne Graf, Hassen Saïdi	Verifying Invariants Using theorem Proving.	CAV	1996	DBLP DOI BibTeX RDF
11	Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch	Automated Verification by Induction with Associative-Commutative Operators.	CAV	1996	DBLP DOI BibTeX RDF
11	Frank S. de Boer, M. van Hulst	Local Nondeterminism in Asynchronously Communicating Processes.	FME	1996	DBLP DOI BibTeX RDF
11	Ben L. Di Vito	Formalizing New Navigation Requirements for NASA's Space Shuttle.	FME	1996	DBLP DOI BibTeX RDF
11	T. C. Nicholas Graham	A Method for The Formal Testing of Program Visualization Tools.	WPC	1996	DBLP DOI BibTeX RDF	Software Architecture Languages, Formal Methods, Visual Programming Environments
11	Jiang Yu Zheng, Saburo Tsuji	Panoramic representation for route recognition by a mobile robot.	Int. J. Comput. Vis.	1992	DBLP DOI BibTeX RDF