NoteZ
NoteZ copied to clipboard
Published
20 hours ago •
jmpews
jmpews
Z3 Theorem Prover
Prologue
Somniliquy 2>
Refer
// get start
https://rise4fun.com/z3/tutorial/guide
// syscan360 paper with practical use
https://www.syscan360.org/slides/2014_EN_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf
// cn version
[2014_ZH_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf](https://github.com/jmpews/NoteZ/files/1783422/2014_ZH_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf)
Barf Binary Analysis
// get start
https://rise4fun.com/z3/tutorial/guide
// syscan360 paper with practical use
https://www.syscan360.org/slides/2014_EN_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf
// cn version
[2014_ZH_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf](https://github.com/jmpews/NoteZ/files/1783422/2014_ZH_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf)
x86 -> REIL -> SMT
https://www.syscan360.org/slides/2014_EN_ProgramAnalysisAndConstraintSolvers_EdgarBarbosa.pdf
