Comparing Under and Over-Approximations of LTL Properties for Model Checking

Authors:

Open Access

Publisher website

1 November 2002

journal article
Published by Elsevier in Electronic Notes in Theoretical Computer Science

Vol. 76, 131-144
DOI:10.1016/s1571-0661(04)80790-4

Abstract

No abstract available

Keywords

SATISFIABILITY

This publication has 7 references indexed in Scilit:

Using XML to implement abstraction for Model Checking
2002
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs
2001
Counterexample-Guided Abstraction Refinement
2000
The model checker SPIN
IEEE Transactions on Software Engineering, 1997
Abstract interpretation of reactive systems
ACM Transactions on Programming Languages and Systems, 1997
Model checking and abstraction
ACM Transactions on Programming Languages and Systems, 1994
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
1977