Loading...
Please wait, while we are loading the content...
Similar Documents
Refining model checking by abstract interpretation (1999)
| Content Provider | CiteSeerX |
|---|---|
| Author | Cousot, Patrick |
| Abstract | Abstract. Formal methods combining abstract interpretation and model-checking have been considered for automated analysis of software. In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/-calculus model-checking can be directly applied. The paper proposes two improvements of abstract model-checking which can be applied to infinite abstract transition systems: – A new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction; – When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyses for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking. |
| File Format | |
| Journal | Automated Software Engineering |
| Journal | AUTOMATED SOFTWARE ENGINEERING |
| Publisher Date | 1999-01-01 |
| Access Restriction | Open |
| Subject Keyword | Formal Method Backwards Abstract Fixed-point Model-checking Computation Abstract Model-checking Partial Result Backward Analysis Abstract Transition System Classical Combination Abstract Interpretation Infinite Transition System Automated Analysis Minimum Maximum Path-length Problem Model Checking Finite Approximation Backward Abstract Interpretation Temporal-logic Calculus Model-checking Universal Safety Concrete State Space New Combination Precise Result |
| Content Type | Text |
| Resource Type | Article |
