Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
- 17 September 1999
- book chapter
- Published by Springer Nature
- p. 323-340
- https://doi.org/10.1007/3-540-48256-3_22
Abstract
No abstract availableKeywords
This publication has 15 references indexed in Scilit:
- The formal verification of a pipelined double-precision IEEE floating-point multiplierPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Combining theorem proving and trajectory evaluation in an industrial environmentPublished by Association for Computing Machinery (ACM) ,1998
- Adding external decision procedures to HOL90 securelyPublished by Springer Nature ,1998
- The village telephone system: A case study in formal software engineeringPublished by Springer Nature ,1998
- Symbolic trajectory evaluationPublished by Springer Nature ,1997
- ML for the Working ProgrammerPublished by Cambridge University Press (CUP) ,1996
- A simple theorem prover based on symbolic trajectory evaluation and BDD'sIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995
- Model checking and abstractionACM Transactions on Programming Languages and Systems, 1994
- Linking BDD-based symbolic evaluation to interactive theorem-provingPublished by Association for Computing Machinery (ACM) ,1993
- A compiler for lazy MLPublished by Association for Computing Machinery (ACM) ,1984