General

Profile

Pavel Putro

Issues

Projects

Activity

02/16/2019

01:39 PM Deductive Verification Tool for Machine Code Revision 3cf148c7: Valid pointer align for risc-v added

01/28/2019

12:08 AM Deductive Verification Tool for Machine Code Revision 7c3f3709: delete Why3modules clone
11:59 PM Deductive Verification Tool for Machine Code Revision 22228212: Memory binding function added

01/26/2019

02:14 AM Deductive Verification Tool for Machine Code Revision 61b0dfff: Translation 64-bit args and locals to smt added

01/25/2019

03:49 PM Deductive Verification Tool for Machine Code Revision 5401e3dd: x64 Support at Why3 and other improvemets

01/10/2019

11:07 PM Deductive Verification Tool for Machine Code Revision 54e34dd3: Support loop invariants for -acsl-onl -produce-smt added

01/08/2019

05:20 PM Deductive Verification Tool for Machine Code Revision 67ed7ab3: Loop invariants extraction added

11/26/2018

09:18 PM Deductive Verification Tool for Machine Code Revision d54f52cb: RISC-V support added

11/23/2018

12:58 PM MicroTESK Bug #9395 (Open): Symexecute не учитывает неявные преобразования типов в nml моделях
Раз неявные преобразования нежелательны, то возможно их стоит запретить на уровне инструмента, чтобы такая ситуация н...

11/22/2018

02:39 PM MicroTESK Bug #9395 (Open): Symexecute не учитывает неявные преобразования типов в nml моделях
В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обраба...

Also available in: Atom