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
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
organized by CHEOPS ESPRIT BRA 3215 ; sponsored by IMEC and the Commission of the European Communities, Leuven, Belgium, 21-24 September 1992 ; edited by Luc J.M. Claesen, Michael J.C. Gordon
出版情報:
Amsterdam ; New York : North-Holland, 1993 xiii, 568 p. ; 23 cm
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
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
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
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
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
図書
