We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...
In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...
We present a statistical framework to automatically determine an associated color for a given arbitrary semantic expression. The expression can not only be a color name but any word or character string. In addition to the color value, we are also able to c ...
We investigate the regularity of the free boundary for the Signorini problem in Rn+1. It is known that regular points are (n−1)-dimensional and C∞. However, even for C∞ obstacles φ, the set of non-regular (or degenerate) points could be very large—e.g. wit ...
In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the ...
Unsupervised template induction over email data is a central component in applications such as information extraction, document classification, and auto-reply. The benefits of automatically generating such templates are known for structured data, e.g. mach ...
The string method is a general and flexible strategy to compute the most probable transition path for an activated process (rare event). We apply here the atomistic string method in the density field to the Cassie-Wenzel transition, a central problem in th ...
We introduce a precise interprocedural effect analysis for programs with mutable state, dynamic object allocation, and dynamic dispatch. Our analysis is precise even in the presence of dynamic dispatch where the context-insensitive estimate on the number o ...
