Übersicht			Auf mobile öffnen

Lieferstatus:	i.d.R. innert 5-10 Tagen versandfertig
Veröffentlichung:	September 1999
Genre:	EDV / Informatik
	formalspecification / formalverification / Hardwaredesign / higher-orderlogics / Künstliche Intelligenz (KI) / Logikprogrammierung / Mathematische und statistische Software / proving / Software Engineering / theoremproving / Theoretische Informatik / Verification mehr...
ISBN:	9783540664635
EAN-Code:	9783540664635
Verlag:	Springer
Einband:	Kartoniert
Sprache:	English
Dimensionen:	H 235 mm / B 155 mm / D 21 mm
Gewicht:	563 gr
Seiten:	372
Bewertung:	Titel bewerten / Meinung schreiben

Inhalt:

Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage.- Disjoint Sums over Type Classes in HOL.- Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.- Isomorphisms - A Link Between the Shallow and the Deep.- Polytypic Proof Construction.- Recursive Function Definition over Coinductive Types.- Hardware Verification Using Co-induction in COQ.- Connecting Proof Checkers and Computer Algebra Using OpenMath.- A Machine-Checked Theory of Floating Point Arithmetic.- Universal Algebra in Type Theory.- Locales A Sectioning Concept for Isabelle.- Isar - A Generic Interpretative Approach to Readable Formal Proof Documents.- On the Implementation of an Extensible Declarative Proof Language.- Three Tactic Theorem Proving.- Mechanized Operational Semantics via (Co)Induction.- Representing WP Semantics in Isabelle/ZF.- A HOL Conversion for Translating Linear Time Temporal Logic to ?-Automata.- From I/O Automata to Timed I/O Automata.- Formal Methods and Security Evaluation.- Importing MDG Verification Results into HOL.- Integrating Gandalf and HOL.- Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.- Symbolic Functional Evaluation.