Formal specifications often contain partial functions that may lead to ill-defined terms. A common technique to eliminate ill-defined terms is to require well-definedness conditions to be proven. The main advantage of this technique is that it allows us to reason in a two-valued logic even if the underlying specification language has a three-valued semantics. Current approaches generate well-definedness conditions that grow exponentially with respect to the input formula. As a result, many tools prove shorter, but stronger approximations of these well-definedness conditions instead. We present a procedure which generates well-definedness conditions that grow linearly with respect to the input formula. The procedure has been implemented in the Spec# verification tool. We also present empirical results that demonstrate the improvements made. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Darvas, Á., Mehta, F., & Rudich, A. (2008). Efficient well-definedness checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 100–115). https://doi.org/10.1007/978-3-540-71070-7_8
Mendeley helps you to discover research relevant for your work.