Automatically Generating Counterexamples to Naive Free Theorems

被引：0

作者：

Seidel, Daniel ^{[1
]}

Voigtlaender, Janis ^{[1
]}

机构：

[1] Univ Bonn, Inst Informat, D-53117 Bonn, Germany

来源：

FUNCTIONAL AND LOGIC PROGRAMMING, PROCEEDINGS | 2010年 / 6009卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Disproof can be as important as proof in studying programs and programming languages. In particular, side conditions in a statement about program behavior are sometimes best understood and explored by trying to exhibit a falsifying example in the absence of a condition in question. Automation is as desirable for such falsification as it is for verification. We develop formal and implemented tools or counterexample generation in the context of free theorems, i.e., statements derived from polymorphic types S la relational parametricity. The machinery we use is rooted in constraining the type system and in intuitionistic proof search.

引用

页码：175 / 190

页数：16

共 50 条

[21] SOME THEOREMS, COUNTEREXAMPLES, AND CONJECTURES IN MULTINOMIAL SELECTION THEORY
CHEN, RW
HWANG, FK
COMMUNICATIONS IN STATISTICS-THEORY AND METHODS, 1984, 13 (10) : 1289 - 1298
[22] THEOREMS FROM MEASURE AXIOMS, COUNTEREXAMPLES FROM DIAMOND(++)
FLEISSNER, W
WORK OF MARY ELLEN RUDIN, 1993, 705 : 67 - 77
[23] Towards automatically generating Double-Free vulnerability signatures using Petri nets
Iwahashi, Ryan
de Oliveira, Daniela A. S.
Wu, S. Felix
Crandall, Jedidiah R.
Heo, Young-Jun
Oh, Jin-Tae
Jang, Jong-Soo
INFORMATION SECURITY, PROCEEDINGS, 2008, 5222 : 114 - +
[24] Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
Blanchette, Jasmin Christian
Claessen, Koen
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 127 - +
[25] Generating counterexamples for quantitative safety specifications in probabilistic B
Ndukwu, Ukachukwu
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (01): : 26 - 45
[26] On Generating A Variety of Unsafe Counterexamples for Linear Dynamical Systems
Goyal, Manish
Duggirala, Parasara Sridhar
IFAC PAPERSONLINE, 2018, 51 (16): : 139 - 144
[27] Generating DFA Construction Problems Automatically
Shenoy, Varun
Aparanji, Ullas
Sripradha, K.
Kumar, Viraj
PROCEEDINGS OF 2016 INTERNATIONAL CONFERENCE ON LEARNING AND TEACHING IN COMPUTING AND ENGINEERING (LATICE 2016), 2016, : 32 - 37
[28] Automatically Generating Models for Botnet Detection
Wurzinger, Peter
Bilge, Leyla
Holz, Thorsten
Goebel, Jan
Kruegel, Christopher
Kirda, Engin
COMPUTER SECURITY - ESORICS 2009, PROCEEDINGS, 2009, 5789 : 232 - +
[29] EXE: Automatically Generating Inputs of Death
Cadar, Cristian
Ganesh, Vijay
Pawlowski, Peter M.
Dill, David L.
Engler, Dawson R.
ACM TRANSACTIONS ON INFORMATION AND SYSTEM SECURITY, 2008, 12 (02)
[30] SEEDB: Automatically Generating Query Visualizations
Vartak, Manasi
Madden, Samuel
Parameswaran, Aditya
Polyzotis, Neoklis
PROCEEDINGS OF THE VLDB ENDOWMENT, 2014, 7 (13): : 1581 - 1584

← 1 2 3 4 5 →