General

Profile

Pavel Putro

Issues

Projects

Activity

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 бит, что обраба...

11/06/2018

01:38 PM MicroTESK Bug #9364 (Open): Некорректная генерация smt-lib формул
Обнаружено 2 бага связанных с генерацией smt-lib формул. В приложенных файлах содержится бинарный код, некорректный и...

10/14/2018

08:37 PM Deductive Verification Tool for Machine Code Revision 178d3ea2: Switch to ISPRAS versions of Why3 and Frama-C
04:44 PM Deductive Verification Tool for Machine Code Revision 5da9c7fd: Return old type system

09/07/2018

12:53 AM Deductive Verification Tool for Machine Code Revision d2797087: Lemmas and axioms support and tests added

09/06/2018

12:42 AM Deductive Verification Tool for Machine Code Revision c5336c0a: Restucted Acsl-Frama-C type system and some other improvements

08/10/2018

11:54 PM Deductive Verification Tool for Machine Code Revision 51c2b5a4: Abstract extract and concat added
09:59 PM Deductive Verification Tool for Machine Code Revision 25bb0b8c: Average test and bvand added

Also available in: Atom