Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...
We consider the problem of comparing several samples of stochastic processes with respect to their second-order structure, and describing the main modes of variation in this second order structure, if present. These tasks can be seen as an Analysis of Vari ...
Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...
This thesis demonstrates that it is feasible for systems code to expose a latency interface that describes its latency and related side effects for all inputs, just like the code's semantic interface describes its functionality and related side effects.S ...
This Replicating Computational Report (RCR) describes (a) our datAFLow fuzzer and (b) how to replicate the results in "datAFLow: Toward a Data-Flow-Guided Fuzzer." Our primary artifact is the datAFLow fuzzer. Unlike traditional coverage-guided greybox fuzz ...
Systems and methods for monitoring penile tumescence are provided that overcome the drawbacks of previously known systems by providing a wearable formed of a flexible and elastic tube having a plurality of sensors disposed on or embedded within it, the wea ...
The potential of automatic code generation through Model-Driven Engineering (MDE) frameworks has yet to be realized. Beyond their ability to help software professionals write more accurate, reusable code, MDE frameworks could make programming accessible fo ...
Fuzzing has emerged as the most broadly used testing technique to discover bugs. Effective fuzzers rely on coverage to prioritize inputs that exercise new program areas. Edge-based code coverage of the Program Under Test (PUT) is the most commonly used cov ...
The hardware complexity of modern machines makes the design of adequate programming models crucial for jointly ensuring performance, portability, and productivity in high-performance computing (HPC). Sequential task-based programming models paired with adv ...
Automated fact-checking is a needed technology to curtail the spread of online misinformation. One current framework for such solutions proposes to verify claims by retrieving supporting or refuting evidence from related textual sources. However, the reali ...
