close
1.

図書

図書
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
出版情報: Berlin : Springer, c2002  xiii, 218 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2283
所蔵情報: loading…
目次情報: 続きを見る
Elementary Techniques / Part I:
The Basics / 1:
Introduction / 1.1:
Theories / 1.2:
Types, Terms, and Formulae / 1.3:
Variables / 1.4:
Interaction and Interfaces / 1.5:
Getting Started / 1.6:
Functional Programming in HOL / 2:
An Introductory Theory / 2.1:
An Introductory Proof / 2.2:
Some Helpful Commands / 2.3:
Datatypes / 2.4:
Lists / 2.4.1:
The General Format / 2.4.2:
Primitive Recursion / 2.4.3:
Case Expressions / 2.4.4:
Structural Induction and Case Distinction / 2.4.5:
Case Study: Boolean Expressions / 2.4.6:
Some Basic Types / 2.5:
Natural Numbers / 2.5.1:
Pairs / 2.5.2:
Datatype option / 2.5.3:
Definitions / 2.6:
Type Synonyms / 2.6.1:
Constant Definitions / 2.6.2:
The Definitional Approach / 2.7:
More Functional Programming / 3:
Simplification / 3.1:
What Is Simplification? / 3.1.1:
Simplification Rules / 3.1.2:
The simp Method / 3.1.3:
Adding and Deleting Simplification Rules / 3.1.4:
Assumptions / 3.1.5:
Rewriting with Definitions / 3.1.6:
Simplifying let-Expressions / 3.1.7:
Conditional Simplification Rules / 3.1.8:
Automatic Case Splits / 3.1.9:
Tracing / 3.1.10:
Induction Heuristics / 3.2:
Case Study: Compiling Expressions / 3.3:
Advanced Datatypes / 3.4:
Mutual Recursion / 3.4.1:
Nested Recursion / 3.4.2:
The Limits of Nested Recursion / 3.4.3:
Case Study: Tries / 3.4.4:
Total Recursive Functions / 3.5:
Defining Recursive Functions / 3.5.1:
Proving Termination / 3.5.2:
Simplification and Recursive Functions / 3.5.3:
Induction and Recursive Functions / 3.5.4:
Presenting Theories / 4:
Concrete Syntax / 4.1:
Infix Annotations / 4.1.1:
Mathematical Symbols / 4.1.2:
Prefix Annotations / 4.1.3:
Syntax Translations / 4.1.4:
Document Preparation / 4.2:
Isabelle Sessions / 4.2.1:
Structure Markup / 4.2.2:
Formal Comments and Antiquotations / 4.2.3:
Interpretation of Symbols / 4.2.4:
Suppressing Output / 4.2.5:
Logic and Sets / Part II:
The Rules of the Game / 5:
Natural Deduction / 5.1:
Introduction Rules / 5.2:
Elimination Rules / 5.3:
Destruction Rules: Some Examples / 5.4:
Implication / 5.5:
Negation / 5.6:
Interlude: The Basic Methods for Rules / 5.7:
Unification and Substitution / 5.8:
Substitution and the subst Method / 5.8.1:
Unification and Its Pitfalls / 5.8.2:
Quantifiers / 5.9:
The Universal Introduction Rule / 5.9.1:
The Universal Elimination Rule / 5.9.2:
The Existential Quantifier / 5.9.3:
Renaming an Assumption: rename_tac / 5.9.4:
Reusing an Assumption: frule / 5.9.5:
Instantiating a Quantifier Explicitly / 5.9.6:
Description Operators / 5.10:
Definite Descriptions / 5.10.1:
Indefinite Descriptions / 5.10.2:
Some Proofs That Fail / 5.11:
Proving Theorems Using the blast Method / 5.12:
Other Classical Reasoning Methods / 5.13:
Forward Proof: Transforming Theorems / 5.14:
Modifying a Theorem Using of and THEN / 5.14.1:
Modifying a Theorem Using OF / 5.14.2:
Forward Reasoning in a Backward Proof / 5.15:
The Method insert / 5.15.1:
The Method subgoal_tac / 5.15.2:
Managing Large Proofs / 5.16:
Tacticals, or Control Structures / 5.16.1:
Subgoal Numbering / 5.16.2:
Proving the Correctness of Euclid's Algorithm / 5.17:
Sets, Functions, and Relations / 6:
Sets / 6.1:
Finite Set Notation / 6.1.1:
Set Comprehension / 6.1.2:
Binding Operators / 6.1.3:
Finiteness and Cardinality / 6.1.4:
Functions / 6.2:
Function Basics / 6.2.1:
Injections, Surjections, Bijections / 6.2.2:
Function Image / 6.2.3:
Relations / 6.3:
Relation Basics / 6.3.1:
The Reflexive and Transitive Closure / 6.3.2:
A Sample Proof / 6.3.3:
Well-Founded Relations and Induction / 6.4:
Fixed Point Operators / 6.5:
Case Study: Verified Model Checking / 6.6:
Propositional Dynamic Logic - PDL / 6.6.1:
Computation Tree Logic - CTL / 6.6.2:
Inductively Defined Sets / 7:
The Set of Even Numbers / 7.1:
Making an Inductive Definition / 7.1.1:
Using Introduction Rules / 7.1.2:
Rule Induction / 7.1.3:
Generalization and Rule Induction / 7.1.4:
Rule Inversion / 7.1.5:
Mutually Inductive Definitions / 7.1.6:
The Reflexive Transitive Closure / 7.2:
Advanced Inductive Definitions / 7.3:
Universal Quantifiers in Introduction Rules / 7.3.1:
Alternative Definition Using a Monotone Function / 7.3.2:
A Proof of Equivalence / 7.3.3:
Another Example of Rule Inversion / 7.3.4:
Case Study: A Context Free Grammar / 7.4:
Advanced Material / Part III:
More about Types / 8:
Numbers / 8.1:
Numeric Literals / 8.1.1:
The Type of Natural Numbers, nat / 8.1.2:
The Type of Integers, int / 8.1.3:
The Type of Real Numbers, real / 8.1.4:
Pairs and Tuples / 8.2:
Pattern Matching with Tuples / 8.2.1:
Theorem Proving / 8.2.2:
Records / 8.3:
Record Basics / 8.3.1:
Extensible Records and Generic Operations / 8.3.2:
Record Equality / 8.3.3:
Extending and Truncating Records / 8.3.4:
Axiomatic Type Classes / 8.4:
Overloading / 8.4.1:
Axioms / 8.4.2:
Introducing New Types / 8.5:
Declaring New Types / 8.5.1:
Defining New Types / 8.5.2:
Advanced Simplification, Recursion, and Induction / 9:
Advanced Features / 9.1:
How the Simplifier Works / 9.1.2:
Advanced Forms of Recursion / 9.2:
Beyond Measure / 9.2.1:
Recursion over Nested Datatypes / 9.2.2:
Partial Functions / 9.2.3:
Advanced Induction Techniques / 9.3:
Massaging the Proposition / 9.3.1:
Beyond Structural and Recursion Induction / 9.3.2:
Derivation of New Induction Schemas / 9.3.3:
CTL Revisited / 9.3.4:
Case Study: Verifying a Security Protocol / 10:
The Needham-Schroeder Public-Key Protocol / 10.1:
Agents and Messages / 10.2:
Modelling the Adversary / 10.3:
Event Traces / 10.4:
Modelling the Protocol / 10.5:
Proving Elementary Properties / 10.6:
Proving Secrecy Theorems / 10.7:
Appendix / A:
Bibliography
Index
Elementary Techniques / Part I:
The Basics / 1:
Introduction / 1.1:
2.

電子ブック

EB
Stefan Berghofer, Takeo Kanade, Tobias Nipkow, Christian Urban, Makarius Wenzel
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2009
所蔵情報: loading…
3.

電子ブック

EB
J. Heering, Karl Meinke, Bernhard Möller, Tobias Nipkow
出版情報: SpringerLink Books Lecture Notes In Computer Science Archive , Springer Berlin Heidelberg, 1994
所蔵情報: loading…
4.

電子ブック

EB
Hendrik Pieter Barendregt, Tobias Nipkow
出版情報: SpringerLink Books Lecture Notes In Computer Science Archive , Springer Berlin Heidelberg, 1994
所蔵情報: loading…
5.

電子ブック

EB
Jayadev Misra, Takeo Kanade, Tobias Nipkow, Emil Sekerinski
出版情報: Springer eBooks Computer Science , Springer Berlin / Heidelberg, 2006
所蔵情報: loading…
目次情報: 続きを見る
Invited Talk
The Embedded Systems Design Challenge / Thomas A. Henzinger ; Joseph Sifakis
Interactive Verification
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse / Gerhard Schellhorn ; Holger Grandy ; Dominik Haneberg ; Wolfgang Reif
Interactive Verification of Medical Guidelines / Jonathan Schmitt ; Alwin Hoffmann ; Michael Balser ; Mar Marcos
Certifying Airport Security Regulations Using the Focal Environment / David Delahaye ; Jean-Frederic Etienne ; Veronique Viguie Donzeau-Gouge
Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study / Shinya Umeno ; Nancy Lynch
Validating the Microsoft Hypervisor / Ernie Cohen
Formal Modelling of Systems
Interface Input/Output Automata / Kim G. Larsen ; Ulrik Nyman ; Andrzej Wasowski
Properties of Behavioural Model Merging / Greg Brunet ; Marsha Chechik ; Sebastian Uchitel
Automatic Translation from Circus to Java / Angela Freitas ; Ana Lucia Caneca Cavalcanti
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems / Annabelle K. McIver
Real Time
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++ / Marcel Verhoef ; Peter Gorm Larsen ; Jozef Hooman
Towards Modularized Verification of Distributed Time-Triggered Systems / Jewgenij Botaschanjan ; Alexander Gruler ; Alexander Harhurin ; Leonid Kof ; Maria Spichkova ; David Trachtenherz
Industrial Experience
A Story About Formal Methods Adoption by a Railway Signaling Manufacturer / Stefano Bacherini ; Alessandro Fantechi ; Matteo Tempestini ; Niccolo Zingoni
Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach / Yujun Zheng ; Jinquan Wang ; Kan Wang ; Jinyun Xue
Specification and Refinement
Compositional Class Refinement in Object-Z / Tim McComb ; Graeme Smith
A Proposal for Records in Event-B / Neil Evans ; Michael Butler
Pointfree Factorization of Operation Refinement / Jose Nuno Oliveira ; Cesar Jesus Rodrigues
A Formal Template Language Enabling Metaproof / Nuno Amalio ; Susan Stepney ; Fiona Polack
Programming Languages
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions (Best Paper) / Ioannis T. Kassios
Type-Safe Two-Level Data Transformation / Alcino Cunha ; Joost Visser
Algebra
Feature Algebra / Peter Hofner ; Ridha Khedri ; Bernhard Moller
Education
Using Domain-Independent Problems for Introducing Formal Methods / Raymond Boute
Compositional Binding in Network Domains / Pamela Zave
Formal Modeling of Communication Protocols by Graph Transformation / Zarrin Langari ; Richard Trefler
Feature Specification and Static Analysis for interaction Resolution / Marc Aiguier ; Karim Berkani ; Pascale Le Gall
A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice / Mass Soldal Lund ; Ketil Stolen
Formal Aspects of Java
Towards Automatic Exception Safety Verification / Xin Li ; H. James Hoover ; Piotr Rudnicki
Enforcer - Efficient Failure Injection / Cyrille Valentin Artho ; Armin Biere ; Shinichi Honiden
Automated Boundary Test Generation from JML Specifications / Fabrice Bouquet ; Frederic Dadeau ; Bruno Legeard
Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic / Wojciech Mostowski
Formal Verification of a C Compiler Front-End / Sandrine Blazy ; Zaynah Dargaye ; Xavier Leroy
A Memory Model Sensitive Checker for C# / Thuan Quang Huynh ; Abhik Roychoudhury
Changing Programs Correctly: Refactoring with Specifications / Fabian Bannwart ; Peter Muller
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic / Viorel Preoteasa
Model Checking
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking / Wendy Johnston ; Kirsten Winter ; Lionel van den Berg ; Paul Strooper ; Peter Robinson
Exact and Approximate Strategies for Symmetry Reduction in Model Checking / Alastair F. Donaldson ; Alice Miller
Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces / Alexandre Genon ; Thierry Massart ; Cedric Meuter
PSL Model Checking and Run-Time Verification Via Testers / Amir Pnueli ; Aleksandr Zaks
Industry Day: Abstracts of Invited Talks
Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline / Werner Stephan
Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche / David von Oheimb
Connector-Based Software Development: Deriving Secure Protocols / Dusko Pavlovic
Model-Based Security Engineering for Real / Jan Jurjens
Cost Effective Software Engineering for Security / D. Randolph Johnson
Formal Methods and Cryptography / Michael Backes ; Birgit Pfitzmann ; Michael Waidner
Verified Software Grand Challenge / Jim Woodcock
Author Index
Invited Talk
The Embedded Systems Design Challenge / Thomas A. Henzinger ; Joseph Sifakis
Interactive Verification
6.

電子ブック

EB
Franz Baader and Tobias Nipkow
出版情報:   1 online resource (xii, 301 pages)
所蔵情報: loading…
目次情報: 続きを見る
Motivating examples / 1:
Abstract reduction systems / 2:
Universal algebra / 3:
Equational problems / 4:
Termination / 5:
Confluence / 6:
Completion / 7:
Gröbner bases and Buchberger's algorithm / 8:
Combination problems / 9:
Equational unification / 10:
Extensions / 11:
Ordered sets / Appendix 1:
A bluffer's guide to ML / Appendix 2:
Bibliography
Index
Motivating examples / 1:
Abstract reduction systems / 2:
Universal algebra / 3:
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼