General

Profile

Mikhail Mandrykin

Issues

Projects

Activity

04/08/2020

09:29 PM Convergent E-Matching Revision 4b4543b0 (tsmt): TSMT Bouned Completeness: More readable proof of theory equivalence
Mikhail Mandrykin
09:13 PM Convergent E-Matching Revision 98d938aa (tsmt): Shorter notation for (m (const c)), session configuration (in ROOT)
Mikhail Mandrykin
06:10 PM Convergent E-Matching Revision 17a44157 (tsmt): TSMT Bounded: Examples from the evaluation section of the paper on bounded integers
Mikhail Mandrykin
06:06 PM Convergent E-Matching Revision 7647a575 (tsmt): TSMT Bounded: Added missing support for special polymorphic constants 0 and 1 (they are not numerals!)
Mikhail Mandrykin

04/07/2020

01:18 AM Convergent E-Matching Revision 3ba9716d (tsmt): WIP: TSMT proof line unsat core-based optimization: definition exporting
Mikhail Mandrykin

04/02/2020

03:54 PM Deductive Verification Tools for Linux Kernel Bug #10198 (Resolved): Invalid serialization of post-decrement operation
It turned out to be caused by a missed case in the implementation of temporary variable folding. In this case tempora... Mikhail Mandrykin
03:36 PM Deductive Verification Tools for Linux Kernel Revision ff77b9ab (framac): Fixed special case of unspecified sequence in temporary variable folding
Mikhail Mandrykin
03:29 PM Deductive Verification Tools for Linux Kernel Revision 9d27efaa (framac): Fixed special case of unspecified sequence in temporary variable folding
Mikhail Mandrykin

04/01/2020

11:39 AM Deductive Verification Tools for Linux Kernel Revision 2dc8ac17 (framac): Loosened the criterion for dropping the result of a GNU body:
also drop if only the result type is interesting Mikhail Mandrykin

03/31/2020

01:49 AM Deductive Verification Tools for Linux Kernel Bug #10192 (Resolved): Frama-C (CIL) issues invalid error "lvalue of type void: tmp"
Mikhail Mandrykin

Also available in: Atom