Daikon

swMATH4319MaRDI QIDQ16498FDOQ16498

Author name not available (Why is that?)

Described by source

• The Daikon system for dynamic detection of likely invariants

Cited In (36)

• Verifying array manipulating programs with full-program induction
• On invariant checking
• Survey on mining signal temporal logic specifications
• Model checking merged program traces
• White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
• Dynamic inference of polymorphic lock types
• Symbolic abstract contract synthesis in a rewriting framework
• Towards light-weight probabilistic model checking
• A formalization of programs in first-order logic with a discrete linear order
• A Hybrid Approach to Modeling Biological Systems
• Automated verification of functional correctness of race-free GPU programs
• Collaborative verification and testing with explicit assumptions
• From invariant checking to invariant inference using randomized search
• A versatile concept for the analysis of loops
• Active learning for extended finite state machines
• Test-data generation for control coverage by proof
• How the design of JML accommodates both runtime assertion checking and formal verification
• Reflexive transitive invariant relations: A basis for computing loop functions
• Policy-centric protection of OS kernel from vulnerable loadable kernel modules
• Automata Learning through Counterexample Guided Abstraction Refinement
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Mathematics for reasoning about loop functions
• Verification and falsification of programs with loops using predicate abstraction
• Specification and runtime verification of Java card programs
• JCML: A specification language for the runtime verification of Java card programs
• Learning register automata: from languages to program structures
• Using fault screeners for software error detection
• Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow
• Specification and verification challenges for sequential object-oriented programs
• Automatic inference of access permissions
• Programming by predicates: a formal model for interactive synthesis
• Relational program reasoning using compiler IR
• Inferring canonical register automata
• Robustness and usability in modern design flows
• Learning shape analysis
• Quick specifications for the busy programmer

This page was built for software: Daikon