close
1.

図書

図書
Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus (eds.)
出版情報: Berlin ; Tokyo : Springer, c1999  viii, 207 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1657
所蔵情報: loading…
目次情報: 続きを見る
On Relating Type Theories and Set Theories / Peter Aczel
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach / René Ahn ; Tijn Borghuis
Gröbner Bases in Type Theory / Thierry Coquand ; Henrik Persson
A Modal Lambda Calculus with Iteration and Case Constructs / Joëlle Despeyroux ; Pierre Leleu
Proof Normalization Modulo / Gilles Dowek ; Benjamin Werner
Proof of Imperative Programs in Type Theory / Jean-Christophe Filliâtre
An Interpretation of the Fan Theoremin Type Theory / Daniel Fridlender
Conjunctive Types and SKInT / Jean Goubault-Larrecq
Modular Structures as Dependent Types in Isabelle / Florian Kammüller
Metatheory of Verification Calculi in LEGO / Thomas Kleymann
Bounded Polymorphism for Extensible Objects / Luigi Liquori
About Effective Quotients in Constructive Type Theory / Maria Emilia Maietti
Algorithms for Equality and Unification in the Presence of Notational Definitions / Frank Pfenning ; Carsten Schurmann
A Preview of the Basic Picture: A New Perspective on Formal Topology / Giovanni Sambin ; Silvia Gebellato
On Relating Type Theories and Set Theories / Peter Aczel
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach / René Ahn ; Tijn Borghuis
Gröbner Bases in Type Theory / Thierry Coquand ; Henrik Persson
2.

図書

図書
Xiao-Shan Gao, Dongming Wang, Lu Yang (eds.)
出版情報: Berlin : Springer, c1999  vi, 285 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1669 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving / Wen-tsün Wu
Solving Geometric Problems with Real Quantifier Elimination / Andreas Dolzmann
Automated Discovering and Proving for Geometric Inequalities / Lu Yang ; Xiaorong Hou ; Bican Xia
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle / Jacques D. Fleuriot ; Lawrence C. Paulson
Readable Machine Solving in Geometry and ICAI Software MSG / Chuan-Zhong Li ; Jing-Zhong Zhang
Plane Euclidean Reasoning / Desmond Fearnley-Sander
A Clifford Algebraic Method for Geometric Reasoning / Haiquan Yang ; Shugong Zhang ; Guochen Feng
Clifford Term Rewriting for Geometric Reasoning in 3D / Thierry Boy de la Tour ; Stéphane Fèvre ; Dongming Wang
Some Applications of Clifford Algebra to Geometries / Hongbo Li
Decomposing Algebraic Varieties
An Application of Automatic Theorem Proving in Computer Vision / Didier Bondyfalat ; Bernard Mourrain ; Thèodore Papadopoulo
Automated Geometry Diagram Construction and Engineering Geometry / Xiao-Shan Gao
A 2D Geometric Constraint Solver for Parametric Design Using Graph Analysis and Reduction / Jae Yeol Lee
Variant Geometry Analysis and Synthesis in Mechanical CAD / Zongying Ou ; Jun Liu
Author Index
Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving / Wen-tsün Wu
Solving Geometric Problems with Real Quantifier Elimination / Andreas Dolzmann
Automated Discovering and Proving for Geometric Inequalities / Lu Yang ; Xiaorong Hou ; Bican Xia
3.

図書

図書
Claude Kirchner, Hélène Kirchner (eds.)
出版情報: Berlin : Springer, c1998  xiv, 441 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1421 . Lecture notes in artificial intelligence
所蔵情報: loading…
4.

図書

図書
Jim Grundy, Malcolm Newey (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 496 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1479
所蔵情報: loading…
目次情報: 続きを見る
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
Refereed Papers
Program Abstraction in a Higher-Order Logic Framework / Marco Benini ; Sara Kalvala ; Dirk Nowotka
The Village Telephone System: A Case Study in Formal Software Engineering / Karthikeyan Bhargavan ; Carl A. Gunter ; Elsa L. Gunter ; Michael Jackson ; Davor Obradovic ; Pamela Zave
Generating Embeddings from Denotational Descriptions / Richard J. Boulton
An Interface between CLaM and HOL / Richard Boulton ; Konrad Slind ; Alan Bundy ; Mike Gordon
Classical Propositional Decidability via Nuprl Proof Extraction / James L. Caldwell
A Comparison of PVS and Isabelle/HOL / David Griffioen ; Marieke Huisman
Adding External Decision Procedures to HOL90 Securely
Formalizing Basic First Order Model Theory / John Harrison
Formalizing Dijkstra
Mechanical Verification of Total Correctness through
Diversion Verification Conditions / Peter V. Homeier ; David F. Martin
A Type Annotation Scheme for Nuprl / Douglas J. Howe
Verifying a Garbage Collection Algorithm / Paul B. Jackson
Hot: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux / Karsten Konrad
Free Variables and Subexpressions in Higher-Order Meta Logic / Chuck Liang
An LPO-Based Termination Ordering for Higher-Order Terms without ?-Abstraction / Maxim Lifantsev ; Leo Bachmair
Proving Isomorphism of First-Order Logic Proof Systems in HOL / Anna Mikhajlova
Exploiting Parallelism in Interactive Theorem Provers / Roderick Moten
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle / Olaf Müller
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic / Wolfgang Naraschewski ; Markus Wenzel
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System / Naren Narasimhan ; Ranga Vemuri
Co-inductive Axiomatization of a Synchronous Language / David Nowak ; Jean-Rene Beauvais ; Jean-Pierre Talpin
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling / François Puitg ; Jean-François Dufourd
A Tool for Data Refinement / Rimvydas RukÃœenas
Mechanizing Relevant Logics with HOL / Hajime Sawamura ; Daisaku Asanuma
Case Studies in Meta-Level Theorem Proving / Friedrich W. von Henke ; Stephan Pfab ; Holger Pfeifer ; Harald Rueß
Formalization of Graph Search Algorithms and Its Applications / Mitsuharu Yamamoto ; Koichi Takahashi ; Masami Hagiya ; Shin-ya Nishizaki ; Tetsuo Tamai
Author Index
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
5.

図書

図書
Eduardo Giménez, Christine Paulin-Mohring (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 372 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1512
所蔵情報: loading…
6.

図書

図書
Harald Ganzinger, David McAllester, Andrei Voronkov (eds.)
出版情報: Berlin ; New York : Springer-Verlag, c1999  xii, 395 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1705 . Lecture notes in artificial intelligence
所蔵情報: loading…
7.

図書

図書
Yves Bertot ... [et al.] (eds.)
出版情報: Berlin : Springer, c1999  viii, 358 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1690
所蔵情報: loading…
8.

図書

図書
Ganesh Gopalakrishnan, Phillip Windley, (eds.)
出版情報: Berlin ; New York : Springer, c1998  ix, 528 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1522
所蔵情報: loading…
目次情報: 続きを見る
Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verification / Kenneth L. McMillan
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution / Robert B. Jones ; Jens U. Skakkebaek ; David L. Dill
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking / Miroslav N. Velev ; Randal E. Bryant
Solving Bit-Vector Equations / M.Oliver Moller ; Harald Rueß
The Formal Design of 1M-Gate ASICs / Asgeir Por Eiriksson
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations / Justin E. Harlow III ; Franc Brglez
A Tutorial on Stalmarck's Proof Procedure for Propositional Logic Mary Sheeran and Gunnar Stalmarck
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods / Macha Nikolskaia ; Antoine Rauzy ; David James Sherman
Bisimulation Minimization in an Automata-Theoretic Verification Framework / Kathi Fisler ; Moshe Y. Vardi
Automatic Verification of Mixed-Level Logic Circuits / Keith Hanna
A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk / S. Tasiran ; S.P. Khatri ; S. Yovine ; R.K. Brayton ; A. Sangiovanni-Vincentelli
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints / Fen Jin ; Henrik Hulgaard ; Eduard Cerny
Using MTBDDs for Composition and Model Checking of Real-Time Systems / Jurgen Ruf ; Thomas Kropf
Formal Methods in CAD from an Industrial Perspective / Carl-Johan H. Seger
A Methodology for Automatic Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool / Nazanin Mansouri ; Ranga Vemuri
Combined Formal Post- and Presynthesis Verification in High Level Synthesis / Thomas Lock ; Michael Mendler ; Matthias Mutz
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem / Abdel Mokkedem ; Ravi Hosabettu ; Ganesh Gopalakrishnan
A Performance Study of BDD-Based Model Checking / Bwolen Yang ; David R. O'Hallaron ; Armin Biere ; Olivier Coudert ; Geert Janssen ; Rajeev K. Ranjan ; Fabio Somenzi
Symbolic Model Checking Visualization / Gila Kamhi ; Limor Fix ; Ziv Binyamini
Input Elimination and Abstraction in Model-Checking / Sela Mador-Haim
Symbolic Simulation of the JEM1 Microprocessor / David A. Greve
Symbolic Simulation: An ACL2 Approach / J. Strother Moore
Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study / Amir Pnueli ; T. Arons
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification / Sergey Berezin ; Edmund Clarke ; Yunshan Zhu
Formally Verifying Data and Control with Weak Reachability Invariants / Jeffrey Su
Generalized Reversible Rules / C. Norris Ip
An Assume-Guarantee Rule for Checking Simulation / Thomas A. Henzinger ; Shaz Qadeer ; Sriram K. Rajamani ; Serdar Tasiran
Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared / Sofiene Tahar ; Paul Curzon ; Jianping Lu
An Instruction Set Process Calculus / Shiu-Kai Chin ; Jang Dae Kim
Techniques for Implicit State Enumeration of EFSMs / James H. Kukula ; Tom R. Shiple ; Adnan Aziz
Model Checking on Product Structures / Klaus Schneider
BDDNOW: A Parallel BDD Package / Kim Milvang-Jensen ; Alan J. Hu
Model-Checking VHDL with CV / David Deharbe ; Subash Shankar ; Edmund M. Clarke
Alexandria: A Tool for Hierarchical Verification / Annette Bunker ; Trent N. Larson ; Michael D. Jones ; Phillip J. Windley
PV: An Explicit Enumeration Model-Checker / Ratan Nalumasu
Author Index
Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verification / Kenneth L. McMillan
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution / Robert B. Jones ; Jens U. Skakkebaek ; David L. Dill
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking / Miroslav N. Velev ; Randal E. Bryant
9.

図書

図書
Willem-Paul de Roever, Hans Langmaack, Amir Pnueli (eds.)
出版情報: Berlin ; New York : Springer, c1998  646 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1536
所蔵情報: loading…
目次情報: 続きを見る
The Need for Compositional Proof Systems: A Survey / Willem-Paul de Roever
Alternating-Time Temporal Logic / Rajeev Alur ; Thomas A. Henzinger ; Orna Kupferman
Compositionality in Data ow Synchronous Languages: Speci cation and Code Generation / Albert Benveniste ; Paul Le Guernic ; Pascal Aubry
Compositional Reasoning in Model Checking / Sergey Berezin ; Sérgio Campos ; Edmund M. Clarke
Modeling Urgency in Timed Systems / Sebastien Bornot ; Joseph Sifakis ; Stavros Tripakis
Compositional Re nement of Interactive Systems Modelled by Relations / Manfred Broy
Toward Parametric Veri cation of Open Distributed Systems / Mads Dam ; Lars-Ã¥ke Fredlund ; Dilian Gurov
A Compositional Real-Time Semantics of STATEMATE Designs / Werner Damm ; Bernhard Josko ; Hardi Hungar ; Amir Pnueli
Deductive Veri cation of Modular Systems / Bernd Finkbeiner ; Zohar Manna ; Henny B. Sipma
Compositional Veri cation of Real-Time Applications / Jozef Hooman
Compositional Proofs for Concurrent Objects / Jerry James ; Ambuj Singh
An Overview of Compositional Translations / Theo M.V. Janssen
Compositional Veri cation of Multi-Agent Systems: A Formal Analysis of Pro-activeness and Reactiveness / Catholijn M. Jonker ; Jan Treur
Modular Model Checking / Moshe Y. Vardi
Composition: A Way to Make Proofs Harder / Leslie Lamport
Compositionality Criteria for De ning Mixed-Styles Synchronous Languages / Florence Maraninchi ; Yann Rémond
Compositional Reasoning Using Interval Temporal Logic and Tempura / Ben C. Moszkowski
Decomposing Real-Time Speci cations / Ernst-Rudiger Olderog ; Henning Dierks
On the Combination of Synchronous Languages / Axel Poigné ; Leszek Holenderski
Compositional Veri cation of Randomized Distributed Algorithms / Roberto Segala
Lazy Compositional Veri cation / Natarajan Shankar
Compositional Reasoning Using the Assumption-Commitment Paradigm / Qiwen Xu ; Mohalik Swarup
An Adequate First Order Interval Logic / Chaochen Zhou ; Michael R. Hansen
Compositional Transformational Design for Concurrent Programs / Job Zwiers
Compositional Proof Methods for Concurrency: A Semantic Approach / Frank S. de Boer
Author Index
The Need for Compositional Proof Systems: A Survey / Willem-Paul de Roever
Alternating-Time Temporal Logic / Rajeev Alur ; Thomas A. Henzinger ; Orna Kupferman
Compositionality in Data ow Synchronous Languages: Speci cation and Code Generation / Albert Benveniste ; Paul Le Guernic ; Pascal Aubry
10.

図書

図書
Didier Galmiche (ed.)
出版情報: Berlin ; Heidelberg : Springer, c1997  xi, 372 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1227 . Lecture notes in artificial intelligence
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼