Search results for "Nqthm"

Found 14 publication records. Showing 14 according to the selection in the facets

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
66	Matt Kaufmann, J Strother Moore	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions
55	Robert S. Boyer, Yuan Yu	Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor.	CADE	1992	DBLP DOI BibTeX RDF	Nqthm, Boyer-Moore Theorem Prover, Gnu, Ada, C, Automated reasoning, object code, formal program verification
44	Christoph Walther	Computing Induction Axioms.	LPAR	1992	DBLP DOI BibTeX RDF
42	David M. Goldschlag	A Mechanization of Unity in PC-NQTHM-92.	J. Autom. Reason.	1999	DBLP DOI BibTeX RDF
42	Michel Allemand, Felix Nicoli, Laurence Pierre	Formal Verification of Hardware using LP and Comparison with Nqthm.	Applied Informatics	1994	DBLP BibTeX RDF
33	Robert S. Boyer, Yuan Yu	Automated Proofs of Object Code for a Widely Used Microprocessor.	J. ACM	1996	DBLP DOI BibTeX RDF	Boyer-Moore logic, MC68xxx, Nqthm, program proving, formal methods, Ada, C, program verification, automated reasoning, Common Lisp, mechanical theorem proving, object code, machine code
22	Wim H. Hesselink	An assertional proof for a construction of an atomic variable.	Formal Aspects Comput.	2004	DBLP DOI BibTeX RDF	Invariant, Atomicity, Wait-free, Safeness
22	Eric Gascard, Laurence Pierre	Induction-Oriented Formal Verification in Symmetric Interconnection Networks.	CHARME	2001	DBLP DOI BibTeX RDF
22	Wim H. Hesselink	The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Message passing, Theorem proving, Minimum spanning tree, Asynchronous communication
22	Matthew Wilding	A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy.	CAV	1998	DBLP DOI BibTeX RDF
22	Denis Lugiez	A Good Class of Tree Automata and Application to Inductive Theorem Proving.	ICALP	1998	DBLP DOI BibTeX RDF
22	Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch	Automated Verification by Induction with Associative-Commutative Operators.	CAV	1996	DBLP DOI BibTeX RDF
22	Matthew Wilding	A Mechanically Verified Application for a Mechanically Verified Environment.	CAV	1993	DBLP DOI BibTeX RDF
22	Robert S. Boyer, J Strother Moore	A Theorem Prover for a Computational Logic.	CADE	1990	DBLP DOI BibTeX RDF