Mikhail Mandrykin
- Login: misha_bear
- Email: mandrykin@ispras.ru
- Registered on: 09/22/2010
- Last connection: 03/23/2023
Issues
open | closed | Total | |
---|---|---|---|
Assigned issues | 29 | 29 | 58 |
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
11/28/2022
- 05:18 PM Deductive Verification Tools for Linux Kernel Revision 15731e1c (framac): Compatibility with OCaml 4.14 (GADT typing fix)
- 04:44 PM Deductive Verification Tools for Linux Kernel Revision 25c19b15 (opam-repository): Bumped version restriction on OCaml compiler (for Why3)
- 04:25 PM Deductive Verification Tools for Linux Kernel Revision 2a2f3574 (opam-repository): Removed dependency on `conf-gtksourceview` as v.2 is not available and v.3 is not supported
05/17/2022
- 07:03 PM TSMT: Tools for bounded E-Matching Revision c5de8a95 (tsmt): Added output context setups
- to avoid failures caused by PLRDF's non-local \at notation
- 04:22 PM Deductive Verification Tools for Linux Kernel Revision 59ea9547 (framac): Exposed a function to set the reference file to itself
- When generating a .pp file way not be an option (e.g. for system
headers)
05/16/2022
- 10:07 PM TSMT: Tools for bounded E-Matching Revision c35bfe8e (tsmt): Fixed term substitution: beware of stray type variables
- 10:00 PM TSMT: Tools for bounded E-Matching Revision 351d50f8 (tsmt): Simply allowed patterns in triggers as essentially this is already OK
- 10:00 PM TSMT: Tools for bounded E-Matching Revision 1daff107 (tsmt): Fix: prefer conservative updates of min/max representants
- 10:00 PM TSMT: Tools for bounded E-Matching Revision 0203fa25 (tsmt): Fixed bug in prop var collection
- 10:00 PM TSMT: Tools for bounded E-Matching Revision ff55cf41 (tsmt): Finally, some working tests (Bounded)
Also available in: Atom