User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
Content added Content deleted
Line 46: | Line 46: | ||
* [[wp:Constraint_programming]] |
* [[wp:Constraint_programming]] |
||
*: How does this relate? |
*: How does this relate? |
||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
===Implementation methods=== |
===Implementation methods=== |
||
* [[wp:Hoare_logic]] |
* [[wp:Hoare_logic]] |
||
⚫ | |||
⚫ | |||
===SMT Research=== |
|||
* http://research.microsoft.com/en-us/um/people/leonardo/lab.pdf |
|||
* SMT solver |
* SMT solver |
||
** http://www.cs.virginia.edu/~weimer/2007-615/lectures.html |
** http://www.cs.virginia.edu/~weimer/2007-615/lectures.html |
||
**: ddunbar on #llvm suggested reading for SMT |
**: ddunbar on #llvm suggested reading for SMT |
||
⚫ | |||
⚫ | |||
* www.key-project.org/keysymposium10/slides/Falke_LLBMC.pdf |
* www.key-project.org/keysymposium10/slides/Falke_LLBMC.pdf |
||
*: Another paper with details about LLVM => SMT |
*: Another paper with details about LLVM => SMT |
||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
==Related work== |
==Related work== |