Pinned Repositories
-MSVL-
使用MSVL程序描述多线程交替执行的模型,针对该模型,使用PPTL描述期望满足的周期重复的性质,进而使用基于多核的运行时验证方法对其进行验证
Aegis
A generic runtime analysis tool to detect and protect against attacks in Ethereum (AsiaCCS 2020).
Alternate-Execution-of-Multiple-Threads-in-a-C-Program-
使用C程序中的SuspendThread和ResumeThread函数实现多线程交替执行
ARVDN
CPA4AV
Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering
DEF_LEAK
Ten C programs used to test the performance of DEF_LEAK combining dynamic analysis and DSE
DEF_LEAK-
PPTLCheck
为了展示单机多核并行运行时验证工具PPTLCheck验证大规模程序的能力,我们将PPTLCheck用来验证10个代码规模为1300行至33000行的工业级程序,每个文件中包含了安全性、活性、弱公平性和周期重复性四种性质和MSVL源程序
SQLite3Check
SQLite3Check验证的调用SQLite3数据库API的C程序等价转换得到的MSVL程序,共30个
SVR-model-based-on-electronic-tongue-test
MATLAB code to estiablish the SVR model to predict the maturity level and human sensory evaluation based on electronic tongue test
BinYu-Xidian-University's Repositories
BinYu-Xidian-University/SVR-model-based-on-electronic-tongue-test
MATLAB code to estiablish the SVR model to predict the maturity level and human sensory evaluation based on electronic tongue test
BinYu-Xidian-University/eth-reentrancy-attack-patterns
Re-entrancy attack patterns from our paper "Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks"
BinYu-Xidian-University/safely-mutable-ERC-20-interface
An interface for an ERC-20 token smart contract that enforces the expected behaviour of each entry-point.
BinYu-Xidian-University/intAbs
Repository for ASE 2017 paper, "Modular Verification of Interrupt-driven Software".
BinYu-Xidian-University/EC-Diff
Repository for ASE 2018 paper, "Datalog-based Scalable Semantic Diffing of Concurrent Programs".
BinYu-Xidian-University/yogar-cbmc
BinYu-Xidian-University/BLNFG
哲学家就餐和银行家算法MSVL程序
BinYu-Xidian-University/SQLite3Check
SQLite3Check验证的调用SQLite3数据库API的C程序等价转换得到的MSVL程序,共30个
BinYu-Xidian-University/PPTLCheck
为了展示单机多核并行运行时验证工具PPTLCheck验证大规模程序的能力,我们将PPTLCheck用来验证10个代码规模为1300行至33000行的工业级程序,每个文件中包含了安全性、活性、弱公平性和周期重复性四种性质和MSVL源程序
BinYu-Xidian-University/AVPredictor
A prototype tool to find Atomicity-violation bugs in multi-threaded programs
BinYu-Xidian-University/DEF_LEAK
Ten C programs used to test the performance of DEF_LEAK combining dynamic analysis and DSE
BinYu-Xidian-University/Alternate-Execution-of-Multiple-Threads-in-a-C-Program-
使用C程序中的SuspendThread和ResumeThread函数实现多线程交替执行
BinYu-Xidian-University/DEF_LEAK-
BinYu-Xidian-University/-MSVL-
使用MSVL程序描述多线程交替执行的模型,针对该模型,使用PPTL描述期望满足的周期重复的性质,进而使用基于多核的运行时验证方法对其进行验证
BinYu-Xidian-University/ECFChecker
A dynamic checker for the ECF property incorporated into geth
BinYu-Xidian-University/APISIM
BinYu-Xidian-University/Whyper
Automatically exported from code.google.com/p/drishti
BinYu-Xidian-University/ICON
Inferring Temporal Constraints from Natural Language API Descriptions