Cited in
(99)- Quick specifications for the busy programmer
- On invariant checking
- Verifying array manipulating programs with full-program induction
- SeLoger
- Survey on mining signal temporal logic specifications
- Model checking merged program traces
- Dynamic inference of polymorphic lock types
- Symbolic abstract contract synthesis in a rewriting framework
- White-Box Testing by Combining Deduction-Based Specification Extraction and Black-Box Testing
- 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
- From invariant checking to invariant inference using randomized search
- Collaborative verification and testing with explicit assumptions
- A versatile concept for the analysis of loops
- Active learning for extended finite state machines
- Test-data generation for control coverage by proof
- Reflexive transitive invariant relations: A basis for computing loop functions
- How the design of JML accommodates both runtime assertion checking and formal verification
- Policy-centric protection of OS kernel from vulnerable loadable kernel modules
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Automata Learning through Counterexample Guided Abstraction Refinement
- Beaver
- Valigator
- jContractor
- Symstra
- WoLFram
- GeoSteiner
- Omnibus
- Cheddar
- ClawZ
- JCML
- Eclat
- Korat
- JUnit
- iFEST
- SANTE
- XMPP
- Rostra
- Cetus
- SATORI
- libalf
- LearnLib
- Ymer
- HANNIBAL
- Pinapa
- PASSAT
- LOOP
- ArgoUML
- tptp2X
- LOOPUS
- JCrasher
- AspectC++
- DynaMate
- ADABU
- RALib
- MuACOsm
- c2i
- Houdini
- PySMT
- VS3
- Zelus
- CodeHint
- KindSpec
- JSketch
- Sigma*
- SyPet
- Jessie
- IDP3
- Falcon
- FlashExtract
- IODINE
- BlinkFill
- ANNA
- Rely
- KERNELC
- SOBER
- Mathematics for reasoning about loop functions
- Verification and falsification of programs with loops using predicate abstraction
- JCML: A specification language for the runtime verification of Java card programs
- Learning register automata: from languages to program structures
- Specification and runtime verification of Java card programs
- Locust
- AALpy
- Code2Inv
- DeepLog
- Texada
- CLN2INV
- 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
- Clang Static Analyzer
This page was built for software: Daikon
