Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This volume contains the proceedings of the second workshop on Computer Aided Verification, held at DIMACS, Rutgers University, June 18-21, 1990. Itfeatures theoretical results that lead to new or more powerful verification methods. Among these are advances in the use of binary decision diagrams, dense time, reductions based upon partial order representations and proof-checking in controller verification. The motivation for holding a workshop on computer aided verification was to bring together work on effective algorithms or methodologies for formal verification - as distinguished, say,from attributes of logics or formal languages. The considerable interest generated by the first workshop, held in Grenoble, June 1989 (see LNCS 407), prompted this second meeting. The general focus of this volume is on the problem of making formal verification feasible for various models of computation. Specific emphasis is on models associated with distributed programs, protocols, and digital circuits. The general test of algorithm feasibility is to embed it into a verification tool, and exercise that tool on realistic examples: the workshop included sessionsfor the demonstration of new verification tools.

Computer-aided design --- Digital integrated circuits --- Conception assistée par ordinateur --- Congresses --- Design and construction --- Data processing --- Congrès --- -Digital integrated circuits --- -Integrated circuits --- 681.3*C22 --- 681.3*C3 --- 681.3*F3 --- Chips (Electronics) --- Circuits, Integrated --- Computer chips --- Microchips --- Electronic circuits --- Microelectronics --- Digital electronics --- Integrated circuits --- CAD (Computer-aided design) --- Computer-assisted design --- Computer-aided engineering --- Design --- Verification --- -Congresses. --- Network protocols: protocol architecture; protocol verification --- Special-purpose and application-based systems: microprocessor/microcomputer; process control-, real-time, signal processing systems (Computer systems organization)--See also {681.3*J7} --- Logics and meanings of programs (Theory of computation) --- 681.3*F3 Logics and meanings of programs (Theory of computation) --- 681.3*C3 Special-purpose and application-based systems: microprocessor/microcomputer; process control-, real-time, signal processing systems (Computer systems organization)--See also {681.3*J7} --- 681.3*C22 Network protocols: protocol architecture; protocol verification --- Conception assistée par ordinateur --- Congrès --- Digital integrated circuits - Design adn construction - Data processing - congresses. --- Computer-aided design - Congresses. --- Logic, Symbolic and mathematical. --- Information theory. --- Logic design. --- Computer science. --- Software engineering. --- Mathematical Logic and Foundations. --- Theory of Computation. --- Logics and Meanings of Programs. --- Mathematical Logic and Formal Languages. --- Software Engineering. --- Special Purpose and Application-Based Systems. --- Computer software engineering --- Engineering --- Informatics --- Science --- Communication theory --- Communication --- Cybernetics --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Design, Logic --- Design of logic systems --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Verification -&delete& --- -Congresses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This book grew out of a NATO Advanced Study Institute summer school that was held in Antalya, TUrkey from 26 May to 6 June 1997. The purpose of the summer school was to expose recent advances in the formal verification of systems composed of both logical and continuous time components. The course was structured in two parts. The first part covered theorem-proving, system automaton models, logics, tools, and complexity of verification. The second part covered modeling and verification of hybrid systems, i. e. , systems composed of a discrete event part and a continuous time part that interact with each other in novel ways. Along with advances in microelectronics, methods to design and build logical systems have grown progressively complex. One way to tackle the problem of ensuring the error-free operation of digital or hybrid systems is through the use of formal techniques. The exercise of comparing the formal specification of a logical system namely, what it is supposed to do to its formal operational description-what it actually does!-in an automated or semi-automated manner is called verification. Verification can be performed in an after-the-fact manner, meaning that after a system is already designed, its specification and operational description are regenerated or modified, if necessary, to match the verification tool at hand and the consistency check is carried out.

Computer systems --- Systèmes informatiques --- Verification. --- Vérification --- Verification --- Systèmes informatiques --- Vérification --- Computer organization. --- Software engineering. --- Computers. --- Artificial intelligence. --- Computational complexity. --- Computer Systems Organization and Communication Networks. --- Software Engineering. --- Computation by Abstract Devices. --- Artificial Intelligence. --- Complexity. --- Complexity, Computational --- Electronic data processing --- Machine theory --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Logic machines --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Cybernetics --- Calculators --- Cyberspace --- Computer software engineering --- Engineering --- Organization, Computer --- Electronic digital computers