Sourav Das

icon company Indian Institute of Technology Kharagpur icon location Kharagpur, West Bengal icon location Ph.D. Scholar at IIT Kharagpur, West Bengal

Results 2 issues of Sourav Das

Dumping Z3 code from IR (IR --> Z3 converter)

6 comment

I want to dump the Z3 equivalent code from the IR that is being generated. Is there any tutorial regarding that? I can see "**xls/xls/solvers/z3_ir_translator.cc**", "**xls/xls/solvers/z3_lec.cc**" and other relevant files,...

question
formal

Improving Formal Verification for IR

4 comment

### What's hard to do? (limit 100 words) Making the generated Z3 code independent and provable standalone. There are three things I would like to address: 1. The assertion node...

enhancement