User Studies of Principled Model Finder Output
User Studies of Principled Model Finder Output
复制标题
原则模型查找器输出的用户研究
DOI：
10.1007/978-3-319-66197-1_11
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Dougherty, Daniel J.
中科院分区：
文献类型：
--
作者：
Danas, Natasha;Nelson, Tim;Harrison, Lane;Krishnamurthi, Shriram;Dougherty, Daniel J.
SAT求解器等模型查找器对于生成具体模型很有吸引力，无论是作为样本实例还是作为属性失败时的反例。然而，生成的模型是任意的。为了解决这个问题，一些研究工作提出了原则形式的输出模型发现者。这些方法包括最小和最大模型，unsat核心和基于证据的事实出处。虽然这些方法享有优雅的数学基础，但它们没有经过严格的用户评估来评估其效用。本文介绍了这三种形式的输出进行先进的学生的用户研究。我们发现，大多数的输出形式是无效的，在某些情况下，甚至主动误导用户。为了使这些研究能够频繁和大规模地运行，我们还展示了如何在众包网站Mechanical Turk上进行这些研究。
Model-finders such as SAT-solvers are attractive for producing concrete models, either as sample instances or as counterexamples when properties fail. However, the generated model is arbitrary. To address this, several research efforts have proposed principled forms of output from model-finders. These include minimal and maximal models, unsat cores, and proof-based provenance of facts.While these methods enjoy elegant mathematical foundations, they have not been subjected to rigorous evaluation on users to assess their utility. This paper presents user studies of these three forms of output performed on advanced students. We find that most of the output forms fail to be effective, and in some cases even actively mislead users. To make such studies feasible to run frequently and at scale, we also show how we can pose such studies on the crowdsourcing site Mechanical Turk.
登录
查看更多内容
DOI：
10.1007/978-3-642-24485-8_44
发表时间：
2011-10
期刊：
--
影响因子：
--
作者：
S. Maoz;Jan Oliver Ringert;Bernhard Rumpe
通讯作者：
S. Maoz;Jan Oliver Ringert;Bernhard Rumpe
Mace4 参考手册和指南
DOI：
10.2172/822574
发表时间：
2003
期刊：
ArXiv
影响因子：
--
作者：
W. McCune
通讯作者：
W. McCune
寻找声明性规范的最小不可满足核心
DOI：
--
发表时间：
2008
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Emina Torlak;F. Chang;D. Jackson
通讯作者：
D. Jackson
验证开放流交换机规格的（不是）好方法：使用合金对开放流交换机进行形式化建模
DOI：
10.1145/2486001.2491711
发表时间：
2013
期刊：
Proceedings of the ACM SIGCOMM 2013 conference on SIGCOMM
影响因子：
--
作者：
Natali Ruchansky;Davide Proserpio
通讯作者：
Davide Proserpio
影响因子：
2
作者：
Simons, DJ
通讯作者：
Simons, DJ