Mandrykin Mikhail Usamovich

Publications in Math-Net.Ru

1. Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT
   
   Proceedings of ISP RAS, 33:4 (2021),  177–194
2. Verified Isabelle/HOL tactic for the theory of bounded integers based on quantifier instantiation and SMT
   
   Proceedings of ISP RAS, 32:2 (2020),  107–124
3. Formal verification of Linux kernel library functions
   
   Proceedings of ISP RAS, 29:6 (2017),  49–76
4. Predicate abstractions memory modeling method with separation into disjoint regions
   
   Proceedings of ISP RAS, 29:4 (2017),  203–216
5. Survey of memory modeling methods in static verification tools
   
   Proceedings of ISP RAS, 29:1 (2017),  195–230
6. Modeling memory with uninterpreted functions for predicate abstractions
   
   Proceedings of ISP RAS, 27:5 (2015),  117–142
7. Towards deductive verification of C programs with shared data
   
   Proceedings of ISP RAS, 27:4 (2015),  49–68