Predator
From MaRDI portal
Cited in
(44)- Unified reasoning about robustness properties of symbolic-heap separation logic
- SeLoger
- Model checking for symbolic-heap separation logic with inductive predicates
- scientific article; zbMATH DE number 7350781 (Why is no real title available?)
- Shape neutral analysis of graph-based data-structures
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- An extension of lazy abstraction with interpolation for programs with arrays
- Semantic-directed clumping of disjunctive abstract states
- MPI-CHECK
- Cseq
- Gauss
- SMCHR
- LLBMC
- SLAyer
- YASM
- FixBag
- Threader
- SIMGRID
- MoonWalker
- Lazy-CSeq
- THOR
- LCTD
- coreStar
- Cyclist
- Infer
- EUREKA
- BoogiePL
- MemCAD
- SimGridMC
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Slide
- LCT
- LCTD: test-guided proofs for C programs on LLVM
- Locust
- The tree width of separation logic with recursive definitions
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Combining model checking and data-flow analysis
- Forest automata for verification of heap manipulation
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- Deciding entailments in inductive separation logic with tree automata
- Learning shape analysis
This page was built for software: Predator
