Daikon

swMATH4319MaRDI QIDQ16498

No author found.

Described by source

• The Daikon system for dynamic detection of likely invariants

Related Items (36)

A formalization of programs in first-order logic with a discrete linear order ⋮ Unnamed Item ⋮ Verifying Array Manipulating Programs with Full-Program Induction ⋮ Automatic Inference of Access Permissions ⋮ Inferring Canonical Register Automata ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ Symbolic abstract contract synthesis in a rewriting framework ⋮ On invariant checking ⋮ Automated verification of functional correctness of race-free GPU programs ⋮ Relational program reasoning using compiler IR ⋮ JCML: A specification language for the runtime verification of Java card programs ⋮ Quick specifications for the busy programmer ⋮ A versatile concept for the analysis of loops ⋮ Learning register automata: from languages to program structures ⋮ Policy-Centric Protection of OS Kernel from Vulnerable Loadable Kernel Modules ⋮ Automata Learning through Counterexample Guided Abstraction Refinement ⋮ Collaborative Verification and Testing with Explicit Assumptions ⋮ From invariant checking to invariant inference using randomized search ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing ⋮ Specification and Runtime Verification of Java Card Programs ⋮ Model Checking Merged Program Traces ⋮ How the design of JML accommodates both runtime assertion checking and formal verification ⋮ Using Fault Screeners for Software Error Detection ⋮ A Hybrid Approach to Modeling Biological Systems ⋮ Active learning for extended finite state machines ⋮ Test-data generation for control coverage by proof ⋮ Programming by predicates: a formal model for interactive synthesis ⋮ Learning Shape Analysis ⋮ Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow ⋮ Mathematics for reasoning about loop functions ⋮ Towards light-weight probabilistic model checking ⋮ Dynamic inference of polymorphic lock types ⋮ Survey on mining signal temporal logic specifications

This page was built for software: Daikon