The Daikon system for dynamic detection of likely invariants

DOI10.1016/J.SCICO.2007.01.015MaRDI QIDQ2463543zbMATH OpenOpenAlexFDO

Authors Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Matthew S. Tschantz, Chen Xiao, Carlos Gabriel Pacheco

Publication date 12 December 2007

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2007.01.015

zbMATH Keywords

Daikondynamic analysisdynamic invariant detectioninductive logic programminginferencelikely invariantprogram understandingspecificationspecification mining

Mathematics Subject Classification ID

Logic programming (68N17) Theory of software (68N99) Learning and adaptive systems in artificial intelligence (68T05)

Recommendations

• Discovering invariants via simple component analysis
• Heuristic search for invariants for one class of programs. 6
• Identifying dynamic data structures by learning evolving patterns in memory
• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• Discovery of invariant equalities in programs over data fields

Cited in

(36)

• Mathematics for reasoning about loop functions
• Daikon
• Automated verification of functional correctness of race-free GPU programs
• Relational program reasoning using compiler IR
• Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow
• Survey on mining signal temporal logic specifications
• Programming by predicates: a formal model for interactive synthesis
• Towards light-weight probabilistic model checking
• A formalization of programs in first-order logic with a discrete linear order
• Automatic inference of access permissions
• Inferring canonical register automata
• Analyzing Array Manipulating Programs by Program Transformation
• Using fault screeners for software error detection
• On invariant checking
• A versatile concept for the analysis of loops
• Learning register automata: from languages to program structures
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• A survey of opponent modeling in adversarial domains
• Verifying array manipulating programs with full-program induction
• Model checking merged program traces
• From invariant checking to invariant inference using randomized search
• Quick specifications for the busy programmer
• Reflexive transitive invariant relations: A basis for computing loop functions
• Bootstrapping library-based synthesis
• Data-Driven Invariant Learning for Probabilistic Programs
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• Abstraction Modulo Stability for Reverse Engineering
• An active learning approach to synthesizing program contracts
• Invariant relations for affine loops
• FlexFringe: modeling software behavior by learning probabilistic automata
• Data-driven invariant learning for probabilistic programs
• Abstraction modulo stability
• \(SL^{\lambda}\): a scalable algorithm for register automata learning
• Active learning for extended finite state machines
• Test-data generation for control coverage by proof
• Verification and falsification of programs with loops using predicate abstraction

Describes a project that uses

Uses Software

• SIMPLIFY
• ESC/Java
• PERL
• GeoSteiner
• JML
• Eclat

This page was built for publication: The Daikon system for dynamic detection of likely invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2463543)