3 résultat(s) recherche sur le mot-clé 'program verification'

Interactive theorem proving and program development / Bertot, Yves

Public ISBD Titre : Interactive theorem proving and program development : Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohrin Type de document : texte imprimé Auteurs : Bertot, Yves ; Castéran, Pierre Editeur : Springer-Verlag Année de publication : 2004 Collection : Texts in Theoretical Computer Science. An EATCS Series Importance : xxv - 469 p. ISBN/ISSN/EAN : 978-3-540-20854-9 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : type theory  theorem proving  proof assistant  program verification  coq Index. décimale : 68C Monographie Interactive theorem proving and program development : Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohrin [texte imprimé] / Bertot, Yves ; Castéran, Pierre . - [S.l.] : Springer-Verlag, 2004 . - xxv - 469 p. . - (Texts in Theoretical Computer Science. An EATCS Series) . ISBN : 978-3-540-20854-9 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : type theory  theorem proving  proof assistant  program verification  coq Index. décimale : 68C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
16714	68C305	imprimé / autre	CRDM	68/INFORMATIQUE	Disponible

Logic in computer science. Modelling and reasoning about systems / Michael Huth

Public ISBD Titre : Logic in computer science. Modelling and reasoning about systems Type de document : texte imprimé Auteurs : Michael Huth, Auteur ; Mark Ryan, Auteur Mention d'édition : 2nd ed. Editeur : Cambridge : Cambridge University Press Année de publication : 2004 Importance : xiv - 427 p. ISBN/ISSN/EAN : 978-0-521-54310-1 Note générale : commande M. Borer Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 68-XX Computer science :68-01 Instructional exposition (textbooks, tutorial papers, etc.) Mots-clés : contract-programming paradigm  program verification  model checking  object modeling  predicate logic  propositional logic  sat solver  natural deduction Index. décimale : 68C Monographie Logic in computer science. Modelling and reasoning about systems [texte imprimé] / Michael Huth, Auteur ; Mark Ryan, Auteur  . -  2nd ed. . - Cambridge : Cambridge University Press, 2004 . - xiv - 427 p. ISBN : 978-0-521-54310-1 commande M. Borer Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 68-XX Computer science :68-01 Instructional exposition (textbooks, tutorial papers, etc.) Mots-clés : contract-programming paradigm  program verification  model checking  object modeling  predicate logic  propositional logic  sat solver  natural deduction Index. décimale : 68C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
17769	68C340	imprimé / autre	CRDM	68/INFORMATIQUE	Disponible

Programming for computations - Python / Svein Linge

Public ISBD Titre : Programming for computations - Python : a gentle introduction to numerical simulations with Python Type de document : texte imprimé Auteurs : Svein Linge, Auteur ; Hans Petter Langtangen, Auteur Editeur : Springer-Verlag Année de publication : 2016 Collection : Texts in Computational Science and Engineering num. 15 Importance : xvi - 232 p. ISBN/ISSN/EAN : 978-3-319-32428-9 Note générale : Catégories : 68-XX Computer science :68-01 Instructional exposition (textbooks, tutorial papers, etc.) Mots-clés : interactive programming  program verification  numerical integration  numerical solution of differential equations Index. décimale : LAREMA Programming for computations - Python : a gentle introduction to numerical simulations with Python [texte imprimé] / Svein Linge, Auteur ; Hans Petter Langtangen, Auteur . - [S.l.] : Springer-Verlag, 2016 . - xvi - 232 p.. - (Texts in Computational Science and Engineering; 15) . ISBN : 978-3-319-32428-9 Catégories : 68-XX Computer science :68-01 Instructional exposition (textbooks, tutorial papers, etc.) Mots-clés : interactive programming  program verification  numerical integration  numerical solution of differential equations Index. décimale : LAREMA

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
30188	LAREMA/LIN	imprimé / autre	Fédération FR 2962 - Angers	Angers Ouvrages	Disponible