Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
- 20 September 2002
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- Microarchitecture Verification by Compositional Model CheckingLecture Notes in Computer Science, 2001
- ChaffPublished by Association for Computing Machinery (ACM) ,2001
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logicACM Transactions on Computational Logic, 2001
- Regular Model CheckingLecture Notes in Computer Science, 2000
- Boolean Satisfiability with Transitivity ConstraintsLecture Notes in Computer Science, 2000
- On-the-fly analysis of systems with unbounded, lossy FIFO channelsLecture Notes in Computer Science, 1998
- Symbolic model checking of infinite state systems using presburger arithmeticLecture Notes in Computer Science, 1997
- Validity checking for combinations of theories with equalityPublished by Springer Nature ,1996
- Automatic verification of pipelined microprocessor controlLecture Notes in Computer Science, 1994
- PVS: A prototype verification systemLecture Notes in Computer Science, 1992