zsu

5 ms·

1.
Semantic reification: how to generate UB-free code with arbitrary control flow?(github.com)
17 points by zsu 4mo ago|1 comments
2.
by zsu 4mo ago
- PLDI'26 paper: https://connglli.github.io/pdfs/reify_pldi26.pdf - Spin-off project symlang: https://github.com/connglli/symlang
3.
Property-based testing for mobile GUI apps(github.com)
2 points by zsu 2y ago|0 comments
4.
Understanding and exploiting optimal function inlining(dl.acm.org)
1 points by zsu 5y ago|0 comments
5.
Finding missed optimizations through the lens of dead code elimination(github.com)
1 points by zsu 5y ago|1 comments
6.
by zsu 5y ago
Link to paper: https://dl.acm.org/doi/pdf/10.1145/3503222.3507764
7.
How to make an award-winning software artifact(sigops.org)
2 points by zsu 6y ago|0 comments
8.
by zsu 6y ago
Thanks!
9.
by zsu 6y ago
Agreed; such an analysis/study would be nice to have. It is worth to point that the small tests were the results of test input reduction --- the original tests were often quite large. Many of the bugs were due to incorrect handling of
10.
by zsu 6y ago
Figure 8 in the OOPSLA paper ( https://arxiv.org/pdf/2004.08799.pdf ) provides a breakdown of the bugs found in different logics for Z3 and CVC4.
11.
by zsu 6y ago
To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.
12.
by zsu 6y ago
Project website: https://testsmt.github.io/
13.
Yin-Yang – A tool for stress-testing SMT solvers(testsmt.github.io)
54 points by zsu 6y ago|14 comments
14.
by zsu 9y ago
For information, links to all the bugs that we reported so far (in GCC/LLVM/CompCert/ICC and Scala) can be found at http://web.cs.ucdavis.edu/~su/emi-project/ : 728 in Clang/LLVM (~250 were mis
15.
by zsu 12y ago
Link to our talk slides: http://www.cs.ucdavis.edu/~su/publications/emi-talk.pdf