Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
cs-686:schedule [2018/10/23 16:19]
egm [Symbolic Execution for Source Code Verification]
cs-686:schedule [2018/10/23 16:23] (current)
egm [Symbolic Execution for Source Code Verification]
Line 81: Line 81:
 * [http://​yices.csl.sri.com/​papers/​cav2007.pdf A Tutorial on Satisfiability Modulo Theories] * [http://​yices.csl.sri.com/​papers/​cav2007.pdf A Tutorial on Satisfiability Modulo Theories]
 * [https://​smtlib.github.io/​jSMTLIB/​SMTLIBTutorial.pdf The SMT-LIBv2 Language and Tools: A Tutorial] * [https://​smtlib.github.io/​jSMTLIB/​SMTLIBTutorial.pdf The SMT-LIBv2 Language and Tools: A Tutorial]
 +* [http://​homepages.inf.ed.ac.uk/​pbj/​papers/​vct-dec09-draft.pdf Proving SPARK Verification Conditions with SMT Solvers]--very similar to this assignment
 The ultimate goal is to implement the [https://​people.eecs.berkeley.edu/​~ksen/​papers/​multise.pdf path merging] version of symbolic execution (the BDDs are a non-needed optimization) for your language, so read the background material enough to understand the approach. The ultimate goal is to implement the [https://​people.eecs.berkeley.edu/​~ksen/​papers/​multise.pdf path merging] version of symbolic execution (the BDDs are a non-needed optimization) for your language, so read the background material enough to understand the approach.
  
cs-686/schedule.txt ยท Last modified: 2018/10/23 16:23 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0