To check whether a program meets its specification, specification-based testing can only reveal bugs but cannot strictly prove that there is no bug in programs. Although formal verification can provide a strict proof ...
详细信息
ISBN:
(纸本)9798400714740
To check whether a program meets its specification, specification-based testing can only reveal bugs but cannot strictly prove that there is no bug in programs. Although formal verification can provide a strict proof for the functional correctness of programs with respect to the corresponding specifications, it often requires significant manual expertise to derive loop invariants to complete automated verification. Testing-based formal verification (TBFV) integrates specification-based testing and formal verification to implement automated verification of whether a program satisfies its specification without the need to derive loop invariants. In this paper, we implement the TBFV4J tool, which supports TBFV for Java programs, where the user only needs to input a functional scenario with Java code and it will automatically perform testing and verification.
Self-reflection is evaluation of one's inferential processes often triggered by complex social and emotional experiences, characterized by their ambiguity and unpredictability, pushing one to re-interpret the expe...
详细信息
ISBN:
(纸本)9781450390927
Self-reflection is evaluation of one's inferential processes often triggered by complex social and emotional experiences, characterized by their ambiguity and unpredictability, pushing one to re-interpret the experience, and update existing knowledge. Using immersive Virtual Reality (VR), we aimed to support social and emotional learning (SEL) through reflection in psychology education. We used the case of psychosis as it involves ambiguous perceptual experiences. With a codesign workshop, we designed a VR prototype that simulates the perceptual, cognitive, affective, and social elements of psychotic experiences, followed by a user-study with psychology students to evaluate the potential of this technology to support reflection. Our analyses suggested that technology-mediated reflection in SEL involves two dimensions: spontaneous perspective-taking and shared state of affect. By exploring the subjective qualities of reflection with the said dimensions, our work contributes to the literature on technology-supported learning and VR developers designing for reflection.
Bluetooth requires device pairing to ensure security in data transmission, encumbering a number of ad-hoc, transactional interactions that require both ease-of-use and "good enough"security: e.g., sharing co...
详细信息
A good graphical userinterface (GUI) is crucial for an application's usability, so vendors and regulatory agencies increasingly place restrictions on how GUI elements should appear to and interact with users. Mot...
详细信息
ISBN:
(纸本)9781450385626
A good graphical userinterface (GUI) is crucial for an application's usability, so vendors and regulatory agencies increasingly place restrictions on how GUI elements should appear to and interact with users. Motivated by this concern, this paper presents a new technique (based on static analysis) for checking conformance between (Android) applications and GUI policies expressed in a formal specification language. In particular, this paper (1) describes a specification language for formalizing GUI policies, (2) proposes a new program abstraction called an event-driven layout forest, and (3) describes a static analysis for constructing this abstraction and checking it against a GUI policy. We have implemented the proposed approach in a tool called Venus, and we evaluate it on 2361 Android applications and 17 policies. Our evaluation shows that Venus can uncover malicious applications that perform ad fraud and identify violations of GUI design guidelines and GDPR laws.
Conventional defect inspections in newly constructed indoor environments still rely heavily on manual checking and judgement, which can be costly, time-consuming, superficial, and prone to human errors. In this paper,...
详细信息
As AI applications are widely deployed in various fields, the computing cost of AI is skyrocketing. The high cost not only puts pressure on the environment but also poses challenges for researchers entering the field ...
详细信息
This paper aims to develop a Matlab application for computer-assisted learning in the evaluation of liver tumors using ultrasound. Diagnosing liver tumors detected during standard ultrasound exams is challenging for d...
详细信息
Research software is often built as prototypes that never get widespread usage and are left unmaintained after a few papers get published. To counteract this trend, we propose a method for building research software w...
详细信息
The proceedings contain 19 papers. The topics discussed include: risks of mobile ambient sensors and user awareness, concerns, and preferences;SOK: young children’s cybersecurity knowledge, skills & practice: a s...
ISBN:
(纸本)9781450397001
The proceedings contain 19 papers. The topics discussed include: risks of mobile ambient sensors and user awareness, concerns, and preferences;SOK: young children’s cybersecurity knowledge, skills & practice: a systematic literature review;what cookie consent notices do users prefer: a study in the wild;‘I just want to play games with friends and it asked me for all of my information’: trading privacy for connection during the COVID-19 pandemic;exploring deceptive design patterns in voice interfaces;vision: design fiction for cybersecurity: using science fiction to help software developers anticipate problems;shoulder surfing through the social lens: a longitudinal investigation & insights from an exploratory diary study;privacy, permissions, and the health app ecosystem: a stack overflow exploration;and assessing real-world applicability of redesigned developer documentation for certificate validation errors.
We introduce the Collection Space Navigator (CSN), a browser-based visualization tool to explore, research, and curate large collections of visual digital artifacts that are associated with multidimensional data, such...
详细信息
暂无评论