Anonymous user
User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/Formal methods (view source)
Revision as of 06:06, 14 October 2010
, 13 years ago→Reference material
Line 46:
* [[wp:Constraint_programming]]
*: How does this relate?
* BLAST, SLAM, and PREfast▼
*: ddunbar mentioned these as similar to this project▼
** [http://research.microsoft.com/en-us/projects/slam/ SLAM], by MS, has [http://research.microsoft.com/pubs/121290/axioms.submitted.pdf a paper] which has the same idea for representing memory in SMT▼
* Slide show demonstrating same project, using LLVM: http://events.iaik.tugraz.at/avm2008/EvdinTorok_StaticMemoryAccessChecking.pdf▼
===Implementation methods===
* [[wp:Hoare_logic]]
* [[wp:Agda_(theorem_prover)]]▼
* [[wp:Automated_theorem_proving]]▼
===SMT Research===
* http://research.microsoft.com/en-us/um/people/leonardo/lab.pdf
* SMT solver
** http://www.cs.virginia.edu/~weimer/2007-615/lectures.html
**: ddunbar on #llvm suggested reading for SMT
▲* [[wp:Agda_(theorem_prover)]]
▲* [[wp:Automated_theorem_proving]]
* www.key-project.org/keysymposium10/slides/Falke_LLBMC.pdf
*: Another paper with details about LLVM => SMT
▲* BLAST, SLAM, and PREfast
▲*: ddunbar mentioned these as similar to this project
▲** [http://research.microsoft.com/en-us/projects/slam/ SLAM], by MS, has [http://research.microsoft.com/pubs/121290/axioms.submitted.pdf a paper] which has the same idea for representing memory in SMT
▲* Slide show demonstrating same project, using LLVM: http://events.iaik.tugraz.at/avm2008/EvdinTorok_StaticMemoryAccessChecking.pdf
==Related work==
| |||