Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
From MaRDI portal
Publication:746778
DOI10.1007/s10703-015-0231-6zbMath1322.68121OpenAlexW1424940833MaRDI QIDQ746778
P. Madhusudan, Pranav Garg, Daniel Neider, Christof Löding
Publication date: 20 October 2015
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-015-0231-6
Related Items (2)
From invariant checking to invariant inference using randomized search ⋮ Non-well-founded deduction for induction and coinduction
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Learning regular sets from queries and counterexamples
- Automata, logics, and infinite games. A guide to current research
- Inference of finite automata using homing sequences
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
- Lazy Abstraction with Interpolants for Arrays
- SAT-Based Model Checking without Unrolling
- Abstraction Refinement for Quantified Array Assertions
- Efficient E-Matching for SMT Solvers
- Learning Minimal Separating DFA’s for Compositional Verification
- Decidable logics combining heap structures and data
- Array Abstractions from Proofs
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Language identification in the limit
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Automata theory and its applications
This page was built for publication: Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
