5 ms·

Is there any introductory course for these kind of stuff?

by 0xFFC 6y ago

sempron64 6y ago
I’m just starting to investigate using formal analysis in practice and I think a much more practical topic is the symbolic execution frameworks which can analyze programs and feed them to theorem solvers like Z3. The most useful and accessible symbolic execution package I’ve found so far is KLEE https://klee.github.io/ https://klee.github.io/ If anyone else has recommendations for tools or beginner material I’m all ears!
- nextos 6y ago
  There's some nice literature. I got into the field 15 years ago and there were practically no good textbooks. Things are way better now: https://avigad.github.io/formal_methods_in_education/ https://avigad.github.io/formal_methods_in_education/ Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Actually, I'd say they are easy going and fun but still retain all the mathematical rigor. They use program graphs, which are a bit less general but a lot easier to digest. They cover all major techniques, including theorem proving, static analysis, model checking, abstract interpretation, type and effect systems, etc: - Formal Methods: An Appetizer https://www.springer.com/gp/book/9783030051556 https://www.springer.com/gp/book/9783030051556 - Program Analysis: An Appetizer https://arxiv.org/abs/2012.10086 https://arxiv.org/abs/2012.10086 There's also a companion website with some F# code. The second book, which seems still unfinished discusses how to implement program analyses using datalog. This speeds up development quite a lot. Otherwise, developing your own static analyzer is a lot of work. My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. I think restricted semantics is the key to make formal methods practical. Quoting Alan Perlis, "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy."
  - the-smug-one 6y ago
    >My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. There's work in this area using monads. Specifically, Darais (from Galois) et al show in "Abstracting Definitional Interpreters" how given a definitional interpreter you can easily create all sorts of abstractions using a stack of monad transformers. The best part of it all is that your particular chosen stack remains valid when moved between interpreters of different languages. Your dream of varied static analysis can be achieved using monad transformers, definitional interpreters written in the required style, and Racket's DSL-creation system.
    - nextos 6y ago
      Thanks. I'm quite familiar with all the work from David Van Horn, including the paper you cited. I also think it's the way forward.
ripecoconut 6y ago
https://sat-smt.codes/main.html https://sat-smt.codes/main.html is a good introduction to applying SMT to many kinds of problems. https://rise4fun.com/ https://rise4fun.com/ for all sorts of examples of what these sorts of algorithms can solve. https://www.coursera.org/learn/discrete-optimization https://www.coursera.org/learn/discrete-optimization is a good introduction to constraint optimization, local search, linear programming, and mixed integer programming.
cjbprime 6y ago
Another option: the "reversing" challenges in infosec Capture The Flag competitions regularly require you to work out which constraints a program has implemented and then plug into Z3 or Angr to find a solution, that might be a fun way to learn.
philzook 6y ago
I'm giving a tutorial in a couple of days. Vids will be up later. https://github.com/philzook58/z3_tutorial https://github.com/philzook58/z3_tutorial
- philzook 6y ago
  These are other good resources: - rise4fun https://rise4fun.com/z3/tutorialcontent/guide https://rise4fun.com/z3/tutorialcontent/guide - https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ericpony.github.io/z3py-tutorial/guide-examples.htm - Programming Z3 -https://theory.stanford.edu/~nikolaj/programmingz3.html https://theory.stanford.edu/~nikolaj/programmingz3.html - Nikolaj Bjorner's tutorial https://youtu.be/nGwyNmsxX6I https://youtu.be/nGwyNmsxX6I - Hakank's examples http://www.hakank.org/z3/ http://www.hakank.org/z3/ - Yurichev's book "SMT by Example" https://yurichev.com/writings/SAT_SMT_by_example.pdf https://yurichev.com/writings/SAT_SMT_by_example.pdf - http://hackage.haskell.org/package/sbv http://hackage.haskell.org/package/sbv - https://www.youtube.com/watch?v=ruNFcH-KibY https://www.youtube.com/watch?v=ruNFcH-KibY Tikhon Jelvis - Analyzing Programs with Z3 - https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSIGPLAN https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSI... - Nadia Polykarpova on Z3 - SAT SMT school https://sat-smt.in/ https://sat-smt.in/ - Emina Torlak's course https://courses.cs.washington.edu/courses/cse507/19au/calendar.html https://courses.cs.washington.edu/courses/cse507/19au/calend... - Lindsey Kuper - SMT Solving and Solver-Aided Systems http://composition.al/CSE290Q-2019-09/ http://composition.al/CSE290Q-2019-09/ - http://www.sc-square.org/CSA/school/lectures.html http://www.sc-square.org/CSA/school/lectures.html

Is there any introductory course for these kind of stuff?

by 0xFFC 6y ago

Is there any introductory course for these kind of stuff?

I’m just starting to investigate using formal analysis in practice and I think a much more practical topic is the symbolic execution frameworks which can analyze programs and feed them to theorem solvers like Z3. The most useful and accessible symbolic execution package I’ve found so far is KLEE https://klee.github.io/ https://klee.github.io/ If anyone else has recommendations for tools or beginner material I’m all ears!

nextos 6y ago
There's some nice literature. I got into the field 15 years ago and there were practically no good textbooks. Things are way better now: https://avigad.github.io/formal_methods_in_education/ https://avigad.github.io/formal_methods_in_education/ Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Actually, I'd say they are easy going and fun but still retain all the mathematical rigor. They use program graphs, which are a bit less general but a lot easier to digest. They cover all major techniques, including theorem proving, static analysis, model checking, abstract interpretation, type and effect systems, etc: - Formal Methods: An Appetizer https://www.springer.com/gp/book/9783030051556 https://www.springer.com/gp/book/9783030051556 - Program Analysis: An Appetizer https://arxiv.org/abs/2012.10086 https://arxiv.org/abs/2012.10086 There's also a companion website with some F# code. The second book, which seems still unfinished discusses how to implement program analyses using datalog. This speeds up development quite a lot. Otherwise, developing your own static analyzer is a lot of work. My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. I think restricted semantics is the key to make formal methods practical. Quoting Alan Perlis, "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy."
- the-smug-one 6y ago
  >My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. There's work in this area using monads. Specifically, Darais (from Galois) et al show in "Abstracting Definitional Interpreters" how given a definitional interpreter you can easily create all sorts of abstractions using a stack of monad transformers. The best part of it all is that your particular chosen stack remains valid when moved between interpreters of different languages. Your dream of varied static analysis can be achieved using monad transformers, definitional interpreters written in the required style, and Racket's DSL-creation system.
  - nextos 6y ago
    Thanks. I'm quite familiar with all the work from David Van Horn, including the paper you cited. I also think it's the way forward.

ripecoconut 6y ago

https://sat-smt.codes/main.html https://sat-smt.codes/main.html is a good introduction to applying SMT to many kinds of problems. https://rise4fun.com/ https://rise4fun.com/ for all sorts of examples of what these sorts of algorithms can solve. https://www.coursera.org/learn/discrete-optimization https://www.coursera.org/learn/discrete-optimization is a good introduction to constraint optimization, local search, linear programming, and mixed integer programming.

cjbprime 6y ago

Another option: the "reversing" challenges in infosec Capture The Flag competitions regularly require you to work out which constraints a program has implemented and then plug into Z3 or Angr to find a solution, that might be a fun way to learn.

philzook 6y ago

I'm giving a tutorial in a couple of days. Vids will be up later. https://github.com/philzook58/z3_tutorial https://github.com/philzook58/z3_tutorial

philzook 6y ago
These are other good resources: - rise4fun https://rise4fun.com/z3/tutorialcontent/guide https://rise4fun.com/z3/tutorialcontent/guide - https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ericpony.github.io/z3py-tutorial/guide-examples.htm - Programming Z3 -https://theory.stanford.edu/~nikolaj/programmingz3.html https://theory.stanford.edu/~nikolaj/programmingz3.html - Nikolaj Bjorner's tutorial https://youtu.be/nGwyNmsxX6I https://youtu.be/nGwyNmsxX6I - Hakank's examples http://www.hakank.org/z3/ http://www.hakank.org/z3/ - Yurichev's book "SMT by Example" https://yurichev.com/writings/SAT_SMT_by_example.pdf https://yurichev.com/writings/SAT_SMT_by_example.pdf - http://hackage.haskell.org/package/sbv http://hackage.haskell.org/package/sbv - https://www.youtube.com/watch?v=ruNFcH-KibY https://www.youtube.com/watch?v=ruNFcH-KibY Tikhon Jelvis - Analyzing Programs with Z3 - https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSIGPLAN https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSI... - Nadia Polykarpova on Z3 - SAT SMT school https://sat-smt.in/ https://sat-smt.in/ - Emina Torlak's course https://courses.cs.washington.edu/courses/cse507/19au/calendar.html https://courses.cs.washington.edu/courses/cse507/19au/calend... - Lindsey Kuper - SMT Solving and Solver-Aided Systems http://composition.al/CSE290Q-2019-09/ http://composition.al/CSE290Q-2019-09/ - http://www.sc-square.org/CSA/school/lectures.html http://www.sc-square.org/CSA/school/lectures.html