### Abstract

For an infinite-state concurrent system with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s∈→∈s' are witnessed by concrete transitions between states in satisfying the respective sets of predicates s and s'. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method - based on rewriting, semantic unification, and variant narrowing - to automatically generate a predicate abstraction when the formal specification of is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

Original language | English (US) |
---|---|

Title of host publication | Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings |

Publisher | Springer-Verlag |

Pages | 61-76 |

Number of pages | 16 |

ISBN (Print) | 9783319089171 |

DOIs | |

State | Published - Jan 1 2014 |

Event | 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: Jul 14 2014 → Jul 17 2014 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 8560 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 |
---|---|

Country | Austria |

City | Vienna |

Period | 7/14/14 → 7/17/14 |

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'Predicate abstraction of rewrite theories'. Together they form a unique fingerprint.

## Cite this

*Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings*(pp. 61-76). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8560 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-08918-8_5