Automatic symbolic compositional verification by learning assumptions
From MaRDI portal
Publication:934713
DOI10.1007/s10703-008-0055-8zbMath1147.68052OpenAlexW2114114829MaRDI QIDQ934713
P. Madhusudan, Rajeev Alur, Wonhong Nam
Publication date: 30 July 2008
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-008-0055-8
Assume-guarantee reasoningFormal verificationSymbolic model checkingCompositional verificationHypergraph partitioningRegular language learning
Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Compositional Reasoning ⋮ Compositional Control Synthesis for Partially Observable Systems ⋮ Learning regular omega languages ⋮ Verification of asynchronous systems with an unspecified component ⋮ ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS ⋮ A framework for compositional verification of multi-valued systems via abstraction-refinement
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Learning regular sets from queries and counterexamples
- Learning regular languages from counterexamples
- Inference of finite automata using homing sequences
- Learning Deterministic Finite Automata from Smallest Counterexamples
- Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
- Graph-Based Algorithms for Boolean Function Manipulation
- An Efficient Heuristic Procedure for Partitioning Graphs
- Parallel Multilevel series k-Way Partitioning Scheme for Irregular Graphs
- Synthesis of interface specifications for Java classes
- SAT-Based Compositional Verification Using Lazy Learning
- Automated Assumption Generation for Compositional Verification
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Computer Aided Verification
- FM 2005: Formal Methods
This page was built for publication: Automatic symbolic compositional verification by learning assumptions
