hax

KEVM என்பது EVM-இன் K-framework செயல்படுத்தக்கூடிய சொற்பொருளியல் (executable semantics) ஆகும்: உங்களுக்கு இணக்கத்தன்மை சரிபார்க்கப்பட்ட செயலாக்கம், குறியீட்டு ஆய்வு, எரிவாயு பகுப்பாய்வு அல்லது எத்திரியத்தின் விதிகளை நெருக்கமாகப் பின்பற்றும் சான்றுகள் தேவைப்படும்போது, பைட் குறியீட்டில் இதைப் பயன்படுத்துங்கள்.

Kontrol ஆனது Foundry பண்புச் சோதனைகளை KEVM-ஆதரவுடைய சான்றுகளாக மாற்றுகிறது, இதனால் வெறும் KEVM-ஐ மட்டும் பயன்படுத்துவதை விட குறைவான கையால் எழுதப்பட்ட விவரக்குறிப்பு வேலைகளுடன் முறைசார் உத்தரவாதங்களை நீங்கள் பெற முடியும்.

Act என்பது எத்திரியத்தின் அறிவிப்பு விவரக்குறிப்பு மொழி மற்றும் கருவித்தொகுப்பாகும். இது ஒரு EVM நிரலின் அனைத்து நடத்தைகளையும் விவரிக்கப் பயன்படுகிறது, இதன் மூலம் SMT தீர்ப்பிகள், தேற்ற நிரூபிகள் அல்லது பொருளாதாரப் பகுப்பாய்வுக் கருவிகள், நடைமுறைச் செயலாக்கங்களுக்கு எதிரான தானியங்கி சுத்திகரிப்பு சான்றுகள் உட்பட, பைட் குறியீடு-நிலை சரியான தன்மை மற்றும் ஊக்கத்தொகை இணக்கத்தன்மை குறித்து பகுப்பாய்வு செய்ய முடியும்.

தானியங்கு SMT அணுகுமுறைகள் போதுமானதாக இல்லாதபோது, மிக வலுவான சரியான தன்மைக்கான உறுதிப்பாடுகளை நீங்கள் இலக்காகக் கொள்ளும் வகையில், Verifereum எத்திரியம் திறன் ஒப்பந்தங்களை HOL4-ஆதரவுடைய தேற்றம் நிரூபித்தலுடன் இணைக்கிறது.