![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Chapter and Conference Paper
The Gradual Verifier
Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress o...
-
Chapter and Conference Paper
Verification of GUI Applications: A Black-Box Approach
In this paper, we propose to base the verification of a GUI application on a reference model used in black-box testing. The reference model is a formal model for the behavior of the GUI application. It is derived...
-
Chapter and Conference Paper
A Theory for Control-Flow Graph Exploration
Detection of infeasible code has recently been identified as a scalable and automated technique to locate likely defects in software programs. Given the (acyclic) control-flow graph of a procedure, infeasible ...
-
Chapter and Conference Paper
Reconstructing Paths for Reachable Code
Infeasible code has proved to be an interesting target for static analysis. It allows modular and scalable analysis, and at the same time, can be implemented with a close-to-zero rate of false warnings. The ch...
-
Chapter and Conference Paper
Parameterized GUI Tests
GUI testing is a form of system testing where test cases are based on user interactions. A user interaction may be encoded by a sequence of events (e.g., mouse clicks) together with input data (e.g., string va...