Verification and Validation and Artificial Intelligence
Advances in computersPublished 1 January 2005
Tim Menzies, Charles Pecheur
Citations75
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
There are enough alternative readily-available methods that enable the V&V of AI software, as it is shown in this article.
Abstract
Artifical Intelligence (AI) is useful. AI can deliver more functionality for reduced cost. AI should be used more widely but won’t be unless developers can trust adapative, nondeterministic, or complex AI systems. Verification and validation is one method used by software analysts to gain that trust. AI systems have features that make them hard to check using conventional V&V methods. Nevertheless, as we show in this article, there are enough alternative readily-available methods that enable the V&V of AI software.
Keywords
Computer Science
Choice Reviews OnlineGenetic algorithms in search, optimization, and machine learning
49,278 Citations1989
This book brings together the computer techniques, mathematical tools, and research results that will enable both students and practitioners to apply genetic algorithms to problems in many fields.
ScienceOptimization by Simulated Annealing
44,600 Citations1983Scott Kirkpatrick, C. D. Gelatt +1 more
A detailed analogy with annealing in solids provides a framework for optimization of the properties of very large and complex systems.
BiometricsClassification and Regression Trees.
23,841 Citations1984Alexander Gordon, Leo Breiman +3 more
C4.5: Programs for Machine Learning
23,665 Citations1992J. R. Quinlan
A complete guide to the C4.5 system as implemented in C for the UNIX environment, which starts from simple core learning methods and shows how they can be elaborated and extended to deal with typical problems such as missing data and over hitting.
Machine LearningInduction of Decision Trees
14,815 Citations1986J. R. Quinlan
This paper summarizes an approach to synthesizing decision trees that has been used in a variety of systems, and it describes one such system, ID3, in detail, which is described in detail.
Programs for Machine Learning
5,794 Citations1994Steven L. Salzberg, Alberto M. Segre
In his new book, C4.5: Programs for Machine Learning, Quinlan has put together a definitive, much needed description of his complete system, including the latest developments, which will be a welcome addition to the library of many researchers and students.
Communications of the ACMOn the criteria to be used in decomposing systems into modules
4,674 Citations1972David Lorge Parnas
IEEE Transactions on Software EngineeringThe model checker SPIN
3,736 Citations1997Gerard J. Holzmann
An overview of the design and structure of the verifier, its theoretical foundation, and an overview of significant practical applications are given.
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
CERN Document Server (European Organization for Nuclear Research)Software architecture: perspectives on an emerging discipline
2,966 Citations1996Mary Shaw, David Garlan
1. architectural Styles, 2. Shared Information Systems, 3. Education of Software Architects, 4. Architectural Design Guidance.
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Artificial IntelligenceThe knowledge level
2,484 Citations1982Allen Newell
A theory of the nature of knowledge is proposed, namely, that there is another computer system level immediately above the symbol (or program) level and knowledge itself is the processing medium at this level and the principle of rationality plays a central role.
Choice Reviews OnlineThe cathedral and the bazaar: musings on Linux and open source by an accidental revolutionary
2,294 Citations2002
Lecture notes in computer scienceSymbolic Model Checking without BDDs
2,113 Citations1999Armin Biere, Alessandro Cimatti +2 more
This paper shows how boolean decision procedures, like Stalmarck's Method or the Davis & Putnam Procedure, can replace BDDs, and introduces a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability.
ACM Computing SurveysSymbolic Boolean manipulation with ordered binary-decision diagrams
2,019 Citations1992Randal E. Bryant
The OBDD data structure is described and a number of applications that have been solved by OBDd-based symbolic analysis are surveyed.
Machine LearningThe CN2 Induction Algorithm
2,015 Citations1989Peter Clark, Tim Niblett
A description and empirical evaluation of a new induction system, CN2, designed for the efficient induction of simple, comprehensible production rules in domains where problems of poor description language and/or noise may be present.
Principles of Program Analysis
1,828 Citations1999Flemming Nielson, Hanne Riis Nielson +1 more
This book is unique in providing an overview of the four major approaches to program analysis: data flow analysis, constraint-based analysis, abstract interpretation, and type and effect systems.
Software Cost Estimation With Cocomo II
1,751 Citations2000Barry Boehm, Chris Abts +7 more
This book will show professional developers how to use the COCOMO (Cost Comparison Model) II model developed by Dr. Boehm at USC to generate end-to-end cost analysis figures for software development projects.
Artificial IntelligenceAn assumption-based TMS
1,745 Citations1986Johan de Kleer
A new view of problem solving motivated by a new kind of truth maintenance system based on manipulating assumption sets is presented, which is possible to work effectively and efficiently with inconsistent information, context switching is free, and most backtracking is avoided.
Software Reliability: Measurement, Prediction, Application
1,678 Citations1987Donald Musa, A. Iannino +1 more
Revised and updated for professional software engineers, systems analysts and project managers, this book provides key concepts of software reliability and practical solutions for measuring reliability.
Safeware: System Safety and Computers
1,665 Citations1995Nancy G. Leveson
Computers & Mathematics with ApplicationsKnowledge engineering and management: The commonKADS methodology
1,492 Citations2000
The CommonKADS methodology, developed over the last decade by an industry-university consortium led by the authors, is used and makes as much use as possible of the new UML notation standard.
Patterns in property specifications for finite-state verification
1,421 Citations1999Matthew B. Dwyer, George S. Avrunin +1 more
A survey of available specifications found that most are instances of the proposed pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification.
Automated Software EngineeringModel Checking Programs
1,353 Citations2003Willem Visser, Klaus Havelund +3 more
A verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing, and uses state compression to handle large states and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space.
Lecture notes in computer scienceSpecification and verification of concurrent systems in CESAR
1,277 Citations1982J. P. Queille, Joseph Sifakis
By an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications, is illustrated.
ACM Transactions on Programming Languages and SystemsModel checking and abstraction
1,217 Citations1994Edmund M. Clarke, Orna Grümberg +1 more
Using techniques similar to those involved in abstract interpretation, an abstract model of a program is constructed without ever examining the corresponding unabstracted model, and it is shown how this abstract model can be used to verify properties of the original program.
A new method for solving hard satisfiability problems
1,183 Citations1992Bart Selman, Hector J. Levesque +1 more
A greedy local search procedure called GSAT is introduced for solving propositional satisfiability problems and its good performance suggests that it may be advantageous to reformulate reasoning tasks that have traditionally been viewed as theorem-proving problems as model-finding tasks.
Machine LearningExplanation-Based Generalization: A Unifying View
1,175 Citations1986Tom M. Mitchell, Richard M. Keller +1 more
This paper proposes a general, domain-independent mechanism, called EBG, that unifies previous approaches to explanation-based generalization, and is illustrated in the context of several example problems, and used to contrast several existing systems for explanation- based generalization.
The MIT Press eBooksAlgorithmic Program Debugging
1,094 Citations1983Ehud Shapiro
An algorithm that can fix a bug that has been identified, and integrate it with the diagnosis algorithms to form an interactive debugging system that can debug programs that are too complex for the Model Inference System to synthesize.
IEEE Transactions on Software EngineeringA critique of software defect prediction models
1,032 Citations1999Norman Fenton, Martin Neil
H holistic models for software defect prediction, using Bayesian belief networks, are recommended as alternative approaches to the single-issue models used at present and research into a theory of "software decomposition" is argued for.
Where the really hard problems are
1,021 Citations1991Peter Cheeseman, Bob Kanefsky +1 more
It is shown that NP-complete problems can be summarized by at least one "order parameter", and that the hard problems occur at a critical value of such a parameter.
Pushing the envelope: planning, propositional logic, and stochastic search
845 Citations1996Henry Kautz, Bart Selman
Stochastic methods are shown to be very effective on a wide range of scheduling problems, but this is the first demonstration of its power on truly challenging classical planning instances.
Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem
771 Citations1996Patrice Godefroid, Jan Van Leeuwen +3 more
Machine LearningExplanation-based generalization: A unifying view
718 Citations1986Tom M. Mitchell, Richard M. Keller +1 more
This paper proposes a general, domain-independent mechanism, called EBG, that unifies previous approaches to explanation-based generalization, and is illustrated in the context of several example problems, and used to contrast several existing systems for explanation- based generalization.
Artificial IntelligenceRemote Agent: to boldly go where no AI system has gone before
700 Citations1998Nicola Muscettola, P. Pandurang Nayak +2 more
The Remote Agent is described, a specific autonomous agent architecture based on the principles of model-based programming, on-board deduction and search, and goal-directed closed-loop commanding, that takes a significant step toward enabling this future of space exploration.
Choice Reviews OnlineEmpirical methods for artificial intelligence
637 Citations1996
Empirical research exploratory data analysis basic issues in experiment design hypothesis testing and estimation computer-intensive statistical methods performance assessment explaining performance - interactions and dependencies modelling tactics for generalization.
IEEE Transactions on Software EngineeringAdvances in software inspections
627 Citations1986Michael Fagan
Studies and experiences are presented which enhance the use of the inspection process and improve its contribution to development of defect-free software on time and at lower cost.
Lecture notes in computer scienceNuSMV: A New Symbolic Model Verifier
605 Citations1999Alessandro Cimatti, Emma L. Clarke +2 more
NUSMV, a new symbolic model checker developed as a joint project between Carnegie Mellon University and Istituto per la Ricerca Scientifica e Tecnolgica (IRST), is described, a well structured, open, flexible and documented platform for model checking.
Knowledge AcquisitionKADS: a modelling approach to knowledge engineering
604 Citations1992Bob Wielinga, A.T. Schreiber +1 more
Five basic principles underlying the KADS approach are discussed, namely the introduction of partial models as a means to cope with the complexity of the knowledge engineering process and the importance of structure—preserving transformation of models of expertise into design and implementation.
ACM Transactions on Software Engineering and MethodologyAutomated consistency checking of requirements specifications
603 Citations1996Constance Heitmeyer, Ralph D. Jeffords +1 more
This article describes a formal analysis technique, called consistency checking, for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation.
Latin american journal of economicsRule Based Expert Systems: The Mycin Experiments of the Stanford Heuristic Programming Project (The Addison-Wesley series in artificial intelligence)
582 Citations1984Bruce G. Buchanan, Edward H. Shortliffe
Formal Methods in System DesignA stubborn attack on state explosion
572 Citations1992Antti Valmari
The LTL-preserving stubborn set method is presented for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications.
Journal of Systems and SoftwareSoftware reliability measurement
564 Citations1979Donald Musa
A theory of software reliability based on execution or cpu time, and a concomitant model of the testing and debugging process that permits execution time to be related to calendar time are outlined.
Machine LearningChunking in Soar: The Anatomy of a General Learning Mechanism
510 Citations1986John E. Laird, Paul S. Rosenbloom +1 more
The anatomy of chunking in Soar is examined and a new demonstration of its learning capabilities involving the acquisition and use of macro-operators is provided.
Formal Methods in System DesignBetter verification through symmetry
491 Citations1996C. Norris Ip, David L. Dill
This work provides a proof of the soundness of the new symmetry-based verification algorithm based on a definition of the formal semantics of a simple description language with scalarsets, and leads to an alternative characterization of data independence.
Systems and Software Verification: Model-Checking Techniques and Tools
490 Citations2001Béatrice Bérard, Michel Bidoit +5 more
The author provides a well written and basic introduction to the new technique model checking, which describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic asA formal language for behavioral properties, and model-checking algorithms.
A model-based approach to reactive self-configuring systems
489 Citations1996Brian C. Williams, P. Pandurang Nayak
Livingstone provides a reactive system that performs significant deduction in the sense/response loop by drawing on past experience at building fast propositional conflict-based algorithms for model-based diagnosis, and by framing a model- based configuration manager as a propositional feedback controller that generates focused, optimal responses.
IEEE Transactions on Software EngineeringMachine learning approaches to estimating software development effort
478 Citations1995Kannan Srinivasan, Douglas Fisher
Two methods of machine learning are described, which are used to build estimators of software development effort from historical data, which indicate that these techniques are competitive with traditional estimators on one dataset, but also illustrate that these methods are sensitive to the data on which they are trained.
DIGITAL.CSIC (Spanish National Research Council (CSIC))Components of expertise
476 Citations1990Luc Steels
A new synthesis is put forward in the form of a componential framework that stresses modularity and an analysis of the pragmatic constraints on the task.
Compositional model checking
471 Citations2003E. M. Clarke, David E. Long +1 more
The authors present a general framework for using additional interface processes to model the environment for a component and can guarantee that these properties will be preserved at the global level.
IEEE ExpertCommonKADS: a comprehensive methodology for KBS development
435 Citations1994Guus Schreiber, Tianrui Li +3 more
The aim of CommonKADS is to fill the need for a structured methodology for KBS projects by constructing a set of engineering models built with the organization and the application in mind.
Lecture notes in computer scienceRule-Based Runtime Verification
368 Citations2004Howard Barringer, Allen Goldberg +2 more
Eagles logic, Eagle, is implemented as a Java library and involves novel techniques for rule definition, manipulation and execution for finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time logics and forms of quantified temporal logics.
Oxford University Press eBooksThe Role of Abduction in Logic Programming
355 Citations1998Antonis Kakas, Robert Kowalski
The general framework of Abduction and its applications to Knowledge Assimilation and Default Reasoning is outlined; the argumentation-theoretic approach to the use of abduction as an interpretation for Negation as Failure is described.
Model checking programs
337 Citations2000Willem Visser, Klaus Havelund +2 more
Formal Methods in System DesignExploiting symmetry in temporal logic model checking
322 Citations1996E. M. Clarke, Reinhard Enders +2 more
What it means for a finite state system to be symmetric is formalized and techniques for reducing such systems when the transition relation is given explicitly in terms of states or symbolically as a BDD are described.
Lecture notes in computer scienceAn analysis of the interacting roles of population size and crossover in genetic algorithms
316 Citations1991Kenneth De Jong, William M. Spears
It is shown empirically that disruption analysis alone is not sufficient for selecting appropriate forms of crossover, but by taking into account the interacting effects of population size and crossover, a general picture begins to emerge.
Backdoors to typical case complexity
311 Citations2003Ryan Williams, Carla P. Gomes +1 more
This work proposes a new framework for studying the complexity of reasoning and constraint processing methods, which incorporates general structural properties observed in practical problem instances into the formal complexity analysis and introduces a notion of "backdoors", which are small sets of variables that capture the overall combinatorics of the problem instance.
Artificial IntelligenceInteractive transfer of expertise: Acquisition of new inference rules
299 Citations1979Randall Davis
The concept of meta-level knowledge is described and illustrations given of its utility in knowledge acquisition and its contribution to the more general issues of creating an intelligent program.
Information and Software TechnologyCan genetic programming improve software effort estimation? A comparative evaluation
299 Citations2001Colin J. Burgess, Martin Lefley
GP has the potential to be a valid additional tool for software effort estimation but set up and running effort is high and interpretation difficult, as it is for any complex meta-heuristic technique.
Lecture notes in computer scienceThe Temporal Rover and the ATG Rover
278 Citations2000Doron Drusinsky
The Temporal Rover is a specification based verification tool for applications written in C, C++, Java, Verilog and VHDL that generates executable code from LTL and MTL assertions written as comments in the source code.
AI MagazineAn Approach to Verifying Completeness and Consistency in a Rule-Based Expert System
276 Citations1982Motoi Suwa, A. Carlisle Scott +1 more
A program for verifying that a set of rules in an expert system comprehensively spans the knowledge of a specialized domain is described, suggesting a general mechanism for correcting many problems with knowledge base completeness and consistency before they can cause performance errors.
Studies in computer science and artificial intelligenceKnowledge Base Verification
252 Citations1989W. A. Perkins, Thomas J. Laffey +2 more
Several tools and techniques for validating a knowledge base are described, with emphasis on the rule checker, which has saved engineers from many hours of tedious debugging.
Communications of the ACMTask-structure analysis for knowledge modeling
245 Citations1992B. Chandrasekaran, Todd R. Johnson +1 more
This article outlines the modeling approach in terms of a task-structure, which recursively links a task to alternative methods and to their subtasks, and emphasis is on the notion of modeling domain knowledge using tasks and methods as mediating concepts.
What we have learned about fighting defects
244 Citations2002Forrest Shull, Victor R. Basili +8 more
The results to date of a series of e-Workshops on software defect reduction are discussed, and reformulated heuristics can be useful both to researchers and practitioners, for pointing out gaps in the current state of the knowledge.
Artificial IntelligenceThe organization of expert systems, a tutorial
235 Citations1982Mark Stefik, Jan S. Aikins +5 more
Artificial IntelligenceExtending the ATMS
222 Citations1986Johan de Kleer
This paper shows how the basic ATMS is extended to handle defaults and disjunctions of assumptions, which are used to encode disjunction of nodes, nonmonotonic justifications, normal defaults, nonnormal defaults, and arbitrary propositional formulas.
Artificial IntelligenceLocating the phase transition in binary constraint satisfaction problems
219 Citations1996Barbara M. Smith, Martin Dyer
It is shown that the variance of the number of solutions can be used to set bounds on the phase transition and to indicate the accuracy of the prediction.
Artificial Intelligence ReviewExpert system verification and validation: a survey and tutorial
199 Citations1993Robert M. O’Keefe, Daniel E. O’Leary
This paper surveys the issues, methods and techniques for verifying and validating expert systems, and reviews of validation methods for validating both the components of a system and the system as a whole.
Lecture notes in computer scienceExploiting symmetry in temporal logic model checking
196 Citations1993E. M. Clarke, Thomas Filkorn +1 more
Experiment al Results on the Application of Sat isfiability Algorithms to Scheduling Problems
195 Citations1994James M. Crawford, Andrew B. Baker
Artificial IntelligencePrototypical knowledge for expert systems
194 Citations1983Janice S. Aikins
A system that uses a representation of prototypical knowledge to guide computer consultations, and to focus the application of production rules used to represent inferential knowledge in the domain is presented.
AI MagazineR1 Revisited: Four Years in the Trenches
185 Citations1984Judith Bachant, John McDermott
R1's knowledge has increased substantially and its usefulness to Digital continues to grow and this article describes what is involved in extending R1's performance during the four year period.
Assumption generation for software component verification
184 Citations2002Dimitra Giannakopoulou, Corina S. Păsăreanu +1 more
This work defines a framework that brings a new dimension to model checking of software components that is implemented in the LTSA tool and has been applied to the analysis of a NASA application.
Lecture notes in computer scienceUsing Runtime Analysis to Guide Model Checking of Java Programs
179 Citations2000Klaus Havelund
Two runtime analysis algorithms, an existing data race detection algorithm and a new deadlock detection algorithm, have been implemented to analyze Java programs to generate a set of warnings which can be used to guide a model checker, thereby reducing the search space.
Electronic Notes in Theoretical Computer ScienceMonitoring Java Programs with Java PathExplorer
173 Citations2001Klaus Havelund, Grigore Roşu
Recent work on the development of Java PathExplorer (\JPaXX), a tool for monitoring the execution of Java programs, can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.
Communications of the ACMApplications of inductive logic programming
166 Citations1995Ivan Bratko, Stephen Muggleton
Attribute-based learning is limited to non-relational descriptions of objects in the sense that the learned descriptions do not specify relations among the objects' parts, and the lack of relations makes the concept description language inappropriate for some domains.
National Conference on Artificial IntelligenceAssessing the maintainability of XCON-in-RIME: coping with the problems of a VERY large rule-base
161 Citations1987Elliot Soloway, Judy Bachant +1 more
Evaluated the potential for enhanced maintainability of XCON-in-RIME over XCON, a rule-based expert system that configures computer systems that is increasingly becoming more difficult to change.
Artificial IntelligenceTask modeling with reusable problem-solving methods
158 Citations1995Henrik Eriksson, Yuval Shaḥar +3 more
This work compares configuration of the board-game method to that of a chronological-backtracking problem-solving method for the same application tasks (for example, towers of Hanoi and the Sisyphus room-assignment problem), and examines how method designers can specialize problem-Solving methods by making ontological commitments to certain classes of tasks.
Choosing between two learning algorithms based on calibrated tests
146 Citations2003Remco Bouckaert
It is posed the case that reuse of the same data causes the effective degrees of freedom to be much lower than theoretically expected, and how to calibrate the effective degree of freedom empirically for various tests is shown.
Artificial IntelligenceModel construction operators
142 Citations1992William J. Clancey
This paper reviews different ways of describing expert system reasoning, emphasizing the use of simple logic, set, and graph notations for making dimensional analyses of modeling languages and inference methods.
Consistency checking of SCR-style requirements specifications
138 Citations2002Constance Heitmeyer, B. Labaw +1 more
A class of formal analysis called consistency checking that mechanically checks requirements specifications, expressed in the SCR tabular notation, for application independent properties, for domain coverage, type correctness, and determinism is described.
The Knowledge Engineering ReviewKnowledge maintenance: the state of the art
135 Citations1999Tim Menzies
This work reviews systems that contribute to these 7*5 = 35 types of knowledge maintenance to make the following conclusions.
Lessons learned from 25 years of process improvement
134 Citations2002Victor R. Basili, F. E. Mcgarry +2 more
The history of the SEL is described, the research that was conducted, how the understanding of software process improvement evolved, and a set of lessons learned and hypotheses that should enable future groups to learn from and improve on their quarter century of experiences are described.
Precise and efficient static array bound checking for large embedded C programs
121 Citations2004Arnaud Venet, Guillaume Brat
The design and implementation of a static array-bound checker for a family of embedded programs: the flight control software of recent Mars missions, which is the first distributed implementation of static analysis algorithms.
Lecture notes in computer scienceVerification of Java Programs Using Symbolic Execution and Invariant Generation
118 Citations2004Corina S. Păsăreanu, Willem Visser
This work presents a novel iterative technique that uses invariant strengthening and approximation for discovering loop invariants automatically and it was used for the verification of several non-trivial Java programs.
Formal verification of diagnosability via symbolic model checking
117 Citations2003Alessandro Cimatti, Charles Pecheur +1 more
This paper addresses the formal verification of diagnosis systems by looking for pairs of scenarios that are observationally indistinguishable, but lead to situations that are required to be distinguished, and reduces the problem to a model checking problem.
ComputerComputing practices - Data mining for very busy people
108 Citations2003Tim Menzies, Ying Hu
The authors take a different approach and assume that busy people don't need, or can't use complex models, and want only the data they need to achieve the most benefits.
Artificial IntelligenceAutomatic knowledge base refinement for classification systems
104 Citations1988Allen Ginsberg, Sholom M. Weiss +1 more
The progress made since the original SEEK program is described, and methods for estimating the expected gain in performance for a refined knowledge base and prospective test cases are described and some results are reported.
Computational IntelligenceOn the consistency of knowledge bases: the COVADIS system
103 Citations1988Marie‐Christine Rousset
This paper describes a complete method to prove the consistency (or the inconsistency) of knowledge bases that is implemented in the COVADIS system and is defined in the framework of classical logic.
Artificial IntelligenceExplanation-based generalisation = partial evaluation
102 Citations1988Frank van Harmelen, Alan Bundy
It is argued that explanation-based generalisation as recently proposed in the machine learning literature is essentially equivalent to partial evaluation, a well-known technique in the functional and logic programming literature.
AI MagazineR1: The Formative Years
100 Citations1981John McDermott
R1 is a rule-based program that configures VAX-11 computer systems and produces a number of diagrams showing the spatial and logical relationships among the 90 or so components that typically constitute a system.
Expert Systems with ApplicationsA report on the Expert Systems Validation Associate (EVA)
95 Citations1990C. L. Chang, J.B. Combs +1 more
The goal of EVA is to build an integrated set of generic tools to validate any knowledge-based system written in any expert system shell such as ART, CLIPS, OPS5, KEE and other.
Validating requirements for fault tolerant systems using model checking
88 Citations2002Frank Schneider, Steve Easterbrook +2 more
Model checking is shown to be an effective tool in validating the behavior of a fault tolerant embedded spacecraft controller and an effective approach for maintaining fidelity between a co-evolving specification and an implementation.
Converging on the optimal attainment of requirements
87 Citations2003Martin S. Feather, Tim Menzies
A novel approach to requirements optimization that focuses human experts' attention on a relatively few decisions and makes them aware of major alternatives and each iteration allows experts to select from among the major alternatives.
Formal Methods in System DesignExperimental Evaluation of Verification and Validation Tools on Martian Rover Software
85 Citations2004Guillaume Brat, Doron Drusinsky +8 more
The study consisted of a controlled experiment where three technologies were compared to traditional testing with respect to their ability to find seeded errors in a prototype Mars Rover controller and confirmed the belief that advanced tools can outperform testing when trying to locate concurrency errors.
…