Update render script and Makefile
This commit is contained in:
@@ -1,4 +1,4 @@
|
||||
[38;5;12m [39m[38;2;255;187;0m[1m[4mProvably Awesome. [0m[38;5;14m[1m[4m![0m[38;5;14m[1m[4m (img/badge.svg)[0m[38;2;255;187;0m[1m[4m (http://awesome.re)[0m
|
||||
[38;5;12m [39m[38;2;255;187;0m[1m[4mProvably Awesome. [0m[38;5;14m[1m[4m![0m[38;5;14m[1m[4m (img/badge.svg)[0m[38;2;255;187;0m[1m[4m (http://awesome.re)[0m
|
||||
|
||||
[38;5;12mThis is a curated list of links and resources related to mathematical proofs[39m
|
||||
[38;5;12mabout the properties of computer programs.[39m
|
||||
@@ -106,7 +106,8 @@
|
||||
[38;5;12m environment: they can be matched, moved from one place to another, modified, or [39m
|
||||
[38;5;12m deleted. This makes K suitable for defining control-intensive features such as [39m
|
||||
[38;5;12m abrupt termination, exceptions or call/cc.[39m
|
||||
[38;5;12m [39m[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mK Tutorial[0m[38;5;12m (http://www.kframework.org/index.php/K_Tutorial) by [39m[38;5;14m[1mGrigore Rosu[0m[38;5;12m (https://github.com/grosu), [39m[38;5;14m[1mvideo playlist[0m[38;5;12m (https://www.youtube.com/watch?v=eSaIKHQOo4c&list=PLx_U8qR-tMtLQEDPvVk1y9gTIdUIWGaQd)[39m
|
||||
[38;5;12m [39m[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mK[0m[38;5;14m[1m [0m[38;5;14m[1mTutorial[0m[38;5;12m [39m[38;5;12m(http://www.kframework.org/index.php/K_Tutorial)[39m[38;5;12m [39m[38;5;12mby[39m[38;5;12m [39m[38;5;14m[1mGrigore[0m[38;5;14m[1m [0m[38;5;14m[1mRosu[0m[38;5;12m [39m[38;5;12m(https://github.com/grosu),[39m[38;5;12m [39m[38;5;14m[1mvideo[0m[38;5;14m[1m [0m[38;5;14m[1mplaylist[0m[38;5;12m [39m
|
||||
[38;5;12m(https://www.youtube.com/watch?v=eSaIKHQOo4c&list=PLx_U8qR-tMtLQEDPvVk1y9gTIdUIWGaQd)[39m
|
||||
[38;5;12m [39m[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12m(https://runtimeverification.com/) : Company formed from K Framework people. [39m
|
||||
[48;5;235m[38;5;249m Runtime Verification Inc. is currently developing three core products: [49m[39m[48;5;235m[38;5;249m [49m[39m
|
||||
[48;5;235m[38;5;249m * RV-Predict is a predictive runtime analysis tool focused on automatically [49m[39m[48;5;235m[38;5;249m [49m[39m
|
||||
@@ -116,11 +117,11 @@
|
||||
[48;5;235m[38;5;249m * RV-Match is a tool allowing for exhaustive runtime verification to be performed [49m[39m
|
||||
[48;5;235m[38;5;249m symbolically on all possible program paths, proving certain properties correct [49m[39m[48;5;235m[38;5;249m [49m[39m
|
||||
[48;5;235m[38;5;249m for all possible executions of a given program.[49m[39m[48;5;235m[38;5;249m [49m[39m
|
||||
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mViper[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/viper.html)[39m[38;5;12m [39m[38;5;12m:[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12m(Verification[39m[38;5;12m [39m[38;5;12mInfrastructure[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPermission-based[39m[38;5;12m [39m[38;5;12mReasoning)[39m[38;5;12m [39m[38;5;12mis[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mlanguage[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12msuite[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mtools[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12mat[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich,[39m[38;5;12m [39m[38;5;12mproviding[39m[38;5;12m [39m[38;5;12man[39m[38;5;12m [39m[38;5;12marchitecture[39m[38;5;12m [39m
|
||||
[38;5;12mon[39m[38;5;12m [39m[38;5;12mwhich[39m[38;5;12m [39m[38;5;12mnew[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mtools[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mprototypes[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12msimply[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mquickly.[39m[38;5;12m [39m[38;5;12mIt[39m[38;5;12m [39m[38;5;12mcomprises[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mnovel[39m[38;5;12m [39m[38;5;12mintermediate[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12malso[39m[38;5;12m [39m[38;5;12mnamed[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mautomatic[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12mas[39m[38;5;12m [39m[38;5;12mwell[39m[38;5;12m [39m[38;5;12mas[39m
|
||||
[38;5;12mexample[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mtools.[39m[38;5;12m [39m[38;5;12mThe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mtoolset[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12mused[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12mimplement[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mtechniques[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mprogramming[39m[38;5;12m [39m[38;5;12mlanguages[39m[38;5;12m [39m[38;5;12mvia[39m[38;5;12m [39m[38;5;12mtranslations[39m[38;5;12m [39m[38;5;12minto[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mlanguage.[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich[39m[38;5;12m [39m[38;5;12mhas[39m[38;5;12m [39m[38;5;12mbuilt[39m[38;5;12m [39m[38;5;12mseveral[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mon[39m
|
||||
[38;5;12mtop[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mincluding[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;14m[1mGobra[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/gobra.html)[39m[38;5;12m [39m[38;5;12mverifier[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mGo,[39m[38;5;12m [39m[38;5;14m[1mNagini[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/nagini.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPython[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;14m[1mPrusti[0m[38;5;12m [39m
|
||||
[38;5;12m(https://www.pm.inf.ethz.ch/research/prusti.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mRust.[39m
|
||||
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mViper[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/viper.html)[39m[38;5;12m [39m[38;5;12m:[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12m(Verification[39m[38;5;12m [39m[38;5;12mInfrastructure[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPermission-based[39m[38;5;12m [39m[38;5;12mReasoning)[39m[38;5;12m [39m[38;5;12mis[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mlanguage[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12msuite[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mtools[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12mat[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich,[39m[38;5;12m [39m
|
||||
[38;5;12mproviding[39m[38;5;12m [39m[38;5;12man[39m[38;5;12m [39m[38;5;12marchitecture[39m[38;5;12m [39m[38;5;12mon[39m[38;5;12m [39m[38;5;12mwhich[39m[38;5;12m [39m[38;5;12mnew[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mtools[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mprototypes[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12msimply[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mquickly.[39m[38;5;12m [39m[38;5;12mIt[39m[38;5;12m [39m[38;5;12mcomprises[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mnovel[39m[38;5;12m [39m[38;5;12mintermediate[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12malso[39m[38;5;12m [39m[38;5;12mnamed[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m
|
||||
[38;5;12mautomatic[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12mas[39m[38;5;12m [39m[38;5;12mwell[39m[38;5;12m [39m[38;5;12mas[39m[38;5;12m [39m[38;5;12mexample[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mtools.[39m[38;5;12m [39m[38;5;12mThe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mtoolset[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12mused[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12mimplement[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mtechniques[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mprogramming[39m[38;5;12m [39m[38;5;12mlanguages[39m[38;5;12m [39m[38;5;12mvia[39m[38;5;12m [39m
|
||||
[38;5;12mtranslations[39m[38;5;12m [39m[38;5;12minto[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mlanguage.[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich[39m[38;5;12m [39m[38;5;12mhas[39m[38;5;12m [39m[38;5;12mbuilt[39m[38;5;12m [39m[38;5;12mseveral[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mon[39m[38;5;12m [39m[38;5;12mtop[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mincluding[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;14m[1mGobra[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/gobra.html)[39m[38;5;12m [39m[38;5;12mverifier[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mGo,[39m[38;5;12m [39m[38;5;14m[1mNagini[0m[38;5;12m [39m
|
||||
[38;5;12m(https://www.pm.inf.ethz.ch/research/nagini.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPython[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;14m[1mPrusti[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/prusti.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mRust.[39m
|
||||
|
||||
[38;2;255;187;0m[4mProjects[0m
|
||||
|
||||
@@ -281,7 +282,8 @@
|
||||
[38;5;12m Uses SEL4, other RTOS[39m
|
||||
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mPentagon Wants Unhackable Helicopters[0m[38;5;12m (https://www.engadget.com/2015/03/16/pentagon-wants-unhackable-helicopters/)[39m
|
||||
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHacker-Proof Code Confirmed[0m[38;5;12m (https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/) : [39m
|
||||
[38;5;12mComputer scientists can prove certain programs to be error-free with the same certainty that mathematicians prove theorems. The advances are being used to secure everything from unmanned drones to the internet.[39m
|
||||
[38;5;12mComputer[39m[38;5;12m [39m[38;5;12mscientists[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mprove[39m[38;5;12m [39m[38;5;12mcertain[39m[38;5;12m [39m[38;5;12mprograms[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12merror-free[39m[38;5;12m [39m[38;5;12mwith[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12msame[39m[38;5;12m [39m[38;5;12mcertainty[39m[38;5;12m [39m[38;5;12mthat[39m[38;5;12m [39m[38;5;12mmathematicians[39m[38;5;12m [39m[38;5;12mprove[39m[38;5;12m [39m[38;5;12mtheorems.[39m[38;5;12m [39m[38;5;12mThe[39m[38;5;12m [39m[38;5;12madvances[39m[38;5;12m [39m[38;5;12mare[39m[38;5;12m [39m[38;5;12mbeing[39m[38;5;12m [39m[38;5;12mused[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12msecure[39m[38;5;12m [39m[38;5;12meverything[39m[38;5;12m [39m[38;5;12mfrom[39m[38;5;12m [39m[38;5;12munmanned[39m[38;5;12m [39m
|
||||
[38;5;12mdrones[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12minternet.[39m
|
||||
|
||||
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCertiKOS enables creation of secure system kernels[0m[38;5;12m (http://www.zdnet.com/article/certikos-a-hacker-proof-os/) [39m[38;5;12mcertikos project[39m[38;5;14m[1m (http://flint.cs.yale.edu/certikos/)[0m[38;5;12m [39m
|
||||
[38;5;12mComputer system security stinks, because our [39m
|
||||
|
||||
Reference in New Issue
Block a user