Theorem Proving in Higher Order Logics
Editat de Joe Hurd, Tom Melhamen Limba Engleză Paperback – 8 aug 2005
Preț: 328.49 lei
Preț vechi: 410.62 lei
-20%
Puncte Express: 493
Carte tipărită la comandă
Livrare economică 24 iulie-07 august
Livrare prin curier în România Termenul estimat este afișat lângă disponibilitate.
Transport gratuit de la 400.00 lei Plată online sau ramburs, în funcție de opțiunile comenzii.
Retur gratuit în 14 zile Comandă securizată și suport în română.
Specificații
ISBN-13: 9783540283720
ISBN-10: 3540283722
Pagini: 424
Ilustrații: X, 414 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540283722
Pagini: 424
Ilustrații: X, 414 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Invited Papers.- On the Correctness of Operating System Kernels.- Alpha-Structural Recursion and Induction.- Regular Papers.- Shallow Lazy Proofs.- Mechanized Metatheory for the Masses: The PoplMark Challenge.- A Structured Set of Higher-Order Problems.- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS.- Proving Equalities in a Commutative Ring Done Right in Coq.- A HOL Theory of Euclidean Space.- A Design Structure for Higher Order Quotients.- Axiomatic Constructor Classes in Isabelle/HOLCF.- Meta Reasoning in ACL2.- Reasoning About Java Programs with Aliasing and Frame Conditions.- Real Number Calculations and Theorem Proving.- Verifying a Secure Information Flow Analyzer.- Proving Bounds for Real Linear Programs in Isabelle/HOL.- Essential Incompleteness of Arithmetic Verified by Coq.- Verification of BDD Normalization.- Extensionality in the Calculus of Constructions.- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.- A Generic Network on Chip Model.- Formal Verification of a SHA-1 Circuit Core Using ACL2.- From PSL to LTL: A Formal Validation in HOL.- Proof Pearls.- Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2.- Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2.- Proof Pearl: Defining Functions over Finite Sets.- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.