User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
Content added Content deleted
No edit summary |
|||
Line 1: | Line 1: | ||
==Formal methods project== |
|||
Write an LLVM pass that will prove certain properties of functions. |
|||
==Features== |
==Features== |
||
Follow the examples of [[wp:Java_Modeling_Language]] and [[wp:SPARK_programming_language]]. |
Follow the examples of [[wp:Java_Modeling_Language]] and [[wp:SPARK_programming_language]]. |
||
Line 11: | Line 8: | ||
* Determine if the function requires Turing-completeness |
* Determine if the function requires Turing-completeness |
||
** [[wp:Termination_analysis]] |
** [[wp:Termination_analysis]] |
||
** Reduction of turing-ness if possible (if provable) to decidable |
|||
** Do some '''good stuff''', as the function is not Turing-complete |
** Do some '''good stuff''', as the function is not Turing-complete |
||
** Equivalence? |
** Equivalence? |
||
Line 17: | Line 15: | ||
*** http://www.cs.nott.ac.uk/~nad/publications/ => http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.pdf |
*** http://www.cs.nott.ac.uk/~nad/publications/ => http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.pdf |
||
*** [http://research.microsoft.com/en-us/um/cambridge/projects/terminator/ Microsoft Terminator] (sounds insidious). |
*** [http://research.microsoft.com/en-us/um/cambridge/projects/terminator/ Microsoft Terminator] (sounds insidious). |
||
* Compute function complexity |
* Compute function complexity (best, average, worst) of an algorithm (function) |
||
** Allow the function to assert complexity |
** Allow the function to assert complexity |
||
* Allow arbitrary restrictions on functions, which would propagate through the call graph |
* Allow arbitrary restrictions on functions, which would propagate through the call graph |
||
Line 41: | Line 39: | ||
*** [http://seanhn.wordpress.com/2010/07/17/applying-taint-analysis-and-theorem-proving-to-exploit-development/ Applying Taint Analysis and Theorem Proving to Exploit Development] |
*** [http://seanhn.wordpress.com/2010/07/17/applying-taint-analysis-and-theorem-proving-to-exploit-development/ Applying Taint Analysis and Theorem Proving to Exploit Development] |
||
***: Another blog post, by thesis author |
***: Another blog post, by thesis author |
||
==Test examples== |
|||
* Prove that a regular expression evaluator halts (IE. calculate the computational complexity). |
|||
==Reference material== |
|||
* [[wp:Correctness_(computer_science)]] |
|||
* [[wp:Declarative_programming]] |
|||
* http://www.jaist.ac.jp/~hirokawa/tool/ |
|||
*: A pretty comprehensive page about whats out there in the proving world |
|||
* [[wp:Constraint_programming]] |
|||
*: How does this relate? |
|||
== Further reading == |
|||
Read this stuff: |
|||
* http://www.csci.csusb.edu/dick/papers/rjb93a.xbnf.html |
|||
===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 |
|||
* 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== |
|||
* [http://llvm.org/pubs/2007-SOSP-SVA.pdf LLVM Secure Virtual Architecture] |
|||
* [http://www.cs.cornell.edu/talc/ Typed assembly language] |
|||
* Native Client? |
|||
* [http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf Total Functional Programming] |
|||
*: Paper that argues for [[wp:Total Functional Programming|Total Functional Programming]] |
|||
* http://www.cs.umd.edu/~saurabhs/pacs/ |
|||
*: '''Program verification specs using SMT solvers''' |
|||
==Non-Turing-complete languages== |
|||
* [[wp:BlooP_and_FlooP]] |
|||
* [[wp:Charity_(programming_language)]] |
|||
* [[wp:Epigram_(programming_language)]] |
|||
* [http://www-fp.cs.st-andrews.ac.uk/hume/index.shtml The Hume Programming Language] (Higher-order Unified Meta-Environment) |
|||
*: Five layers of progressively more complete, and progressively less safe, languages, see the [http://www-fp.cs.st-andrews.ac.uk/hume/report/hume-report.pdf Hume Report] |
|||
==Other interesting languages== |
|||
* [[wp:UNITY_(programming_language)]] |
|||
*: No flow control; seems very declarative |
|||
* [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] |
|||
*: Requires termination proofs, effectively making it decidable (I think) |
|||
** Also a theorem proover (can be a language and its proof according to the [[wp:Curry–Howard_correspondence#Related_proofs-as-programs_correspondences| Curry–Howard correspondence]] |