Learning Minimal Separating DFA’s for Compositional Verification

DOI10.1007/978-3-642-00768-2_3zbMath1234.68166OpenAlexW98666333MaRDI QIDQ3617752

Yih-Kuen Tsay, Azadeh Farzan, Bow-Yaw Wang, Yu-Fang Chen, Edmund M. Clarke

Publication date: 31 March 2009

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00768-2_3

Mathematics Subject Classification ID

Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Assume, Guarantee or Repair, Learning union of integer hypercubes with queries (with applications to monadic decomposition), Minimal consistent DFA revisited, Compositional Reasoning, Automated circular assume-guarantee reasoning, Automated program repair using formal verification techniques, Parametric random generation of deterministic tree automata, A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees, Fundamental results for learning deterministic extended finite state machines from queries, A multi-parameter analysis of hard problems on deterministic finite automata, Automatically inferring loop invariants via algorithmic learning, A sufficient condition to polynomially compute a minimum separating DFA, Optimal state reductions of automata with partially specified behaviors, Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys, Automated Circular Assume-Guarantee Reasoning, Learning Minimal Separating DFA’s for Compositional Verification, Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists, A novel learning algorithm for Büchi automata based on family of DFAs and classification trees, Random Generation of Deterministic Tree (Walking) Automata, Learning algorithms, A framework for compositional verification of multi-valued systems via abstraction-refinement

Cites Work

• Unnamed Item
• Learning regular sets from queries and counterexamples
• Inference of finite automata using homing sequences
• Inferring Network Invariants Automatically
• Learning Minimal Separating DFA’s for Compositional Verification
• SAT-Based Compositional Verification Using Lazy Learning
• Automated Assumption Generation for Compositional Verification
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Computer Aided Verification
• FM 2005: Formal Methods
• Refining Interface Alphabets for Compositional Verification
• Optimized L*-Based Assume-Guarantee Reasoning