Computer-aided reasoning : ACL2 case studies Matt Kaufmann; Panagiotis Manolios; J Strother Moore

By:

Kaufmann, Matt

Contributor(s):

Material type: Text

TextLanguage: English Publication details: New York: Springer Science+Business Media 2000.Description: xi, 337 p. 24 cmISBN:

9781441949813

Subject(s):

DDC classification:

006.33 KAU

Contents:

An exercise in graph theory / J Strother Moore -- Modular proof : the fundamental theorem of calculus / Matt Kaufmann -- Mu-calculus model-checking / Panagiotis Manolios -- High-speed, analyzable simulators / David Greve, Matthew Wilding, and David Hardin -- Verification of a simple pipelined machine model / Jun Sawada -- The DE language / Warren A. Hunt, Jr. -- Using macros to mimic VHDL / Dominique Borrione, Philippe Georgelin, and Vanderlei Rodrigues -- Symbolic trajectory evaluation / Damir A. Jamsek -- RTL verification : a floating-point multiplier / David M. Russinoff and Arthur Flatau -- Design verification of a safety-critical embedded verifier / Piergiorgio Bertoli and Paolo Traverso -- Compiler verification revisited / Wolfgang Goerigk -- Ivy : a preprocessor and proof checker for first-order logic / William McCune and Olga Shumsky -- Knuth's generalization of McCarthy's 91 function / John Cowles -- Continuity and differentiability / Ruben Gamboa.

Tags from this library: No tags from this library for this title. Log in to add tags.

Average rating: 0.0 (0 votes)

Holdings
Item type	Current library	Collection	Call number	Status	Date due	Barcode
General Books	CUTN Central Library Generalia	Non-fiction	006.33 KAU (Browse shelf(Opens below))	Available		29937

An exercise in graph theory / J Strother Moore --
Modular proof : the fundamental theorem of calculus / Matt Kaufmann --

Mu-calculus model-checking / Panagiotis Manolios --

High-speed, analyzable simulators / David Greve, Matthew Wilding, and David Hardin --
Verification of a simple pipelined machine model / Jun Sawada --
The DE language / Warren A. Hunt, Jr. --

Using macros to mimic VHDL / Dominique Borrione, Philippe Georgelin, and Vanderlei Rodrigues --
Symbolic trajectory evaluation / Damir A. Jamsek --

RTL verification : a floating-point multiplier / David M. Russinoff and Arthur Flatau --

Design verification of a safety-critical embedded verifier / Piergiorgio Bertoli and Paolo Traverso --

Compiler verification revisited / Wolfgang Goerigk --

Ivy : a preprocessor and proof checker for first-order logic / William McCune and Olga Shumsky --

Knuth's generalization of McCarthy's 91 function / John Cowles --
Continuity and differentiability / Ruben Gamboa.

There are no comments on this title.

to post a comment.