Lightweight Data-flow Analysis for Execution-driven Constraint Solving

Slides:



Advertisements
Similar presentations
國立交通大學應用數學系 數學建模與科學計算研究所 簡 介. 隨著科技的日新月異,人類為追求完美的生活,其 所面臨的科學與工程問題也日趨複雜,舉凡天氣的 預測、飛機的設計、生物醫學中的神經網路、奈米 材料的研發、衍生性金融產品的定價、甚至交通流 量的監測等問題,透過「數學建模」的量化過程, 再配合以「科學計算」的方式去模擬現象並嘗試尋.
Advertisements

組別:第一組 指導老師:陳怡昌 老師 組員: 4020L005 楊明軒 4020L012 康家誠 4020L034 許慈芳 4020L065 潘姵璇 4020L072 許乃文 4020L078 馮家興 4020L097 戴嘉辰 4031L004 吳怡樺 報告日期: 2015/06/05 教育訓練發展期末報告.
语态变化法 廖文君 许君 覃志斌. 这里说的语态是指主动语态和被动语 态。这两种语态在英汉两种语言中的 使用情况是很不相同的:英语大量使 用被动语态,而汉语很少使用,即使 使用,也不像英语那样有固定的构成 形式。譬如说,汉语的被动不是只用 一个 “ 被 ” 字表示。因此,为使译文更 加地道,在翻译中就必须采用变化语.
传媒学生应该如何度 过四年大学生活?. 进入大学一个多月了,用一个词形容大 学生活 自卑感 不适应 空虚感 被动感 孤独感 失望感 一、大学新生不适应大学生活的表现:
劉凝慧 青年新歌.
第9章 市场风险管理.
3 供需彈性與均衡分析.
第 6 章 使用資料分析工具 建立樞紐分析表 修訂樞紐分析表 建立、 修訂樞紐分析圖 為Web建立互動式的樞紐分析表清單.
学党章党规、学系列讲话,做合格党员 学习教育
34 府学胡同的文天祥祠,相传是南宋民族英雄文天祥当年遭囚禁和就义的地方,1376年明洪武九年建祠 。
宏 观 经 济 学 N.Gregory Mankiw 上海杉达学院.
商务礼仪 新员工培训.
高考文言文的整体阅读.
師資培育中心外埠教育參觀.
——奧科特公開及內部培訓 系列課程(三)之十一
資料探勘(Data Mining)及其應用之介紹
新竹教育大學 數理教育研究所 蘇宏仁 中華民國 100 年 7 月 27 日 於竹市環境教育輔導小組
第四章 日月地系统.
線上課程設計.
臺北市立松山家商 103學年度第1學期 學校日 教學說明 簡報
经 络 学.
商業智慧與資料倉儲 課程簡介 靜宜大學資管系 楊子青.
心理的力量 --兼谈教师心理压力的调适
项目申报及投资推进工作实务 更多模板、视频教程: 兰溪市发展和改革局 2013年9月 1.
大数据在医疗行业的应用.
Chaoping Li, Zhejiang University
前不久看到了这样一则报道:某个大学校园里,一个大学生出寝室要给室友留一张字条,告诉他钥匙放在哪里。可是“钥匙”两个字他不会写,就问了其他寝室的同学,问了好几个,谁也不会写,没办法,只好用“KEY”来代替了。 请大家就此事发表一下自己看法。
行为礼仪培训 二○○八年十一月.
XI. Hilbert Huang Transform (HHT)
Population proportion and sample proportion
利用共同供應契約 辦理大量訂購流程說明.
The Empirical Study on the Correlation between Equity Incentive and Enterprise Performance for Listed Companies 上市公司股权激励与企业绩效相关性的实证研究 汇报人:白欣蓉 学 号:
Working with Databases (II) 靜宜大學資管系 楊子青
Digital Terrain Modeling
HLA - Time Management 陳昱豪.
Responsibility Accounting
创建型设计模式.
塑膠材料的種類 塑膠在模具內的流動模式 流動性質的影響 溫度性質的影響
Understanding the Supply Chain
第 四 章 ADDIE系統化教學設計模式 課程名稱:數位學習 授課老師:李春雄 博士
Symbolic Execution During Test Data Generation and Augmentation Top Paper Review Zhiyi Zhang.
句子成分的省略(1).
Chapter 5 Recursion.
研究技巧與論文撰寫方法 中央大學資管系 陳彥良.
第八章 線性迴歸 8.1 線性迴歸概論 8.2 相關分析 8.3 簡單迴歸分析 8.4 迴歸模型係數的推導
Introduction to C Programming
前向人工神经网络敏感性研究 曾晓勤 河海大学计算机及信息工程学院 2003年10月.
An Automated Approach to Generating Efficient Constraint Solvers
ER Model.
虚 拟 仪 器 virtual instrument
國外案例報告:Nobelprize.org The Diabetic Dog Game 組員: 吳聲侑 陳富星 許瓈方
Lesson 19: A Story or a Poem?
從 ER 到 Logical Schema ──兼談Schema Integration
與傳媒共舞四大重點 李燦榮
数独简介 ◎数独是一种以数字为表现形式的逻辑推理谜题。 数独起源于18世纪末的瑞士,后在美国发展、并在日本得以发扬光大。
An Efficient MSB Prediction-based Method for High-capacity Reversible Data Hiding in Encrypted Images 基于有效MSB预测的加密图像大容量可逆数据隐藏方法。 本文目的: 做到既有较高的藏量(1bpp),
兒童及少年保護、 家庭暴力及性侵害事件、 高風險家庭 宣導與通報
外埔國小103學年度下學期期末校務會議 吳文芳 校長 104/06/24.
中国农业科学院博士后学术论坛 博士后基金申请的经验及体会 中国农业科学院生物技术研究所 秦 华 博士
Create and Use the Authorization Objects in ABAP
Mechanics Exercise Class Ⅱ
主講 / Alice Lee 李麗貞 2006 主題二 叫我第一名 主講 / Alice Lee 李麗貞
第七章 知識管理.
進階 WWW 程式設計 -- PHP Array 靜宜大學資訊管理學系 蔡奇偉副教授
常州市教育学会学业水平监测 九年级英语试卷分析 常州市第二十四中学 许喆 2012年2月.
有理数的乘方(二).
Chapter4工作分析與工作評價 第一節 工作分析 第二節 工作評價.
定语从句(4).
POWER-EFFICIENT RANGE-MATCH-BASED PACKET CLASSIFICATION ON FPGA
Presentation transcript:

Lightweight Data-flow Analysis for Execution-driven Constraint Solving Junaid Haroon Siddiqui Darko Marinov Sarfraz Khurshid

背景 Constraint-based testing Key challenge-valid inputs generation execution-driven solving Wasteful Repeated predicate execution, predicate result

贡献 Lightweight static data-flow analysis for constraint solving Multi-value comparisons Implementation Evaluation

Traditional Korat 1,建立一个要测试的初始结构,执行repok算法; 2,当repok算法执行完后,将field domain中最后一个输入域中的数值改成一个新数值,然后重新执行repok算法; 3,如果最后一个field domain中的数值没有更多的数值,则到前一个field domain中; 4,一直所有的field domain中的数值都执行完。

Koratmulti: multi-value comparisons A multi-value comparison compares a given value against all values in the field domain of a field not yet accessed in the repOk predicate. If a field has already been accessed, the given value can only be compared against its ssigned value and no multi-value comparison can take place.

Koratmulti: multi-value comparisons 条件: 至少有一个可能的结果能够决定哪个repOk predicate能够返回。

Koratmulti: multi-value comparisons

Koratmulti: multi-value comparisons

Technique 主要思路: 对candidate进行判断是否为marked,如果是marked,则不需要执行repOk, repOk的结果就可以知道。 主要方法: 结合Data-flow analysis和Multi-value comparisons,在Multi-value comparisons中使用数据流分析方法,然后用Multi-value comparisons将candidate分为marked和unmarked。

1,followUseChain the accessed value is directly used as one argument of a comparison. 2,br The comparison is used inside an if statement. 3,ret determines if a constant is returned.

Evaloution 1,the number of repOk executions 2,the time it takes to generate valid inputs.

Evaloution