General

Profile

Mikhail Mandrykin

  • Login: misha_bear
  • Email: mandrykin@ispras.ru
  • Registered on: 09/22/2010
  • Last connection: 07/27/2021

Issues

open closed Total
Assigned issues 29 28 57
Reported issues 5 3 8

Projects

Project Roles Registered on
AstraVer Toolset Manager, Developer, Project Creator 04/26/2018
Deductive Verification Tools for Linux Kernel Manager, Developer, Project Creator 09/02/2014
Дополнительные материалы к монографии Manager, Developer, Project Creator 04/28/2018
Klever Reporter 09/04/2015
Linux Driver Verification Developer, Project Creator 09/22/2010
BLAST Manager 09/16/2011
Crude_slicer Manager, Developer, Project Creator 10/31/2017
LDV Tools Developer, Project Creator 03/17/2018
CPAchecker Developer, Project Creator 07/28/2018
CVC3 with small optimizations for BLAST Developer, Project Creator 07/25/2018
Linux Kernel Safety RuleDB Developer 04/25/2012
Imperative HOL examples Manager, Developer, Project Creator 10/16/2019
TSMT: Tools for bounded E-Matching Manager, Developer, Project Creator 08/19/2019
VerKer - Verification of Linux Kernel Library Functions Developer, Reporter 05/21/2017

Activity

07/30/2021

04:03 PM Deductive Verification Tools for Linux Kernel Revision 61c689f5 (framac): Follow-up commit for preliminary _Atomic support
Somehow, `make` suppressed all regular OCaml warnings and some match cases were
missed
Mikhail Mandrykin

07/29/2021

05:29 PM Deductive Verification Tools for Linux Kernel Revision b58627e8 (framac): Added tentative support for the C11 _Atomic
type qualifiers and specifiers (syntax only)
Both are represented as attributes, the qualifier is called "Atomic" and...
Mikhail Mandrykin

07/23/2021

09:29 PM TSMT: Tools for bounded E-Matching Revision 6b57c6ad (tsmt): Cleanup cont'd
Mikhail Mandrykin

07/22/2021

10:59 PM TSMT: Tools for bounded E-Matching Revision 5d4b3748 (tsmt): Started cleanup of the completeness proof for the theory of
bounded pointer arithmetic (BPA) Mikhail Mandrykin

07/20/2021

01:26 AM TSMT: Tools for bounded E-Matching Revision 7cf95d60 (tsmt): Finished proof of A_offset_shift
Mikhail Mandrykin

07/19/2021

03:54 PM TSMT: Tools for bounded E-Matching Revision 9b88a219 (tsmt): A fix in the locale axioms + Finished A_array_shift
Mikhail Mandrykin
03:03 PM TSMT: Tools for bounded E-Matching Revision 24c69870 (tsmt): Fixes in axioms, model and proof of A_p_diff
Mikhail Mandrykin

07/16/2021

06:20 PM Deductive Verification Tools for Linux Kernel Revision 1dc8f093 (astraver): Added missing dependency on `ref.(:=)` hard-coded for assignments
in Why3 module printing Mikhail Mandrykin
05:04 PM TSMT: Tools for bounded E-Matching Revision 76a5b53b (tsmt): Simplified model of pointer comparison
Mikhail Mandrykin
04:15 PM TSMT: Tools for bounded E-Matching Revision aef8153d (tsmt): Proved axiom about poiner comparison in the reconstructed model;
propagated fixes to other proofs Mikhail Mandrykin

Also available in: Atom