close
1.

図書

図書
Andrei Voronkov (ed.)
出版情報: Berlin : Springer, c2002  xii, 534 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2392 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Description Logics and Semantic Web / Session 1:
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks
BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi
Proof-Carrying Code and Compiler Verification / Session 2:
Temporal Logic for Proof-Carrying Code / Andrew Bernard ; Peter Lee
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code / Robert R. Schneck ; George C. Necula
Formal Verification of a Java Compiler in Isabelle / Martin Strecker
Non-classical Logics / Session 3:
Embedding Lax Logic into Intuitionistic Logic / Uwe Egly
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic / Dominique Larchey-Wendling
Connection-Based Proof Search in Propositional BI Logic / Didier Galmiche ; Daniel Méry
System Descriptions / Session 4:
DDDLIB: A Library for Solving Quantified Difference Inequalities / Jesper B. Møller
An LCF-Style Interface between HOL and First-Order Logic / Joe Hurd
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning / Jürgen Zimmer ; Michael Kohlhase
Proof Development with ΩMEGA / Jörg Siekmann ; Christoph Benzmüller ; Vladimir Brezhnev ; Lassaad Cheikhrouhou ; Armin Fiedler ; Andreas Franke ; Helmut Horacek ; Andreas Meier ; Erica Melis ; Markus Moschner ; Immanuel Normann ; Martin Pollet ; Volker Sorge ; Carsten Ullrich ; Claus-Peter Wirth ; Juörgen Zimmer
LearnΩmatic: System Description / Mateja Jamnik ; Manfred Kerber
HyLoRes 1.0: Direct Resolution for Hybrid Logics / Carlos Areces ; Juan Heguiabehere
SAT / Session 5:
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points / Eugene Goldberg
A Note on Symmetry Heuristics in SEM / Thierry Boy de la Tour
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions / Gilles Audemard ; Piergiorgio Bertoli ; Alessandro Cimatti ; Artur Kornilowicz ; Roberto Sebastiani
Model Generation / Session 6:
Deductive Search for Errors in Free Data Type Specifications Using Model Generation / Wolfgang Ahrendt
Reasoning by Symmetry and Function Ordering in Finite Model Generation / Belaid Benhamou
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations / Bernhard Gramlich ; Reinhard Pichler
A New Clausal Class Decidable by Hyperresolution / Lilia Georgieva ; Ullrich Hustadt ; Renate A. SchmidtSession 7:
CASC / Session 8:
Spass Version 2.0 / Christoph Weidenbach ; Uwe Brahm ; Thomas Hillenbrand ; Enno Keen ; Christian Theobald ; Dalibor Topić
System Description: GrAnDe 1.0 / Stephan Schulz ; Geoff Sutcliffe
The HR Program for Theorem Generation / Simon Colton
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description - / Michael Whalen ; Johann Schumann ; Bernd Fischer
CADE-CAV Invited Talk
The Quest for Efficient Boolean Satisfiability Solvers / Lintao Zhang ; Sharad Malik
Recursive Path Orderings Can Be Context-Sensitive / Cristina Borralleras ; Salvador Lucas ; Albert RubioSession 9:
Combination of Decision Procedures / Session 10:
Shostak Light / Harald Ganzinger
Formal Verification of a Combination Decision Procedure / Jonathan Ford ; Natarajan Shankar
Combining Multisets with Integers / Calogero G. Zarba
Logical Frameworks / Session 11:
The Reflection Theorem: A Study in Meta-theoretic Reasoning / Lawrence C. Paulson
Faster Proof Checking in the Edinburgh Logical Framework / Aaron Stump ; David L. Dill
Solving for Set Variables in Higher-Order Theorem Proving / Chad E. Brown
Model Checking / Session 12:
The Complexity of the Graded μ-Calculus / Orna Kupferman
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains / Leonardo de Moura ; Harald Rueß ; Maria Sorea
Equational Reasoning / Session 13:
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation / Miquel Bofill
Basic Syntactic Mutation / Christopher Lynch ; Barbara Morawska
The Next Waldmeister Loop / Bernd Lochner
Proof Theory / Session 14:
Focussing Proof-Net Construction as a Middleware Paradigm / Jean Marc Andreoli
Proof Analysis by Resolution / Matthias Baaz
Author Index
Description Logics and Semantic Web / Session 1:
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks
BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi
2.

図書

図書
Peter J. Stuckey (ed.)
出版情報: Berlin : Springer, c2002  xi, 486 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2401
所蔵情報: loading…
3.

図書

図書
Uwe Egly, Christian G. Fermüller (eds.)
出版情報: Berlin : Springer, c2002  x, 339 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2381 . Lecture notes in artificial intelligence
所蔵情報: loading…
4.

図書

図書
Victor A. Carreño, César A. Muñoz, Sofiène Tahar (eds.)
出版情報: Berlin : Springer, c2002  x, 347 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2410
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
Regular Papers
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction / Simon J. Ambler ; RoyL. Crole ; Alberto Momigliano
Efficient Reasoning about Executable Specifications in Coq / Gilles Barthe ; Pierre Courtieu
Verified Bytecode Model Checkers / David Basin ; Stefan Friedrich ; Marek Gawkowski
The 5 Colour Theorem in Isabelle/Isar / Gertrud Bauer ; Tobias Nipkow
Type-Theoretic Functional Semantics / Yves Bertot ; Venanzio Capretta ; Kuntal Das Barman
A Proposal for a Formal OCL Semantics in Isabelle/HOL / Achim D. Brucker ; Burkhart Wolff
Explicit Universes for the Calculus of Constructions / Judicaël Courant
Formalised Cut Admissibility for Display Logic / JeremyE. Dawson ; Rajeev GorÆe
Formalizing the Trading Theorem for the Classification of Surfaces / Christophe Dehlinger ; Jean-Francois Dufourd
Free-Style Theorem Proving / David Delahaye
A Comparison of Two Proof Critics: Power vs. Robustness / Louise A. Dennis ; Alan Bundy
Two-Level Meta-reasoning in Coq / AmyP. Felty
PuzzleTool: An Example of Programming Computation and Deduction / Michael J.C. Gordon
A Formal Approach to Probabilistic Termination / Joe Hurd
Using Theorem Proving for Numerical Analysis / Micaela Mayero
Quotient Types: A Modular Approach / AlekseyNogin
Sequent Schema for Derived Rules / Jason Hickey
Algebraic Structures and Dependent Records / Virgile Prevosto ; Damien Doligez ; Therese Hardin
Proving the Equivalence of Microstep and Macrostep Semantics / Klaus Schneider
Weakest Precondition for General Recursive Programs Formalized in Coq / Xingyuan Zhang ; Malcolm Munro ; Mark Harman ; Lin Hu
Author Index
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
5.

図書

図書
Reinhard Kahle, Peter Schroeder-Heister, Robert Stärk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2001  viii, 238 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2183
所蔵情報: loading…
目次情報: 続きを見る
Linear Ramified Higher Type Recursion and Parallel Complexity / Klaus Aehlig ; Jan Johannsen ; Helmut Schwichtenberg ; Sebastiaan A. Terwijn
Reflective λ-Calculus / Jesse Alt ; Sergei Artemov
A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity / Matthias Baaz ; Christian G. Fermuller
Comparing the Complexity of Cut-Elimination Methods / Alexander Leitsch
Program Extraction from Gentzen's Proof of Transfinite Induction up to ε0 / Ulrich Berger
Coherent Bicartesian and Sesquicartesian Categories / Kosta DoÜen ; Zoran Petri?
Indexed Induction-Recursion / Peter Dybjer ; Anton Setzer
Modeling Meta-logical Features in a Calculus with Frozen Variables / Birgit Elbl
Proof Theory and Post-turing Analysis / Lew Gordeew
Interpolation for Natural Deduction with Generalized Eliminations / Ralph Matthes
Implicit Characterizations of Pspace / Isabel Oitavem
Iterate Logic / Peter H. Schmitt
Constructive Foundations for Featherweight Java / Thomas Studer
Author Index
Linear Ramified Higher Type Recursion and Parallel Complexity / Klaus Aehlig ; Jan Johannsen ; Helmut Schwichtenberg ; Sebastiaan A. Terwijn
Reflective λ-Calculus / Jesse Alt ; Sergei Artemov
A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity / Matthias Baaz ; Christian G. Fermuller
6.

図書

図書
Robert Nieuwenhuis, Andrei Voronkov (eds.)
出版情報: Berlin ; New York : Springer, c2001  xv, 738 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2250 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Invited Talk / Session 1:
Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev
Verification / Session 2:
On Bounded Specifications / Orna Kupferman ; Moshe Y. Vardi
Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy / Klaus Schneider
Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets / Volker Diekert ; Paul Gastin
Guarded Logics / Session 3:
Games and Model Checking for Guarded Logics / Dietmar Berwanger ; Erich Grädel
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae / Lilia Georgieva ; Ullrich Hustadt ; Renate A. Schmidt
Agents / Session 4:
Local Conditional High-Level Robot Programs / Natasha Alechina ; Brian Logan ; Sebastian SardiñaLogical Omniscience and the Cost of Deliberation:
A Refinement Theory That Supports Reasoning about Knowledge and Time for Synchronous Agents / Kai Engelhardt ; Ron van der Meyden ; Yoram Moses
Automated Theorem Proving / Session 5:
Proof and Model Generation with Disconnection Tableaux / Reinhold Letz ; Gernot Stenz
Counting the Number of Equivalent Binary Resolution Proofs / Joseph D. Horton
Splitting through New Proposition Symbols / Hans de NivelleSession 6:
Complexity of Linear Standard Theories / Christopher Lynch ; Barbara Morawska
Herbrand's Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving / Matthias Baaz ; Agata Ciabattoni ; Christian G. Fermüller
Non-classical Logics / Session 7:
Unification in a Description Logic with Transitive Closure of Roles / Franz Baader ; Ralf Küsters
Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions / Guy Perrier
Types / Session 8:
Coherence and Transitivity in Coercive Subtyping / Yong Luo ; Zhaohui Luo
A Type-Theoretic Approach to Induction with Higher-Order Encodings / Carsten Schürmann
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification / Jan-Georg Smaus
Experimental Papers / Session 9:
First-Order Atom Definitions Extended / Miyuki Koshimura ; Hiroshi Fujita ; Ryuzo Hasegawa ; Bijan Afshordel ; Thomas Hillenbrand ; Christoph WeidenbachModel Generation with Boolean Constraints:
Automated Proof Support for Interval Logics / Thomas Marthedal Rasmussen
Foundations of Logic / Session 10:
The Functions Provable by First Order Abstraction / Daniel Leivant
A Local System for Classical Logic / Kai Brunnler ; Alwen Fernanto Tiu
CSP and SAT / Session 11:
Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae / Jussi Rintanen
Permutation Problems and Channelling Constraints / Toby Walsh
Simplifying Binary Propositional Theories into Connected Components Twice as Fast / Alvaro del Val
Non-monotonic Reasoning / Session 12:
Reasoning about Evolving Nonmonotonic Knowledge Bases / Thomas Eiter ; Michael Fink ; Giuliana Sabbatini ; Hans Tompits
Efficient Computation of the Well-Founded Model Using Update Propagation / Andreas Behrend
Semantics / Session 13:
Indexed Categories and Bottom-Up Semantics of Logic Programs / Gianluca Amato ; James Lipton
Functional Logic Programming with Failure: A Set-Oriented View / F.J. Lopez-Fraguas ; J. Sanchez-Hernandez
Operational Semantics for Fixed-Point Logics on Constraint Databases / Stephan Kreutzer
Efficient Negation Using Abstract Interpretation / Susana Muñoz ; Juan José Moreno ; Manuel HermenegildoSession 14:
Certifying Synchrony for Free / Sylvain Boulmé ; Grégoire Hamon
A Computer Environment for Writing Ordinary Mathematical Proofs / David McMath ; Marianna Rozenfeld ; Richard Sommer
Termination / Session 15:
On Termination of Meta-programs / Alexander Serebrenik ; Danny De Schreye
A Monotonic Higher-Order Semantic Path Ordering / Cristina Borralleras ; Albert Rubio
Knowledge-Based Systems / Session 16:
The Elog Web Extraction Language / Robert Baumgartner ; Sergio Flesca ; Georg Gottlob
Census Data Repair: A Challenging Application of Disjunctive Logic Programming / Enrico Franconi ; Antonio Laureti Palma ; Nicola Leone ; Simona Perri ; Francesco Scarcello
Analysis of Logic Programs / Session 17:
Boolean Functions for Finite-Tree Dependencies / Roberto Bagnara ; Enea Zaffanella ; Roberta Gori ; Patricia M. Hill
How to Transform an Analyzer into a Verifier / Marco Comini ; Giorgio Levi
Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search / Rong Yang ; Steve Gregory
Databases and Knowledge Bases / Session 18:
Coherent Composition of Distributed Knowledge-Bases through Abduction / Ofer Arieli ; Bert Van Nuffelen ; Marc Denecker ; Maurice Bruynooghe
Tableaux for Reasoning about Atomic Updates / Georg Moser ; Richard Zach
Inference of Termination Conditions for Numerical Loops in Prolog / Session 19:
Termination of Rewriting with Strategy Annotations / Salvador Lucas
Inferring Termination Conditions for Logic Programs Using Backwards Analysis / Samir Genaim ; Michael Codish
Program Analysis and Proof Planning / Session 20:
Reachability Analysis of Term Rewriting Systems with Timbuk / Thomas Genet ; Valerie Viet Triem Tong
Binding-Time Annotations without Binding-Time Analysis / Wim Vanhoof
Concept Formation via Proof Planning Failure / Raúl Monroy
Author Index
Invited Talk / Session 1:
Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev
Verification / Session 2:
7.

図書

図書
Philippe Codognet (ed.)
出版情報: Berlin ; New York : Springer, c2001  xi, 364 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2237
所蔵情報: loading…
8.

図書

図書
Rajeev Goré, Alexander Leitsch, Tobias Nipkow (eds.)
出版情報: Berlin : Springer, c2001  xv, 708 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2083 . Lecture notes in artificial intelligence
所蔵情報: loading…
9.

図書

図書
Paul Callaghan ... [et al.] (eds.)
出版情報: Berlin ; New York : Springer, c2002  viii, 242 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2277
所蔵情報: loading…
目次情報: 続きを見る
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
An Implementation of Type: Type / Thierry Coquand ; Makoto Takeyama
On the Logical Content of Computational Type Theory: A Solution to CurryÆs Problem / Matt Fairtlough ; Michael Mendler
Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers ; Milad Niqui
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Freek Wiedijk ; Jan Zwanenburg
AKripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen
Towards Limit Computable Mathematics / Susumu Hayashi ; Masahiro Nakata
Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo
Changing Data Structures in Type Theory: AStudy of Natural Numbers / Nicolas Magaud ; Yves Bertot
Elimination with a Motive / Conor McBride
Generalization in Type Theory Based Proof Assistants / Olivier Pons
An Inductive Version of Nash-WilliamsÆ Minimal-Bad-Sequence Argument for HigmanÆs Lemma / Monika Seisenberger
Author Index
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
10.

図書

図書
Richard J. Boulton, Paul B. Jackson (eds.)
出版情報: Berlin : Springer, c2001  x, 393 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2152
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
JavaCard Program Verification / Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001) / Steven D. Johnson
Using Decision Procedures with a Higher-Order Logic / Natarajan Shankar
Regular Contributions
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS / Andrew Adams ; Martin Dunstan ; Hanne Gottliebsen ; Tom Kelsey ; Ursula Martin ; Sam Owre
An Irrational Construction of R from Z / Rob D. Arthan
HELM and the Semantic Math-Web / Andrea Asperti ; Luca Padovani ; Claudio Sacerdoti Coen ; Irene Schena
Calculational Reasoning Revisited (An Isabelle/Isar Experience) / Gertrud Bauer ; Markus Wenzel
Mechanical Proofs about a Non-repudiation Protocol / Giampaolo Bella ; Lawrence C. Paulson
Proving Hybrid Protocols Correct / Mark Bickford ; Christoph Kreitz ; Robbert van Renesse ; Xiaoming Liu
Nested General Recursion and Partiality in Type Theory / Ana Bove ; Venanzio Capretta
A Higher-Order Calculus for Categories / Mario Cáccamo ; Glynn Winskel
Certifying the Fast Fourier Transform with Coq
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing / Marc Daumas ; Laurence Rideau ; Laurent Théry
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain / Louise A. Dennis ; Alan Smaill
Abstraction and Refinement in Higher Order Logic / Matt Fairtlough ; Michael Mendler ; Xiaochun Cheng
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL / Simon J. Gay
Representing Hierarchical Automata in Interactive Theorem Provers / Steffen Helke ; Florian Kammüller
Refinement Calculus for Logic Programming in Isabelle/HOL / David Hemer ; Ian Hayes ; Paul Strooper
Predicate Subtyping with Predicate Sets / Joe Hurd
A Structural Embedding of Ocsid in PVS / Pertti Kellomaki
A Certified Polynomial-Based Decision Procedure for Propositional Logic / Inmaculada Medina-Bulo ; Francisco Palomo-Lozano ; José A. Alonso-Jiménez
Finite Set Theory in ACL2 / J Strother Moore
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability) / Pavel Naumov ; Mark-Oliver Stehr ; José Meseguer
Formalizing Convex Hull Algorithms / David Pichardie ; Yves Bertot
Experiments with Finite Tree Automata in Coq / Xavier Rival ; Jean Goubault-Larrecq
Mizar Light for HOL Light / Freek Wiedijk
Author Index
Invited Talks
JavaCard Program Verification / Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001) / Steven D. Johnson
11.

図書

図書
Jürgen Richter-Gebert, Dongming Wang (eds.)
出版情報: Berlin : Springer, c2001  viii, 323 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2061 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
On Spatial Constraint Solving Approaches / Christoph M. Hoffmann ; Bo Yuan
A Hybrid Method for Solving Geometric Constraint Problems / Xiao-Shan Gao ; Lei-Dong Huang ; Kun Jiang
Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study / Fabrice Rouillier ; Mohab Safey El Din ; Éric Schost
A Practical Program of Automated Proving for a Class of Geometric Inequalities / Lu Yang ; Ju Zhang
Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving / Daniela Tulone ; Chee Yap ; Chen Li
Algebraic and Semialgebraic Proofs: Methods and Paradoxes / Pasqualina Conti ; Carlo Traverso
Remarks on Geometric Theorem Proving / Laura Bazzotti ; Giorgio Dalzotto ; Lorenzo Robbiano
The Kinds of Truth of Geometry Theorems / Michael Bulmer ; Desmond Fearnley-Sander ; Tim Stokes
A Complex Change of Variables for Geometrical Reasoning
Reasoning about Surfaces Using Differential Zero and Ideal Decomposition / Philippe Aubry ; Dongming Wang
Effective Methods in Computational Synthetic Geometry / Jürgen Bokowski
Decision Complexity in Dynamic Geometry / Ulrich Kortenkamp ; Jürgen Richter-Gebert
Automated Theorem Proving in Incidence Geometry - A Bracket Algebra Based Elimination Method / Hongbo Li ; Yihong Wu
Qubit Logic, Algebra and Geometry / Timothy F. Havel
Nonstandard Geometric Proofs / Jacques D. Fleuriot
Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization / Ricardo Caferra ; Nicolas Peltier ; François Puitg
Higher-Order Intuitionistic Formalization and Proofs in HilbertÆs Elementary Geometry / Christophe Dehlinger ; Jean-François Dufourd ; Pascal Schreck
Author Index
On Spatial Constraint Solving Approaches / Christoph M. Hoffmann ; Bo Yuan
A Hybrid Method for Solving Geometric Constraint Problems / Xiao-Shan Gao ; Lei-Dong Huang ; Kun Jiang
Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study / Fabrice Rouillier ; Mohab Safey El Din ; Éric Schost
12.

図書

図書
Hoon Hong, Dongming Wang (eds.)
出版情報: Berlin : Springer, c2006  x, 211 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3763 . Lecture notes in artificial intelligence
所蔵情報: loading…
13.

図書

図書
Jean Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner (eds.)
出版情報: Berlin : Springer, c2006  viii, 273 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3839
所蔵情報: loading…
14.

図書

図書
Bart Demoen, Vladimir Lifschitz (eds.)
出版情報: Berlin ; Tokyo : Springer, c2004  xii, 480 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3132
所蔵情報: loading…
15.

図書

図書
Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.)
出版情報: Berlin : Springer, c2004  viii, 336 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3223
所蔵情報: loading…
目次情報: 続きを見る
Error Analysis of Digital Filters Using Theorem Proving / Behzad Akbarpour ; Sofiène Tahar
Verifying Uniqueness in a Logical Framework / Penny Anderson ; Frank Pfenning
A Program Logic for Resource Verification / David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
Proof Reuse with Extended Inductive Types / Olivier Boite
Hierarchical Reflection / Luís Cruz-Filipe ; Freek Wiedijk
Correct Embedded Computing Futures / Al Davis
Higher Order Rippling in IsaPlanner / Lucas Dixon ; Jacques Fleuriot
A Mechanical Proof of the Cook-Levin Theorem / Ruben Gamboa ; John Cowles
Formalizing the Proof of the Kepler Conjecture / Thomas Hales
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code / Nadeem Abdul Hamid ; Zhong Shao
Extensible Hierarchical Tactic Construction in a Logical Framework / Jason Hickey ; Aleksey Nogin
Theorem Reuse by Proof Term Transformation / Einar Broch Johnsen ; Christoph Lüth
Proving Compatibility Using Refinement / Michael Jones ; Aaron Benson ; Dan Delorey
Java Program Verification via a JVM Deep Embedding in ACL2 / Hanbing Liu ; J. Strother Moore
Reasoning About CBV Functional Programs in Isabelle/HOL / John Longley ; Randy Pollack
Proof Pearl: From Concrete to Functional Unparsing / Jean-Fraçois Monin
A Decision Procedure for Geometry in Coq / Julien Narboux
Recursive Function Definition for Types with Binders / Michael Norrish
Abstractions for Fault-Tolerant Distributed System Verification / Lee Pike ; Jeffrey Maddalon ; Paul Miner ; Alfons Geser
Formalizing Integration Theory with an Application to Probabilistic Algorithms / Stefan Richter
Formalizing Java Dynamic Loading in HOL / Tian-jun Zuo ; Jun-gang Han ; Ping Chen
Certifying Machine Code Safety: Shallow Versus Deep Embedding / Martin Wildmoser ; Tobias Nipkow
Term Algebras with Length Function and Bounded Quantifier Alternation / Ting Zhang ; Henny B. Sipma ; Zohar Manna
Author Index
Error Analysis of Digital Filters Using Theorem Proving / Behzad Akbarpour ; Sofiène Tahar
Verifying Uniqueness in a Logical Framework / Penny Anderson ; Frank Pfenning
A Program Logic for Resource Verification / David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
16.

図書

図書
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
17.

図書

図書
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
18.

図書

図書
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…
19.

図書

図書
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
20.

図書

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

図書

図書
Sandro Etalle, Mirosław Truszczyński (eds.)
出版情報: Berlin : Springer, c2006  xiv, 474 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 4079
所蔵情報: loading…
22.

図書

図書
Maurizio Gabbrielli, Gopal Gupta (eds.)
出版情報: Berlin : Springer, c2005  xiv, 454 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3668
所蔵情報: loading…
23.

図書

図書
Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.)
出版情報: Berlin ; Tokyo : Springer, c2004  x, 408 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3085
所蔵情報: loading…
24.

図書

図書
David Basin, Michaël Rusinowitch(eds.)
出版情報: Berlin ; Tokyo : Springer, c2004  xii, 491 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3097 . Lecture notes in artificial intelligence
所蔵情報: loading…
25.

図書

図書
Warren A. Hunt Jr., Steven D. Johnson (eds.)
出版情報: Berlin : Springer, c2000  xi, 537 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1954
所蔵情報: loading…
26.

図書

図書
Michel Parigot, Andrei Voronkov (eds.)
出版情報: Berlin ; New York : Springer-Verlag, c2000  xiii, 486 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1955 . Lecture notes in artificial intelligence
所蔵情報: loading…
27.

図書

図書
Mark Aagaard, John Harrison (eds.)
出版情報: Berlin : Springer, c2000  ix, 533 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1869
所蔵情報: loading…
28.

図書

図書
David McAllester (ed.)
出版情報: Berlin : Springer, c2000  xiii, 512 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1831 . Lecture notes in artificial intelligence
所蔵情報: loading…
29.

図書

図書
Roy Dyckhoff (ed.)
出版情報: Berlin : Springer, c2000  x, 440 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1847 . Lecture notes in artificial intelligence
所蔵情報: loading…
30.

図書

図書
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…
31.

図書

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

図書

図書
Thierry Coquand ... [et al.] (eds.)
出版情報: Berlin ; New York : Springer, c2000  193 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1956
所蔵情報: loading…
目次情報: 続きを見る
Specification and Verification of a Formal System for Structurally Recursive Functions / Andreas Abel
A Predicative Strong Normalisation Proof for a ?-Calculus with Interleaving Inductive Types / Thorsten Altenkirch
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and ?-Rule / Steffen van Bakel ; Franco Barbanera ; Maribel Fernandez
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar) / Gertrud Bauer ; Markus Wenzel
Specification of a Smart Card Operating System / Gustavo Betarte ; Cristina Cornes ; Nora Szasz ; Alvaro Tasistro
Implementation Techniques for Inductive Types in Plastic / Paul Callaghan ; Zhaohui Luo
A Co-inductive Approach to Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
Information Retrieval in a Coq Proof Library Using Type Isomorphisms / David Delahaye
Memory Management: An Abstract Formulation of Incremental Tracing / Healfdene Goguen ; Richard Brooksby ; Rod Burstall
The Three Gap Theorem (Steinhaus Conjecture) / Micaela Mayero
Formalising Formulas-as-Types-as-Objects / Qiao Haiyan
Author Index
Specification and Verification of a Formal System for Structurally Recursive Functions / Andreas Abel
A Predicative Strong Normalisation Proof for a ?-Calculus with Interleaving Inductive Types / Thorsten Altenkirch
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and ?-Rule / Steffen van Bakel ; Franco Barbanera ; Maribel Fernandez
33.

図書

図書
Herman Geuvers, Freek Wiedijk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  viii, 330 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2646
所蔵情報: loading…
34.

図書

図書
Franz Baader (ed.)
出版情報: Berlin ; Tokyo : Springer, c2003  xii, 502 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2741 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Invited Talk / Session 1:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke
Session 2
Equational Abstractions / José Meseguer ; Miguel Palomino ; Narciso Martí-Oliet
Deciding Inductive Validity of Equations / Jürgen Giesl ; Deepak Kapur
Automating the Dependency Pair Method / Nao Hirokawa ; Aart Middeldorp
An AC-Compatible Knuth-Bendix Order / Konstantin Korovin ; Andrei Voronkov
Session 3
The Complexity of Finite Model Reasoning in Description Logics / Carsten Lutz ; Ulrike Sattler ; Lidia Tendera
Optimizing a BDD-Based Modal Solver / Guoqiang Pan ; Moshe Y. Vardi
A Translation of Looping Alternating Automata into Description Logics / Jan Hladik
Session 4
Foundational Certified Code in a Metalogical Framework / Karl Crary ; Susmit Sarkar
Proving Pointer Programs in Higher-Order Logic / Farhad Mehta ; Tobias Nipkow
λ / Dimitri Hendriks ; Vincent van Oostrom
Subset Types and Partial Functions / Aaron Stump
Session 5
Reasoning about Quantifiers by Matching in the E-graphGreg Nelson
Session 6
A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols / Sumit Gulwani ; George C. Necula
Superposition Modulo a Shostak Theory / Harald Ganzinger ; Thomas Hillenbrand ; Uwe Waldmann
Canonization for Disjoint Unions of Theories / Sava Krstić ; Sylvain Conchon
Matching in a Class of Combined Non-disjoint Theories / Christophe Ringeissen
Session 7
Reasoning about Iteration in Gödel's Class Theory / Johan Gijsbertus Frederik Belinfante
Algorithms for Ordinal Arithmetic / Panagiotis Manolios ; Daron Vroon
Certifying Solutions to Permutation Group Problems / Arjeh Cohen ; Scott H. Murray ; Martin Pollet ; Volker Sorge
System Descriptions / Session 8:
TRP++ 2.0: A Temporal Resolution Prover / Ullrich Hustadt ; Boris Konev
IsaPlanner: A Prototype Proof Planner in Isabelle / Lucas Dixon ; Jacques Fleuriot
'Living Book': - 'Deduction', 'Slicing', 'Interaction' / Peter Baumgartner ; Ulrich Furbach ; Margret Gross-Hardt ; Alex Sinner
The Homer System / Simon Colton ; Sophie Huczynska
CASC-19 Results / Session 9:
The CADE-19 ATP System Competition / Geoff Sutcliffe ; Christian Suttner
Proof Search and Proof Check for Equational and Inductive Theorems / Eric Deplagne ; Claude Kirchner ; Hélène Kirchner ; Quang Huy NguyenSession 10:
The New Waldmeister Loop at Work / Jean-Marie Gaillourdet ; Bernd Löuchner ; Hendrik SpiesSession 11:
About VeriFun / Christoph Walther ; Stephan Schweitzer
How to Prove Inductive Theorems? QuodLibet! / Jürgen Avenhaus ; Ulrich Kühler ; Tobias Schmidt-Samoa ; Claus-Peter Wirth
Reasoning about Qualitative Representations of Space and Time / Anthony G. CohnSession 12:
Session 13
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation / Jürgen Stuber
The Model Evolution Calculus / Cesare Tinelli
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms / Hans de Nivelle
Efficient Instance Retrieval with Standard and Relational Path Indexing / Alexandre Riazanov
Session 14
Monodic Temporal Resolution / Anatoly Degtyarev ; Michael Fisher
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae / Renate A. Schmidt
Schematic Saturation for Decision and Unification Problems / Christopher Lynch
Session 15
Unification Modulo ACUI Plus Homomorphisms/Distributivity / Siva Anantharaman ; Paliath Narendran ; Michael Rusinowitch
Source-Tracking Unification / Venkatesh Choppella ; Christopher T. Haynes
Optimizing Higher-Order Pattern Unification / Brigitte Pientka ; Frank Pfenning
Decidability of Arity-Bounded Higher-Order Matching / Manfred Schmidt-Schauß
Author Index
Invited Talk / Session 1:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke
Session 2
35.

図書

図書
David Basin, Burkhart Wolff (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  x, 366 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2758
所蔵情報: loading…
36.

図書

図書
Marta Cialdea Mayer, Fiora Pirri (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  x, 270 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2796 . Lecture notes in artificial intelligence
所蔵情報: loading…
37.

図書

図書
Franz Winkler (ed.)
出版情報: Berlin ; Tokyo : Springer, c2004  vi, 229 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2930 . Lecture notes in artificial intelligence
所蔵情報: loading…
38.

図書

図書
Catuscia Palamidessi (ed.)
出版情報: Berlin ; Tokyo : Springer, c2003  xii, 520 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2916
所蔵情報: loading…
39.

図書

図書
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
40.

図書

図書
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
41.

図書

図書
Didier Galmiche (ed.)
出版情報: Berlin ; Heidelberg : Springer, c1997  xi, 372 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1227 . Lecture notes in artificial intelligence
所蔵情報: loading…
42.

図書

図書
William McCune (ed.)
出版情報: Berlin ; New York : Springer, c1997  xiv, 462 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1249 . Lecture notes in artificial intelligence
所蔵情報: loading…
43.

図書

図書
Jan Komorowski, Jan Zytkow (eds.)
出版情報: Berlin ; Tokyo : Springer, c1997  ix, 396 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1263 . Lecture notes in artificial intelligence
所蔵情報: loading…
44.

図書

図書
Elsa L. Gunter, Amy Felty (eds.)
出版情報: Berlin ; Heidelberg : Springer, c1997  viii, 337 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1275
所蔵情報: loading…
45.

図書

図書
Georg Gottlob, Alexander Leitsch, Daniele Mundici, (eds.)
出版情報: Berlin ; Tokyo : Springer, c1997  viii, 348 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1289
所蔵情報: loading…
46.

図書

図書
Jacques Calmet, Carla Limongelli (eds.)
出版情報: Berlin : Springer, c1996  ix, 356 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1128
所蔵情報: loading…
47.

図書

図書
Stefano Berardi, Mario Coppo, (eds.)
出版情報: Berlin ; New York : Springer, c1996  x, 296 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1158
所蔵情報: loading…
48.

図書

図書
Mandayam Srivas, Albert Camilleri (eds.)
出版情報: Berlin : Springer, c1996  ix, 470 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1166
所蔵情報: loading…
49.

図書

図書
E. Thomas Schubert, Phillip J. Windley, James Alves-Foss (eds.)
出版情報: Berlin ; New York ; Tokyo : Springer-Verlag, c1995  viii, 400 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 971
所蔵情報: loading…
50.

図書

図書
Peter Dybjer, Bengt Nordström, Jan Smith (eds.)
出版情報: Berlin : Springer-Verlag, c1995  x, 202 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 996
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼